Enforcing --no-bv-eq, --no-bv-algebraic and --no-bv-ineq when proofs are enabled (#1801)

Currently, if the user enables proofs but does not disable the algebraic/equality/inequality bv-solvers, then we reach an internal error while printing the proof (unreachable code becomes reachable).
This commit auto-disable these bv options when proofs are enabled, unless these options were set by the user. In such a case, an error message is given to the user.

8 files changed, 149 insertions, 11 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index a65d55859..9cb3387c8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2173,6 +2173,42 @@ void SmtEngine::setDefaults() {
     Warning() << "SmtEngine: turning off incremental solving mode (not yet supported with --proof, try --tear-down-incremental instead)" << endl;
     setOption("incremental", SExpr("false"));
   }
+
+  if (options::proof())
+  {
+    if (options::bitvectorAlgebraicSolver())
+    {
+      if (options::bitvectorAlgebraicSolver.wasSetByUser())
+      {
+        throw OptionException(
+            "--bv-algebraic-solver is not supported with proofs");
+      }
+      Notice() << "SmtEngine: turning off bv algebraic solver to support proofs"
+               << std::endl;
+      options::bitvectorAlgebraicSolver.set(false);
+    }
+    if (options::bitvectorEqualitySolver())
+    {
+      if (options::bitvectorEqualitySolver.wasSetByUser())
+      {
+        throw OptionException("--bv-eq-solver is not supported with proofs");
+      }
+      Notice() << "SmtEngine: turning off bv eq solver to support proofs"
+               << std::endl;
+      options::bitvectorEqualitySolver.set(false);
+    }
+    if (options::bitvectorInequalitySolver())
+    {
+      if (options::bitvectorInequalitySolver.wasSetByUser())
+      {
+        throw OptionException(
+            "--bv-inequality-solver is not supported with proofs");
+      }
+      Notice() << "SmtEngine: turning off bv ineq solver to support proofs"
+               << std::endl;
+      options::bitvectorInequalitySolver.set(false);
+    }
+  }
 }
 
 void SmtEngine::setProblemExtended(bool value)
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 47f2b9245..1b1e83ae3 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -74,25 +74,27 @@ TheoryBV::TheoryBV(context::Context* c, context::UserContext* u,
   setupExtTheory();
   getExtTheory()->addFunctionKind(kind::BITVECTOR_TO_NAT);
   getExtTheory()->addFunctionKind(kind::INT_TO_BITVECTOR);
-
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
     d_eagerSolver = new EagerBitblastSolver(this);
     return;
   }
 
-  if (options::bitvectorEqualitySolver()) {
+  if (options::bitvectorEqualitySolver() && !options::proof())
+  {
     SubtheorySolver* core_solver = new CoreSolver(c, this);
     d_subtheories.push_back(core_solver);
     d_subtheoryMap[SUB_CORE] = core_solver;
   }
 
-  if (options::bitvectorInequalitySolver()) {
+  if (options::bitvectorInequalitySolver() && !options::proof())
+  {
     SubtheorySolver* ineq_solver = new InequalitySolver(c, u, this);
     d_subtheories.push_back(ineq_solver);
     d_subtheoryMap[SUB_INEQUALITY] = ineq_solver;
   }
 
-  if (options::bitvectorAlgebraicSolver()) {
+  if (options::bitvectorAlgebraicSolver() && !options::proof())
+  {
     SubtheorySolver* alg_solver = new AlgebraicSolver(c, this);
     d_subtheories.push_back(alg_solver);
     d_subtheoryMap[SUB_ALGEBRAIC] = alg_solver;
diff --git a/test/regress/Makefile.tests b/test/regress/Makefile.tests
index a29236914..88ea4ebd5 100644
--- a/test/regress/Makefile.tests
+++ b/test/regress/Makefile.tests
@@ -161,6 +161,10 @@ REG0_TESTS = \
 	regress0/bv/bug734.smt2 \
 	regress0/bv/bv-int-collapse1.smt2 \
 	regress0/bv/bv-int-collapse2.smt2 \
+	regress0/bv/bv-options1.smt2 \
+	regress0/bv/bv-options2.smt2 \
+	regress0/bv/bv-options3.smt2 \
+	regress0/bv/bv-options4.smt2 \
 	regress0/bv/bv2nat-ground-c.smt2 \
 	regress0/bv/bv2nat-simp-range.smt2 \
 	regress0/bv/bvmul-pow2-only.smt2 \
diff --git a/test/regress/regress0/bv/bv-options1.smt2 b/test/regress/regress0/bv/bv-options1.smt2
new file mode 100644
index 000000000..b1e87fc7e
--- /dev/null
+++ b/test/regress/regress0/bv/bv-options1.smt2
@@ -0,0 +1,24 @@
+; SCRUBBER: sed -e 's/(error \"Error.in.option.parsing.*$/Error in option parsing/'
+; EXPECT: Error in option parsing
+; COMMAND-LINE: --check-proofs --bv-algebraic-solver
+; EXIT: 1
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(assert (and
+	 (bvult v2 v4)
+	 (bvult v3 v4)
+	 (bvult v0 v1)
+	 (bvult v1 v2)
+	 (bvult v1 v3)
+	 (bvult v4 v5)
+	 (bvult v5 v1)
+	 ))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/bv-options2.smt2 b/test/regress/regress0/bv/bv-options2.smt2
new file mode 100644
index 000000000..d1ee44084
--- /dev/null
+++ b/test/regress/regress0/bv/bv-options2.smt2
@@ -0,0 +1,24 @@
+; SCRUBBER: sed -e 's/(error \"Error.in.option.parsing.*$/Error in option parsing/'
+; EXPECT: Error in option parsing
+; COMMAND-LINE: --check-proofs --bv-eq-solver
+; EXIT: 1
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(assert (and
+	 (bvult v2 v4)
+	 (bvult v3 v4)
+	 (bvult v0 v1)
+	 (bvult v1 v2)
+	 (bvult v1 v3)
+	 (bvult v4 v5)
+	 (bvult v5 v1)
+	 ))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/bv-options3.smt2 b/test/regress/regress0/bv/bv-options3.smt2
new file mode 100644
index 000000000..4d16230b4
--- /dev/null
+++ b/test/regress/regress0/bv/bv-options3.smt2
@@ -0,0 +1,24 @@
+; SCRUBBER: sed -e 's/(error \"Error.in.option.parsing.*$/Error in option parsing/'
+; EXPECT: Error in option parsing
+; COMMAND-LINE: --check-proofs --bv-inequality-solver
+; EXIT: 1
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(assert (and
+	 (bvult v2 v4)
+	 (bvult v3 v4)
+	 (bvult v0 v1)
+	 (bvult v1 v2)
+	 (bvult v1 v3)
+	 (bvult v4 v5)
+	 (bvult v5 v1)
+	 ))
+(check-sat)
+(exit)
diff --git a/test/regress/regress0/bv/bv-options4.smt2 b/test/regress/regress0/bv/bv-options4.smt2
new file mode 100644
index 000000000..842650ebd
--- /dev/null
+++ b/test/regress/regress0/bv/bv-options4.smt2
@@ -0,0 +1,24 @@
+; SCRUBBER: sed -e 's/unsat.*/unsat/'
+; EXPECT: unsat
+; COMMAND-LINE: --check-proofs 
+; EXIT: 0
+(set-logic QF_BV)
+(set-info :smt-lib-version 2.0)
+(set-info :category "crafted")
+(declare-fun v0 () (_ BitVec 16))
+(declare-fun v1 () (_ BitVec 16))
+(declare-fun v2 () (_ BitVec 16))
+(declare-fun v3 () (_ BitVec 16))
+(declare-fun v4 () (_ BitVec 16))
+(declare-fun v5 () (_ BitVec 16))
+(assert (and
+	 (bvult v2 v4)
+	 (bvult v3 v4)
+	 (bvult v0 v1)
+	 (bvult v1 v2)
+	 (bvult v1 v3)
+	 (bvult v4 v5)
+	 (bvult v5 v1)
+	 ))
+(check-sat)
+(exit)
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index db72854eb..ea744d838 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -201,13 +201,6 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
             # If there is no expected output/error and the exit status has not
             # been set explicitly, the benchmark is invalid.
             sys.exit('Cannot determine status of "{}"'.format(benchmark_path))
-
-    if not proof and ('(get-unsat-core)' in benchmark_content
-                      or '(get-unsat-assumptions)' in benchmark_content):
-        print(
-            '1..0 # Skipped: unsat cores not supported without proof support')
-        return
-
     if expected_exit_status is None:
         expected_exit_status = 0
 
@@ -216,6 +209,13 @@ def run_regression(proof, dump, wrapper, cvc4_binary, benchmark_path, timeout):
             os.environ['CVC4_REGRESSION_ARGS'])
     basic_command_line_args += shlex.split(command_line)
     command_line_args_configs = [basic_command_line_args]
+    if not proof and ('(get-unsat-core)' in benchmark_content
+                      or '(get-unsat-assumptions)' in benchmark_content
+                      or '--check-proofs' in basic_command_line_args
+                      or '--dump-proofs' in basic_command_line_args):
+        print(
+            '1..0 # Skipped: unsat cores not supported without proof support')
+        return
 
     extra_command_line_args = []
     if benchmark_ext == '.sy' and \