A tool for testing SMT solver for incompleteness bugs, i.e., unexpected unknown-results. janus has found dozens of incompleteness bugs in in the two state-of-the-art SMT solvers Z3 and cvc5.
Incompleteness bugs: janus can find two types of incompleteness bugs, regression incompleteneses and implication incompletenesses. Regression incompletenesses are caused by (recent) code changes leading to an incompleteness on previously decided formulas. Typically they affect client software that worked correctly with an older version of the SMT solver but fails after updating the SMT solver. Implication incompletenesses occur when an SMT solver can decide a given input formula but minor changes in the formula cause the solver to report unknown. Such formula pairs can suggest possible improvements for SMT solvers, e.g., to formula rewriters, pre-processors, theory solvers etc.
janus is part of the YinYang project and its codebase is based on a fork of the SMT solver testing framework yinyang.
git clone https://github.com/testsmt/janus.git
pip3 install antlr4-python3-runtime==4.9.2Note that you may want to add janus/bin to your PATH, for running janus conveniently without prefix.
-
Get pre-processed SMT-LIB 2 seeds. Clone the repository
https://github.com/testsmt/semantic-fusion-seedsto obtain pre-processed SMT-LIB files (sat/unsat). Alternatively, you can download and pre-process benchmarks directly from the SMT-LIB website or supply your own benchmarks. -
Get and build SMT solvers for testing. Install two or more SMT solvers that support the SMT-LIB 2 format. You may find it convenient to add them to your PATH.
-
Run janus on the seeds e.g. with Z3 and cvc5.
a.) Regression incompleteness mode
janus "z3-trunk" -cr "z3-4.8.10" -o sat examples/phi1.smt2
This command checks the z3-trunk against its stable release z3-4.8.10 for incompleteness regressions.
b.) Implication incompleteness mode
janus "z3;cvc5" -o sat examples/phi1.smt2This command checks both z3 and cvc5 for implication incompletenesses.
Execute janus --help for more information.
For details on the internals of janus, read our ASE '22 paper. In it we describe Weakening & Strengthening which is the underlying technique behind janus, how we used janus in an incompleteness bug hunting campaign for Z3 and cvc5 etc.
You can view all bugs reported with janus via the following link. The research and tool were conducted and developed as part of Mauro Bringolf's master thesis with the AST Lab at ETH Zurich.
For bugs/issues/questions/feature requests please file an issue. We are always happy to receive your feedback or help you adjust janus to the needs of your custom solver, help you build on, compare against, help integrate janus.
- Mauro Bringolf's thesis
- Project yinyang website with bug statistics, talk videos, etc.