From 6411f92760a9116dec7e3390dd1d2f1bd8566e94 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 2 Sep 2020 16:20:31 -0700 Subject: [PATCH] Fix CryptoMiniSat build, regression (#5006) This commit fixes builds that include CryptoMiniSat after commit 8ad308b removed them. It also fixes one of the regressions that requires unsat cores but was run when the build was configured without them. --- src/prop/cryptominisat.cpp | 1 - test/regress/regress1/sygus-abduct-test-user.smt2 | 1 + 2 files changed, 1 insertion(+), 1 deletion(-) diff --git a/src/prop/cryptominisat.cpp b/src/prop/cryptominisat.cpp index 92817a70c..9927172be 100644 --- a/src/prop/cryptominisat.cpp +++ b/src/prop/cryptominisat.cpp @@ -62,7 +62,6 @@ void toInternalClause(SatClause& clause, CryptoMinisatSolver::CryptoMinisatSolver(StatisticsRegistry* registry, const std::string& name) : d_solver(new CMSat::SATSolver()), - d_bvp(nullptr), d_numVariables(0), d_okay(true), d_statistics(registry, name) diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2 index bb02ebce2..fed9bd2a6 100644 --- a/test/regress/regress1/sygus-abduct-test-user.smt2 +++ b/test/regress/regress1/sygus-abduct-test-user.smt2 @@ -1,3 +1,4 @@ +; REQUIRES: proofs ; COMMAND-LINE: --produce-abducts ; COMMAND-LINE: --produce-abducts --sygus-core-connective ; SCRUBBER: grep -v -E '(\(define-fun)' -- 2.30.2