From e623f1e9c950c79fd85d783c8a16a0660ea56ccd Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 12 Jan 2019 01:01:49 -0800
Subject: [PATCH] restoring clause sizes after deletion

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/ba_solver.cpp      |  2 +-
 src/sat/sat_simplifier.cpp | 12 +++++-------
 2 files changed, 6 insertions(+), 8 deletions(-)

diff --git a/src/sat/ba_solver.cpp b/src/sat/ba_solver.cpp
index b1502d98e..47fc2c27f 100644
--- a/src/sat/ba_solver.cpp
+++ b/src/sat/ba_solver.cpp
@@ -1065,7 +1065,7 @@ namespace sat {
 
     uint64_t ba_solver::get_coeff(literal lit) const {
         int64_t c1 = get_coeff(lit.var());
-        SASSERT(c1 < 0 == lit.sign());
+        SASSERT((c1 < 0) == lit.sign());
         int64_t c = std::abs(c1);
         m_overflow |= (c != c1);
         return static_cast<uint64_t>(c);
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 2c5059b18..f0b024817 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -351,7 +351,8 @@ namespace sat {
                 break;
             case 2:
                 s.mk_bin_clause(c[0], c[1], c.is_learned());
-                s.del_clause(c, false);
+                c.restore(sz0);
+                s.del_clause(c, true);
                 break;
             default:
                 *it2 = *it;
@@ -613,13 +614,9 @@ namespace sat {
             }
         }
         if (j < sz && !r) {
-            if (s.m_config.m_drat) {
-                m_dummy.set(c.size(), c.begin(), c.is_learned());
-            }
             c.shrink(j);
             if (s.m_config.m_drat) {
                 s.m_drat.add(c, true);
-                s.m_drat.del(*m_dummy.get());
             }
         }
         return r;
@@ -692,6 +689,7 @@ namespace sat {
         clause_use_list & occurs = m_use_list.get(l);
         occurs.erase_not_removed(c);
         m_sub_counter -= occurs.size()/2;
+        unsigned sz0 = c.size();
         if (cleanup_clause(c, true /* clause is in the use lists */)) {
             // clause was satisfied
             TRACE("elim_lit", tout << "clause was satisfied\n";);
@@ -707,12 +705,12 @@ namespace sat {
             TRACE("elim_lit", tout << "clause became unit: " << c[0] << "\n";);
             propagate_unit(c[0]);
             // propagate_unit will delete c.
-            // remove_clause(c);
             break;
         case 2:
             TRACE("elim_lit", tout << "clause became binary: " << c[0] << " " << c[1] << "\n";);
             s.mk_bin_clause(c[0], c[1], c.is_learned());
-            m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned()));
+            m_sub_bin_todo.push_back(bin_clause(c[0], c[1], c.is_learned()));            
+            c.restore(sz0);
             remove_clause(c);
             break;
         default: