projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: 2e00199) | patch
bv: Enable bitblast solver by default. (#6660)
authorMathias Preiner <mathias.preiner@gmail.com>
Fri, 4 Jun 2021 13:30:35 +0000 (06:30 -0700)
committerGitHub <noreply@github.com>
Fri, 4 Jun 2021 13:30:35 +0000 (13:30 +0000)
commit125b1c56d64b6dde1638565152b86950ef3c1342
tree4469c67dd1c3029d33d5537040c0610bbd217b42tree
parent2e001991f926c307ff0f812dafca4d9dc6e4d831commit | diff
bv: Enable bitblast solver by default. (#6660)

This commit enables the new bitblast solver by default. This commit also fixes model generation for Boolean variables when --bitblast=eager is enabled.

Fixes #3958, #5396, #5736, #5743, #5947.
12 files changed:
src/options/bv_options.toml diff | blob | history
src/theory/bv/bv_solver_bitblast.cpp diff | blob | history
test/regress/CMakeLists.txt diff | blob | history
test/regress/regress0/bv/bv-int-collapse1.smt2 diff | blob | history
test/regress/regress0/bv/bv-int-collapse2.smt2 diff | blob | history
test/regress/regress0/bv/issue5396.smt2 [new file with mode: 0644] blob
test/regress/regress0/issue5736.smt2 [new file with mode: 0644] blob
test/regress/regress0/issue5743.smt2 [new file with mode: 0644] blob
test/regress/regress0/issue5947.smt2 [new file with mode: 0644] blob
test/regress/regress1/bv/bv2nat-ground.smt2 diff | blob | history
test/regress/regress1/bv/issue3958.smt2 [new file with mode: 0644] blob
test/unit/theory/theory_bv_white.cpp diff | blob | history