do not delete reason clauses

krobelus · May 28, 2019 · e0e1e52 · e0e1e52
1 parent de8a97c
commit e0e1e52
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/minisat/core/Solver.cc b/minisat/core/Solver.cc
@@ -633,7 +633,10 @@ void Solver::removeSatisfied(vec<CRef>& cs)
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
         if (satisfied(c))
-            removeClause(cs[i]);
+            if (locked(c))
+                cs[j++] = cs[i];
+            else
+                removeClause(cs[i]);
         else{
             // Trim clause:
             assert(value(c[0]) == l_Undef && value(c[1]) == l_Undef);