diff options
Diffstat (limited to 'src/smt/set_defaults.cpp')
| -rw-r--r-- | src/smt/set_defaults.cpp | 26 |
1 files changed, 0 insertions, 26 deletions
diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 31d14c569..67c5c5647 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -189,8 +189,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) if (options::solveBVAsInt() != options::SolveBVAsIntMode::OFF) { - // do not rewrite bv2nat eagerly - opts.bv.bvLazyRewriteExtf = true; if (options::boolToBitvector() != options::BoolToBVMode::OFF) { throw OptionException( @@ -215,14 +213,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) logic.lock(); } } - else if (options::bvSolver() == options::BVSolver::SIMPLE - || options::bvSolver() == options::BVSolver::BITBLAST) - { - // Only BVSolver::LAZY natively supports int2bv and nat2bv, for other - // solvers we need to eagerly eliminate the operators. Note this is only - // applied if we are not eliminating BV (e.g. with solveBVAsInt). - opts.bv.bvLazyReduceExtf = false; - } // set options about ackermannization if (options::ackermann() && options::produceModels() @@ -1401,22 +1391,6 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) opts.arrays.arraysOptimizeLinear = false; } - if (!options::bitvectorEqualitySolver()) - { - if (options::bvLazyRewriteExtf()) - { - if (opts.bv.bvLazyRewriteExtfWasSetByUser) - { - throw OptionException( - "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set"); - } - } - Trace("smt") - << "disabling bvLazyRewriteExtf since equality solver is disabled" - << std::endl; - opts.bv.bvLazyRewriteExtf = false; - } - if (options::stringFMF() && !opts.strings.stringProcessLoopModeWasSetByUser) { Trace("smt") << "settting stringProcessLoopMode to 'simple' since " |