Disabling bvLazyRewriteExtf in the right place (#2214)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 42d8c4730f0e01c45f054c19c71998caf9ab7e46..d807567b70f349c20cba76ba4b39503d52ce491c 100644 (file)
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1767,11 +1767,6 @@ void SmtEngine::setDefaults() {
     options::bvEagerExplanations.set(true);
   }
 
-  if( !options::bitvectorEqualitySolver() ){
-    Trace("smt") << "disabling bvLazyRewriteExtf since equality solver is disabled" << endl;
-    options::bvLazyRewriteExtf.set(false);
-  }
-
   // Turn on arith rewrite equalities only for pure arithmetic
   if(! options::arithRewriteEq.wasSetByUser()) {
     bool arithRewriteEq = d_logic.isPure(THEORY_ARITH) && d_logic.isLinear() && !d_logic.isQuantified();
@@ -2320,6 +2315,22 @@ void SmtEngine::setDefaults() {
       options::bitvectorInequalitySolver.set(false);
     }
   }
+
+  if (!options::bitvectorEqualitySolver())
+  {
+    if (options::bvLazyRewriteExtf())
+    {
+      if (options::bvLazyRewriteExtf.wasSetByUser())
+      {
+        throw OptionException(
+            "--bv-lazy-rewrite-extf requires --bv-eq-solver to be set");
+      }
+    }
+    Trace("smt")
+        << "disabling bvLazyRewriteExtf since equality solver is disabled"
+        << endl;
+    options::bvLazyRewriteExtf.set(false);
+  }
 }
 
 void SmtEngine::setProblemExtended(bool value)

diff --git a/test/regress/regress0/bv/bv2nat-ground-c.smt2 b/test/regress/regress0/bv/bv2nat-ground-c.smt2
index aa5acde6eba483c42d7e6db6468a6acfc871c51a..325010b1a4b1d24936cf3529daa5e1a2323c0c88 100644 (file)
--- a/test/regress/regress0/bv/bv2nat-ground-c.smt2
+++ b/test/regress/regress0/bv/bv2nat-ground-c.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BVLIA)
 (set-info :status unsat)

diff --git a/test/regress/regress0/bv/bv2nat-simp-range.smt2 b/test/regress/regress0/bv/bv2nat-simp-range.smt2
index e5ea20885758110eebe2dec669130c50b0e7ec82..bc3ce73b743e11655dd8253ade3ea8e15e8b4303 100644 (file)
--- a/test/regress/regress0/bv/bv2nat-simp-range.smt2
+++ b/test/regress/regress0/bv/bv2nat-simp-range.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)