diff options
| author | Mathias Preiner <mathias.preiner@gmail.com> | 2021-05-19 10:21:42 -0700 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-05-19 17:21:42 +0000 |
| commit | ff5ecff78ade286f2836c6fa76b6c502fa8f3c3b (patch) | |
| tree | f9ec4b4b461945d4ba32c3294c52f52088fe24bd /src/smt | |
| parent | bcb536ef60cb24c19001c0efbde55ff3a37e114f (diff) | |
bv: Add support for --bitblast=eager. (#6516)
This PR adds support for handling --bitblast=eager in the new bitblast solver.
Diffstat (limited to 'src/smt')
| -rw-r--r-- | src/smt/set_defaults.cpp | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index b97c99eae..7c5d775ed 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -162,10 +162,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) "Incremental eager bit-blasting is currently " "only supported for QF_BV. Try --bitblast=lazy."); } - - // Force lazy solver since we don't handle EAGER_ATOMS in the - // BVSolver::BITBLAST solver. - opts.set(options::bvSolver, options::BVSolver::LAZY); } /* Only BVSolver::LAZY natively supports int2bv and nat2bv, for other solvers |