metaSMT-Based SMT-LIB2 Consistency Checker
metaSMT-toolbox-smt2eval is a metaSMT toolbox project that allows
a user to read and evaluate SMT-LIB2 instances utilizing a varity of
different solving engines. The project leverages Z3’s parser to read
files in SMT-LIB2 format and metaSMT to evaluate them.
The following software is required in order to build metaSMT-toolbox-smt2eval
metaSMT-toolbox-smt2eval is not a standalone application but a
toolbox project for metaSMT. The metaSMT source code has to
be installed first. The Z3 library is automatically installed as
a part of metaSMT.
Install metaSMT to directory <metaSMT_DIRECTORY>.
Clone metaSMT-toolbox-smt2eval in directory<metaSMT_DIRECTORY>/toolbox.
Build metaSMT following the normal build instructions. metaSMT
will build in the usual way with the additional executables to check
satisfiability and consistency of SMT-LIB2 instances. The additional
executables follow the naming scheme smt2_sat_check_* andsmt2_consistency_check_*.