From 1918395f0eabad5038d8a97f2fe16855a27c4fa9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 5 Jul 2018 12:19:03 -0700
Subject: [PATCH] fix bug in sat-solver where frozen clauses get re-attached

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

diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index a59dd2b46..04a0274c4 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -17,6 +17,7 @@ Revision History:
 
 --*/
 
+
 #include <cmath>
 #include "sat/sat_solver.h"
 #include "sat/sat_integrity_checker.h"
@@ -298,6 +299,9 @@ namespace sat {
         if (!c.is_learned()) {
             m_stats.m_non_learned_generation++;
         } 
+        if (c.frozen()) {
+            --m_num_frozen;
+        }
         if (m_config.m_drat && !m_drat.is_cleaned(c)) {
             m_drat.del(c);
         }
@@ -481,9 +485,10 @@ namespace sat {
         }
         unsigned some_idx = c.size() >> 1;
         literal block_lit = c[some_idx];
-        DEBUG_CODE(for (auto const& w : m_watches[(~c[0]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off););
-        DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) VERIFY(!w.is_clause() || w.get_clause_offset() != cls_off););
-        VERIFY(c[0] != c[1]);
+        VERIFY(!c.frozen());
+        DEBUG_CODE(for (auto const& w : m_watches[(~c[0]).index()]) SASSERT(!w.is_clause() || w.get_clause_offset() != cls_off););
+        DEBUG_CODE(for (auto const& w : m_watches[(~c[1]).index()]) SASSERT(!w.is_clause() || w.get_clause_offset() != cls_off););
+        SASSERT(c[0] != c[1]);
         m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off));
         m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off));
         return reinit;
@@ -2139,7 +2144,6 @@ namespace sat {
                 else {
                     c.inc_inact_rounds();
                     if (c.inact_rounds() > m_config.m_gc_k) {
-                        m_num_frozen--;
                         del_clause(c);
                         m_stats.m_gc_clause++;
                         deleted++;
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index b44c04604..ad972b2af 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -682,10 +682,10 @@ namespace sat {
         bool m_deleted;
     public:
         scoped_detach(solver& s, clause& c): s(s), c(c), m_deleted(false) {
-            s.detach_clause(c);
+            if (!c.frozen()) s.detach_clause(c);
         }            
         ~scoped_detach() {
-            if (!m_deleted) s.attach_clause(c);
+            if (!m_deleted && !c.frozen()) s.attach_clause(c);
         }
         
         void del_clause() {