From 7363e6cdb0d2440114f246ba473bc52bf5228c55 Mon Sep 17 00:00:00 2001
From: Johannes Altmanninger <aclopte@gmail.com>
Date: Sat, 25 May 2019 20:26:44 +0200
Subject: [PATCH] do not delete reason clauses

---
 sources/core/Solver.cc     | 19 ++++++++++++++-----
 sources/simp/SimpSolver.cc |  2 +-
 2 files changed, 15 insertions(+), 6 deletions(-)

diff --git a/sources/core/Solver.cc b/sources/core/Solver.cc
index ac8e596..a2b63c2 100644
--- a/sources/core/Solver.cc
+++ b/sources/core/Solver.cc
@@ -487,7 +487,10 @@ bool Solver::simplifyLearnt_x(vec<CRef>& learnts_x)
                 }
             }
             if (sat){
-                removeClause(cr);
+                if (locked(c))
+                    learnts_x[cj++] = learnts_x[ci];
+                else
+                    removeClause(cr);
             }
             else{
                 detachClause(cr, true);
@@ -602,7 +605,10 @@ bool Solver::simplifyLearnt_core()
                 }
             }
             if (sat){
-                removeClause(cr);
+                if (locked(c))
+                    learnts_core[cj++] = learnts_core[ci];
+                else
+                    removeClause(cr);
             }
             else{
                 detachClause(cr, true);
@@ -727,7 +733,10 @@ bool Solver::simplifyLearnt_tier2()
                 }
             }
             if (sat){
-                removeClause(cr);
+                if (locked(c))
+                    learnts_tier2[cj++] = learnts_tier2[ci];
+                else
+                    removeClause(cr);
             }
             else{
                 detachClause(cr, true);
@@ -1636,7 +1645,7 @@ void Solver::removeSatisfied(vec<CRef>& cs)
     int i, j;
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
-        if (satisfied(c))
+        if (satisfied(c) && !locked(c))
             removeClause(cs[i]);
         else
             cs[j++] = cs[i];
@@ -1650,7 +1659,7 @@ void Solver::safeRemoveSatisfied(vec<CRef>& cs, unsigned valid_mark)
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
         if (c.mark() == valid_mark)
-            if (satisfied(c))
+            if (satisfied(c) && !locked(c))
                 removeClause(cs[i]);
             else
                 cs[j++] = cs[i];
diff --git a/sources/simp/SimpSolver.cc b/sources/simp/SimpSolver.cc
index b2610ec..969167b 100644
--- a/sources/simp/SimpSolver.cc
+++ b/sources/simp/SimpSolver.cc
@@ -626,7 +626,7 @@ void SimpSolver::removeSatisfied()
     for (i = j = 0; i < clauses.size(); i++){
         const Clause& c = ca[clauses[i]];
         if (c.mark() == 0)
-            if (satisfied(c))
+            if (satisfied(c) && !locked(c))
                 removeClause(clauses[i]);
             else
                 clauses[j++] = clauses[i];