diff options
| -rw-r--r-- | src/prop/cryptominisat.cpp | 1 | ||||
| -rw-r--r-- | test/regress/regress1/sygus-abduct-test-user.smt2 | 1 |
2 files changed, 1 insertions, 1 deletions
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)' |