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

diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp
index feb9373975b0081c941c25e1e454b44faf2cc554..b701df173f395545551dbe9b7fcdfcd90e89a641 100644 (file)
--- 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;