Smt-Switch 0.2.0
Pre-release
Pre-release
This release contains:
- Backends for quantifier-free solving with Boolector, CVC4 and MathSAT for the following theories
- Fixed with bitvectors
- Linear/Nonlinear integer arithmetic (except Boolector)
- Linear/Nonlinear real arithmetic (except Boolector)
- Arrays
- Uninterpreted functions
- Python bindings
Known issues:
- Transferring terms between solvers is not always supported
- Some solvers have non-SMT-LIB internal representations that are not currently mapped back to SMT-LIB correctly