[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 e650473b3f1874b9e0bf98acc53b92a39d630276..74617a52173db4a19f810f7adef50eba54b82e62 100644 (file)
--- 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 625d5faea52082335537d763b2fb66189195502c..2a96818eb11badece80f818e7bad0c9d555097c0 100644 (file)
--- 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 (file)
index 0000000..0f7f896
--- /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