From eaf845c2f48f6c2bed0264ea75bd4f9e53973bae Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 7 Feb 2017 18:04:24 -0800
Subject: [PATCH] updates

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

diff --git a/src/sat/card_extension.cpp b/src/sat/card_extension.cpp
index 546a6905d..cd7271811 100644
--- a/src/sat/card_extension.cpp
+++ b/src/sat/card_extension.cpp
@@ -120,9 +120,8 @@ namespace sat {
             return;
         }
         ptr_vector<card>*& cards = m_var_infos[lit.var()].m_lit_watch[lit.sign()];
-        if (cards) {
+        if (!is_tag_empty(cards)) {
             if (remove(*cards, c)) {
-                std::cout << "Empty: " << cards->empty() << "\n";
                 cards = set_tag_empty(cards);
             }        
         }
@@ -291,6 +290,7 @@ namespace sat {
         unsigned num_steps = 0;
         DEBUG_CODE(active2pb(m_A););
 
+        std::cout << m_num_marks << "\n";
         do {
 
             if (offset == 0) {
@@ -298,6 +298,7 @@ namespace sat {
             }
             // TBD: need proper check for overflow.
             if (offset > (1 << 12)) {
+                std::cout << "Offset: " << offset << "\n";
                 goto bail_out;
             }
 
@@ -386,6 +387,9 @@ namespace sat {
                 consequent = lits[idx];
                 v = consequent.var();
                 if (s().is_marked(v)) break;
+                if (idx == 0) {
+                    goto bail_out;
+                }
                 SASSERT(idx > 0);
                 --idx;
             }
@@ -481,7 +485,8 @@ namespace sat {
         return true;
 
     bail_out:
-        while (m_num_marks > 0 && idx > 0) {
+        std::cout << "bail num marks: " << m_num_marks << " idx: " << idx << "\n";
+        while (m_num_marks > 0 && idx >= 0) {
             bool_var v = lits[idx].var();
             if (s().is_marked(v)) {
                 s().reset_mark(v);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 73829c6b8..f5f9de6fc 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -371,6 +371,7 @@ namespace sat {
         if (m_watches.size() <= (~c[1]).index()) std::cout << c << "\n";
         if (m_watches[(~c[0]).index()].size() >= 20000) {
             std::cout << m_par_id << ": " << c << "\n";
+            enable_trace("sat");
         }
         m_watches[(~c[0]).index()].push_back(watched(block_lit, cls_off));
         m_watches[(~c[1]).index()].push_back(watched(block_lit, cls_off));