From: yoni206 <yoni206@users.noreply.github.com>
Date: Thu, 26 Jul 2018 22:16:04 +0000 (-0700)
Subject: Disabling bvLazyRewriteExtf in the right place (#2214)
X-Git-Tag: cvc5-1.0.0~4857
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=68de263452bbde839f0bec7896e3f85a8ab8fb9e;p=cvc5.git

Disabling bvLazyRewriteExtf in the right place (#2214)
---

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 42d8c4730..d807567b7 100644
--- 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 aa5acde6e..325010b1a 100644
--- 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 e5ea20885..bc3ce73b7 100644
--- 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)