NAME¶

bitwuzla - SMT solver for bit vectors and arrays

DESCRIPTION¶

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 per satisfiability check

-j <n>, --nthreads <n>

[1] set number of threads to utilize in parallel (currently, this only configures parallel threads in the CryptoMiniSat back end)

--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}

--write-aiger <...>

[] write bv abstraction as AIGER to filename

--write-cnf <...>

[] write bv abstraction as CNF to filename

--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

--abstraction

[true] enable abstraction module

--abstraction-bv-size <n>

[33] 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

[false] check model for each satisfiable query

--check-unsat-core

[false] check unsat core for each unsatisfiable query

SEE ALSO¶

The full documentation for bitwuzla is maintained as a Texinfo manual. If the info and bitwuzla programs are properly installed at your site, the command

info bitwuzla

should give you access to the complete manual.