summaryrefslogtreecommitdiff
path: root/src/prop
diff options
context:
space:
mode:
Diffstat (limited to 'src/prop')
-rw-r--r--src/prop/sat_proof_manager.cpp2
1 files changed, 2 insertions, 0 deletions
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback