Welcome to lazybv2int. It is an SMT-solver for the theory of bit-vectors and uninterpreted functions.
lazybv2int is based on a translation of the input problem into an equisatisfiable problem over the theory of integer arithmetic and uninterpreted functions. There are several variants of this translation, all activated with various options that are described in the tool's help (see below).
Incremental solving is supported.
The tool is built on top of smt-switch. It uses mathsat to parse the input problem and cvc4 to solve the arithmetic translations.
A description of lazybv2int is available here.
The tool is an early prototype. Currently, the technique is implemented as part of cvc5, and is described in: Bit-precise reasoning via Int-blasting
# make sure you meet all the license requirements to use mathsat
./contrib/setup-msat.sh
./contrib/setup-smt-switch.sh
./configure.sh
cd build
make
From build do:
./lazybv2int <smtlib-file>
or
./lazybv2int -h
to see possible options.