From 0b8dbf28545eaea8820715224b65ea371e892dad Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 12 Jan 2019 00:30:21 -0800
Subject: [PATCH] fixing drat proofs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/sat/sat_drat.cpp       | 7 ++++++-
 src/sat/sat_simplifier.cpp | 9 ++-------
 src/sat/sat_solver.cpp     | 1 -
 3 files changed, 8 insertions(+), 9 deletions(-)

diff --git a/src/sat/sat_drat.cpp b/src/sat/sat_drat.cpp
index ca45bd971..608728002 100644
--- a/src/sat/sat_drat.cpp
+++ b/src/sat/sat_drat.cpp
@@ -68,7 +68,7 @@ namespace sat {
         case status::asserted: return;
         case status::external: return; // requires extension to drat format.
         case status::learned: break;
-        case status::deleted: return; (*m_out) << "d "; break;
+        case status::deleted: (*m_out) << "d "; break;
         }
         for (unsigned i = 0; i < n; ++i) (*m_out) << c[i] << " ";
         (*m_out) << "0\n";
@@ -220,6 +220,7 @@ namespace sat {
                 SASSERT(m_assignment[u.var()] != l_undef);
             });
 
+#if 0
         if (!m_inconsistent) {
             literal_vector lits(n, c);
             IF_VERBOSE(0, verbose_stream() << "not drup " << lits << "\n");
@@ -268,6 +269,8 @@ namespace sat {
             IF_VERBOSE(0, s.display(verbose_stream()));
             exit(0);
         }
+#endif
+
         for (unsigned i = num_units; i < m_units.size(); ++i) {
             m_assignment[m_units[i].var()] = l_undef;
         }
@@ -568,7 +571,9 @@ namespace sat {
         if (m_check) 
             append(l1, l2, status::deleted);
     }
+
     void drat::del(clause& c) {
+
         TRACE("sat", tout << "del: " << c << "\n";);
         if (m_out) dump(c.size(), c.begin(), status::deleted);
         if (m_check) {
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 34f89c3aa..2c5059b18 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -347,22 +347,17 @@ namespace sat {
                 return;                
             case 1:
                 s.assign(c[0], justification());
-                c.restore(sz0);
-                s.del_clause(c);
+                s.del_clause(c, false);
                 break;
             case 2:
                 s.mk_bin_clause(c[0], c[1], c.is_learned());
-                c.restore(sz0);
-                s.del_clause(c, true);
+                s.del_clause(c, false);
                 break;
             default:
                 *it2 = *it;
                 it2++;
                 if (!c.frozen()) {
                     s.attach_clause(c);
-                    if (sz != sz0 && s.m_config.m_drat) {
-                        s.m_drat.add(c, true);
-                    }
                 }
                 break;
             }
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 6f181dcc9..2e4e4c299 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -2382,7 +2382,6 @@ namespace sat {
         while (num_marks > 0);
 
         m_lemma[0] = ~consequent;
-        m_drat.verify(m_lemma.size(), m_lemma.c_ptr());
         learn_lemma_and_backjump();
         return true;
     }