[proofs] Set BV solver to better proof-producing one when proofs on (#6903)

Since the internal bitblaster can be way slower, the regressions that would have slow runs when --check-proofs is passed now have the command line that forces the use of the default bitblaster.

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index c7a2c8916646cbce8e10ff296b15adaa0f05c83d..0a5c399ec5c794ecd0d7d0e98b6208d97886745f 100644 (file)
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -411,6 +411,18 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver)
     opts.bv.bvAssertInput = false;
   }
 
+  // If proofs are required and the user did not specify a specific BV solver,
+  // we make sure to use the proof producing BITBLAST_INTERNAL solver.
+  if (options::produceProofs()
+      && options::bvSolver() != options::BVSolver::BITBLAST_INTERNAL
+      && !opts.bv.bvSolverWasSetByUser
+      && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT)
+  {
+    Notice() << "Forcing internal bit-vector solver due to proof production."
+             << std::endl;
+    opts.bv.bvSolver = options::BVSolver::BITBLAST_INTERNAL;
+  }
+
   // whether we want to force safe unsat cores, i.e., if we are in the default
   // ASSUMPTIONS mode, since other ones are experimental
   bool safeUnsatCores =

diff --git a/test/regress/regress0/fp/issue-5524.smt2 b/test/regress/regress0/fp/issue-5524.smt2
index 741d77a19258fb737929016d090d8287db677e9a..3902f9c370387c0061940711fc6a8d252da66109 100644 (file)
--- a/test/regress/regress0/fp/issue-5524.smt2
+++ b/test/regress/regress0/fp/issue-5524.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --bv-solver=bitblast
 ; EXPECT: unsat
 (set-logic QF_FP)
 (declare-fun fpv5 () Float32)

diff --git a/test/regress/regress1/aufbv/bug348.smtv1.smt2 b/test/regress/regress1/aufbv/bug348.smtv1.smt2
index 207da82c5f137c9f59210061ddbfd10704be2f9b..a1fc92d771b79f99339464d32f1f284e4230f20b 100644 (file)
--- a/test/regress/regress1/aufbv/bug348.smtv1.smt2
+++ b/test/regress/regress1/aufbv/bug348.smtv1.smt2
@@ -1,3 +1,4 @@
+; COMMAND-LINE: --bv-solver=bitblast
 (set-option :incremental false)
 (set-info :status unsat)
 (set-logic QF_AUFBV)

diff --git a/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 b/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
index d39ad79f40d764fbeef37c65f466a189362e30f8..7ef6ff8ef5ae653fd749e28923adf0b08279e33f 100644 (file)
--- a/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
+++ b/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-bv
+; COMMAND-LINE: --cegqi-bv --bv-solver=bitblast
 ; EXPECT: unsat
 (set-logic BV)
 (set-info :status unsat)
@@ -8,14 +8,13 @@
 (assert
  (and (bvsle c_main_~i~6 (_ bv3 32)) (bvsle c_main_~i~6 (_ bv2 32))
  (exists ((v_nnf_34 (_ BitVec 32)))
-  (and (bvsle (bvadd v_nnf_34 (_ bv3 32)) c_main_~k~6) 
+  (and (bvsle (bvadd v_nnf_34 (_ bv3 32)) c_main_~k~6)
   (bvsle v_nnf_34 (_ bv3 32)) (bvsle c_main_~j~6 (bvadd (bvmul (_ bv2 32) v_nnf_34) (_ bv1 32)))))))
 (assert
  (not
  (and (bvsle c_main_~i~6 (_ bv3 32)) (bvsle c_main_~i~6 (_ bv2 32))
  (exists ((v_nnf_30 (_ BitVec 32)))
-  (and (bvsle (bvadd v_nnf_30 (_ bv1 32)) c_main_~k~6) 
+  (and (bvsle (bvadd v_nnf_30 (_ bv1 32)) c_main_~k~6)
   (bvsle v_nnf_30 (_ bv3 32)) (bvsle c_main_~j~6 (bvadd (bvmul (_ bv2 32) v_nnf_30) (_ bv1 32))))))))
 (check-sat)
 (exit)
-

diff --git a/test/regress/regress2/bug394.smt2 b/test/regress/regress2/bug394.smt2
index c0c8ca48cbbb6a8023b21b1720bc9dd19d316ef1..c32ca4ab88b69a4c7bfec63a69a4e0a187601e13 100644 (file)
--- a/test/regress/regress2/bug394.smt2
+++ b/test/regress/regress2/bug394.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --incremental
+; COMMAND-LINE: --incremental --bv-solver=bitblast
 ; EXPECT: sat
 ; EXPECT: unsat
 ; EXPECT: unsat