From: Haniel Barbosa Date: Tue, 26 Oct 2021 20:27:39 +0000 (-0300) Subject: [proofs] Reset local var in SatProofManager since incremental exists (#7500) X-Git-Tag: cvc5-1.0.0~964 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=28d75255c93fdfd8bca3cac4673702f6ffc8b3be;p=cvc5.git [proofs] Reset local var in SatProofManager since incremental exists (#7500) Fixes cvc5/cvc5-projects#317 --- diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index e650473b3..74617a521 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -722,6 +722,8 @@ void SatProofManager::finalizeProof() << "SatProofManager::finalizeProof: conflicting (lazy) satLit: " << d_conflictLit << "\n"; finalizeProof(getClauseNode(d_conflictLit), {d_conflictLit}); + // reset since if in incremental mode this may be used again + d_conflictLit = undefSatVariable; } void SatProofManager::finalizeProof(Minisat::Lit inConflict, bool adding) diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt index 625d5faea..2a96818eb 100644 --- a/test/regress/CMakeLists.txt +++ b/test/regress/CMakeLists.txt @@ -449,7 +449,7 @@ set(regress_0_tests regress0/cores/issue4971-2.smt2 regress0/cores/issue4971-3.smt2 regress0/cores/issue5079.smt2 - regress0/cores/issue5234-uc-ua.smt2 + regress0/cores/issue5234-uc-ua.smt2 regress0/cores/issue5238.smt2 regress0/cores/issue5902.smt2 regress0/cores/issue5908.smt2 @@ -857,6 +857,7 @@ set(regress_0_tests regress0/proofs/open-pf-datatypes.smt2 regress0/proofs/open-pf-if-unordered-iff.smt2 regress0/proofs/open-pf-rederivation.smt2 + regress0/proofs/project-issue317-inc-sat-conflictlit.smt2 regress0/proofs/qgu-fuzz-1-bool-sat.smt2 regress0/proofs/qgu-fuzz-2-bool-chainres-checking.smt2 regress0/proofs/qgu-fuzz-3-chainres-checking.smt2 diff --git a/test/regress/regress0/proofs/project-issue317-inc-sat-conflictlit.smt2 b/test/regress/regress0/proofs/project-issue317-inc-sat-conflictlit.smt2 new file mode 100644 index 000000000..0f7f89651 --- /dev/null +++ b/test/regress/regress0/proofs/project-issue317-inc-sat-conflictlit.smt2 @@ -0,0 +1,7 @@ +; EXPECT: unsat +; EXPECT: unsat +(set-logic ALL) +(declare-const __ (_ BitVec 1)) +(set-option :incremental true) +(check-sat-assuming ((bvsgt ((_ sign_extend 42) (bvcomp ((_ zero_extend 10) __) ((_ zero_extend 10) __))) (_ bv0 43)))) +(check-sat-assuming ((bvsgt ((_ sign_extend 42) (bvcomp ((_ zero_extend 10) __) ((_ zero_extend 10) __))) (_ bv0 43)))) \ No newline at end of file