Remove support for lazy BV extended function reductions and inferences (#6728)

solve-int-as-bv is now the preferred method for solving these benchmarks.

Adds solve-int-as-bv to a regression that became slow in my previous commit.

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 "