Command Line Interface
Bitwuzla provides a command line interface that supports parsing of SMT-LIBv2 [BFT17] and non-sequential BTOR2 [NPWB18] input files (i.e. no model-checking features supported).
The command line usage of Bitwuzla is as follows:
Usage:
bitwuzla [<options>] [<input>]
Options:
<input> [<stdin>] input file
-h, --help print this message and exit
-V, --version print version and exit
-c, --copyright print copyright and exit
-p, --print-formula print formula in smt2 format
--print-unsat-core print unsat core in smt2 format
--print-model print model in smt2 format
--print-no-letify do not letify expressions when
printing
-P, --parse-only [false] only parse input without calling
check-sat
--pp-only [false] exit after preprocessing
--bv-output-format [2] output number format for bit-vector
values {2, 10, 16}
-t <n>, --time-limit <n> [0] time limit in milliseconds
--lang <M> [smt2] input language {smt2, btor2}
-l <n>, --log-level <n> [0] log level
-m, --produce-models [false] model production
--produce-unsat-assumptions [false] unsat assumptions production
--produce-unsat-cores [false] unsat core production
-s <n>, --seed <n> [27644437] seed for the random number generator
-v <n>, --verbosity <n> [0] verbosity level
-T <n>, --time-limit-per <n> [0] time limit in milliseconds per
satisfiability check
-M <n>, --memory-limit <n> [0] set maximum memory limit in MB
-j <n>, --nthreads <n> [1] set number of threads to utilize in
parallel (currently, this only
configures parallel threads in the
CryptoMiniSat back end)
--relevant-terms [false] consider relevant terms only when
checking
--bv-solver <M> [bitblast] bv solver engine {preprop, prop,
bitblast}
-rwl <n>, --rewrite-level <n> [2] rewrite level
-S <M>, --sat-solver <M> [cadical] backend SAT solver {kissat, cms,
cadical}
--prop-const-bits [true] use constant bits propagation
--prop-ineq-bounds [true] infer inequality bounds for
invertibility conditions and
inverse value computation
--prop-nprops <n> [0] number of propagation steps used as a
limit for propagation-based local
search engine
--prop-nupdates <n> [0] number of model value updates used as a
limit for propagation-based local
search engine
--prop-opt-lt-concat-sext [false] optimization for inverse value
computation of inequalities over
concat and sign extension operands
--prop-path-sel <M> [essential] propagation path selection mode for
propagation-based local search
engine {random, essential}
--prop-prob-pick-rand-input <n> [10] probability for selecting a random
input instead of an essential input
(interpreted as <n>/1000)
--prop-prob-pick-inv-value <n> [990] probability for producing inverse
rather than consistent values
(interpreted as <n>/1000)
--prop-sext [true] use sign_extend nodes for concats
that represent sign_extend nodes for
propagation-based local search
engine
--prop-normalize [false] enable normalization for local
search
--abstraction [false] enable abstraction module
--abstraction-bv-size <n> [32] enable abstraction for bit-vector
terms of given minimum size
--abstraction-eager-refine [false] add all violated abstraction lemmas
at once
--abstraction-value-limit <n> [8] value instantiation limit
bv-size/<n> until adding original
term as refinement
--abstraction-value-only [false] only add value instantiations
--abstraction-assert [false] assertion abstraction
--abstraction-assert-refs <n> [100] number of assertion refinements per
check
--abstraction-initial-lemmas [false] use initial lemma refinements only
--abstraction-inc-bitblast [false] incrementally bit-blast bvmul and
bvadd
--abstraction-bvadd [false] term abstraction for bvadd
--abstraction-bvmul [true] term abstraction for bvmul
--abstraction-bvudiv [true] term abstraction for bvudiv
--abstraction-bvurem [true] term abstraction for bvurem
--abstraction-eq [false] term abstraction for =
--abstraction-ite [false] term abstraction for ite
--preprocess [true] enable preprocessing
--pp-contr-ands [false] enable contradicting ands
preprocessing pass
--pp-elim-extracts [false] eliminate extract on BV constants
--pp-elim-bvudiv [false] eliminate bvudiv and bvurem
--pp-embedded [true] enable embedded constraint
preprocessing pass
--pp-flatten-and [true] enable AND flattening preprocessing
pass
--pp-normalize [true] enable normalization pass
--pp-skeleton-preproc [true] enable skeleton preprocessing pass
--pp-variable-subst [true] enable variable substitution
preprocessing pass
--pp-variable-subst-norm-eq [true] enable equality normalization via
Gaussian elimination if variable
substitution preprocessing pass is
enabled
--pp-variable-subst-norm-diseq [false] enable disequality normalization if
variable substitution
preprocessing pass is enabled
--pp-variable-subst-norm-bv-ineq [false] enable bit-vector unsigned
inequality normalization if
variable substitution
preprocessing pass is enabled
--dbg-rw-node-thresh <n> [0] warn threshold [#] for new nodes
created through rewriting steps
--dbg-pp-node-thresh <n> [0] warn threshold [%] for new nodes
created through preprocessing in
total
--check-model [true] check model for each satisfiable
query
--check-unsat-core [true] check unsat core for each
unsatisfiable query