From: Mathias Preiner <mathias.preiner@gmail.com>
Date: Tue, 2 Nov 2021 01:26:26 +0000 (-0700)
Subject: Fix setDefaults() for proofs with bitblast-internal. (#7552)
X-Git-Tag: cvc5-1.0.0~909
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b5849b2061c841926f7548858613223d1e805b21;p=cvc5.git

Fix setDefaults() for proofs with bitblast-internal. (#7552)
---

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index feb937397..b701df173 100644
--- a/src/smt/set_defaults.cpp
+++ b/src/smt/set_defaults.cpp
@@ -898,8 +898,7 @@ bool SetDefaults::incompatibleWithProofs(Options& opts,
   // 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 (opts.bv.bvSolver != options::BVSolver::BITBLAST_INTERNAL
-      && !opts.bv.bvSolverWasSetByUser
-      && opts.bv.bvSatSolver == options::SatSolverMode::MINISAT)
+      && !opts.bv.bvSolverWasSetByUser)
   {
     Notice() << "Forcing internal bit-vector solver due to proof production."
              << std::endl;