Releases: stanford-centaur/smt-switch
Releases · stanford-centaur/smt-switch
Pono submission for HWMCC20
Smt-Switch 0.2.0
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