0.4.1

bugfix release.

0.4

Now supports quantification on datatypes and booleans. The quantified formula is lazily unrolled as a conjunction or disjunction. Undefined is used as the last conjunct/disjunct to account for the loss of precision.

0.3.1

Bugfix release, also compatible with more recent versions of containers and msat.

0.3

Second usable version, with many small features added:

• add flag --check-proof for checking SAT solver proofs
• remove parser for custom format; only keep TIP; remove .lisp from tests
• less accurate detection of incomplete expansions (without unsat-cores)
• bugfixes in uninterpreted types
• detect some evaluation loops with a term_being_evaled field
• internal notion of undefined for asserting, loops, and selectors
• simple prefix skolemization for assert axioms
• add asserting construct
• delay a bit combinatorial explosion for HO functions
• support for HO unknowns
• allow quantification over booleans, translated as conjunction/disjunction
• better error message for HO metas
• add support for selectors

version 0.2

First usable version of smbc. It accepts a fragment of TIP.
For production use, you should really use --check to double-check the models.