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
-P, --parse-only [false] only parse input without calling
check-sat
--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> [42] 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
--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 [true] 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
--preprocess [true] enable preprocessing
--pp-contr-ands [false] enable contradicting ands
preprocessing pass
--pp-elim-extracts [false] eliminate extract on BV constants
--pp-embedded [true] enable embedded constraint
preprocessing pass
--pp-flatten-and [true] enable AND flattening preprocessing
pass
--pp-normalize [true] enable normalization pass
--pp-normalize-share-aware [true] disable normalizations in
normalization pass that may yield
blow-up on the bit-level
--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 [false] check model for each satisfiable
query
--check-unsat-core [false] check unsat core model for each
unsatisfiable query