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

1 files changed, 14 insertions, 8 deletions

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]);