diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-06-04 06:30:35 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-06-04 13:30:35 +0000 |
| commit | 125b1c56d64b6dde1638565152b86950ef3c1342 (patch) | |
| tree | 4469c67dd1c3029d33d5537040c0610bbd217b42 /src/options | |
| parent | 2e001991f926c307ff0f812dafca4d9dc6e4d831 (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.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/bv_options.toml | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index e5b96b54a..fcad51ceb 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -227,7 +227,7 @@ name = "Bitvector Theory" category = "regular" long = "bv-solver=MODE" type = "BVSolver" - default = "LAZY" + default = "BITBLAST" help = "choose bit-vector solver, see --bv-solver=help" help_mode = "Bit-vector solvers." [[option.mode.BITBLAST]] |