Simon Cruanes

see e7f7f6c4873dca817fda9693acd589798f10ea2e

It's actually hard to do because we'd need to check the equisatisfiability of the split clause with *all* the resulting clauses. (it's esa, because technically the boolean atoms are like...

Simplest fix could be to add to sidekick a notion of boolean terms that are not to be considered as literals (namely here, non-closed boolean terms).

Depending on how complicated the changes are, you might have an easier time just adapting the current parser to follow TIP 3. It's nice that they got closer to smtlib,...

depends on merges + release + ocamlformat first

is it more reasonable to ground to SAT, or directly to SMT?

should have a lazy bitvector in `Clause.t` (depends on ordering, so can't be in Lit.t)

Be careful that bit vectors are mutable, like arrays. You could use an option instead to implement the lazy semantics yourself (and never mutate it afterwards). Also be sure to...

side note: orderings typically have their own cache, so if you compute `s

Hmm if we solve #64 (maybe with a custom way of handling `a