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_*
.