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 92817a70c94eba4192f184f9c82d5416db77ef35..9927172bef685d7b8998728353e1cdc7a52a8983 100644 (file)
--- 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 bb02ebce2089031efb7c04e368889e4d2e6e7fcc..fed9bd2a6d2c9587c6379756c0435986a79238ed 100644 (file)
--- 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)'