From b5849b2061c841926f7548858613223d1e805b21 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Mon, 1 Nov 2021 18:26:26 -0700 Subject: [PATCH] Fix setDefaults() for proofs with bitblast-internal. (#7552) --- src/smt/set_defaults.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) 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; -- 2.30.2