From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Wed, 2 Sep 2020 23:20:31 +0000 (-0700)
Subject: Fix CryptoMiniSat build, regression (#5006)
X-Git-Tag: cvc5-1.0.0~2909
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6411f92760a9116dec7e3390dd1d2f1bd8566e94;p=cvc5.git

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.
---

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)'