From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Tue, 15 Mar 2011 20:48:57 +0000 (+0000)
Subject: fix for bug 254, lemmas were propagating at lower levels, and the conflict clauses... 
X-Git-Tag: cvc5-1.0.0~8657
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d7554865a91733a39dd658e2003ca072e8e2ed4b;p=cvc5.git

fix for bug 254, lemmas were propagating at lower levels, and the conflict clauses asserting literal  would overwrite the propagated literal
let's see if i break the build again
---

diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 80d6b116e..3e4c9d8a2 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -933,17 +933,23 @@ lbool Solver::search(int nof_conflicts)
 
         CRef confl = propagate(check_type);
         if (confl != CRef_Undef){
-            // CONFLICT
-            conflicts++; conflictC++;
-            if (decisionLevel() == 0) return l_False;
-
-	    // Clear the propagated literals
+            // Clear the propagated literals
             lemma_propagated_literals.clear();
             lemma_propagated_reasons.clear();
+
+            // CONFLICT
+            int max_level = 0;
+            do {
+              conflicts++; conflictC++;
+              if (decisionLevel() == 0) return l_False;
 			
-            learnt_clause.clear();
-            int max_level = analyze(confl, learnt_clause, backtrack_level);
-            cancelUntil(backtrack_level);
+              learnt_clause.clear();
+              max_level = std::max(max_level, analyze(confl, learnt_clause, backtrack_level));
+              cancelUntil(backtrack_level);
+
+              // It might have happened that we have repropagated a literal that is actually learnt_clause[0]
+              // so we must go into conflict resolition again
+            } while (value(learnt_clause[0]) != l_Undef);
 
             if (learnt_clause.size() == 1){
                 uncheckedEnqueue(learnt_clause[0]);