Z3 is an SMT solver that combines several theory solvers into a combined framework. It can be used to prove theorems and find counter-examples for non-theorems. Philippe Suter made a JNI binding available. There is also an existing Python binding by Sascha Boehme.
Features:
- Enable check_assumptions without enclosing push/pop. This resolves the limitation described in Limitations:
- Expose coefficients used in arithmetical proofs.
- Allow quantified theory axioms.
- Fixes to the SMT-LIB 2.0 pretty printing mode.
- Detect miss-annotated SMT-LIB benchmarks to avoid crashes when using the wrong solvers. Thanks to Trevor Hansen.
- A digression in the managed API from 2.10 when passing null parameters.
- Crash/incorrect handling of inequalities over the reals during quantifier elimination. Thanks to Mikkel Larsen Pedersen.
- Bug in destructive equality resolution. Thanks to Sascha Boehme.
- Bug in initialization for x64_mt executable on SMT benchmarks. Thanks to Alvin Cheung.
Comments