diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 2cc1a7f09..09cb063f5 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1070,7 +1070,7 @@ namespace sat {
             for (; !it.at_end(); it.next()) {
                 bool tautology = false;
                 clause & c = it.curr();
-                if (c.is_blocked()) continue;
+                if (c.is_blocked() && !adding) continue;
                 for (literal lit : c) {
                     if (s.is_marked(~lit) && lit != ~l) {
                         tautology = true;
@@ -1322,8 +1322,12 @@ namespace sat {
                 }                
                 if (!found) {
                     IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";);
-                    s.get_wlist(~l).push_back(watched(l2, true));
-                    s.get_wlist(~l2).push_back(watched(l, true));
+                    watched w1(l2, false);
+                    w1.set_blocked();
+                    watched w2(l, false);
+                    w2.set_blocked();
+                    s.get_wlist(~l).push_back(w1);
+                    s.get_wlist(~l2).push_back(w2);
                     ++s.m_num_bca;
                 }
             }
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 5db9d44c6..1f0015476 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1553,8 +1553,10 @@ namespace sat {
 
 // #ifndef _EXTERNAL_RELEASE
         IF_VERBOSE(10, verbose_stream() << "\"checking model\"\n";);
-        if (!check_model(m_model))
+        if (!check_model(m_model)) {
+            UNREACHABLE();
             throw solver_exception("check model failed");
+        }
 
         if (m_clone) {
             IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model (on original set of clauses)\"\n";);
@@ -1576,6 +1578,9 @@ namespace sat {
                       tout << "model: " << m << "\n";
                       m_mc.display(tout);
                       );
+                for (literal l : c) {
+                    if (was_eliminated(l.var())) IF_VERBOSE(0, verbose_stream() << "eliminated: " << l << "\n";);
+                }
                 ok = false;
             }
         }
@@ -1588,7 +1593,7 @@ namespace sat {
                         continue;
                     literal l2 = w.get_literal();
                     if (value_at(l2, m) != l_true) {
-                        IF_VERBOSE(0, verbose_stream() << "failed binary: " << l << " " << l2 << " "  << "\n";);
+                        IF_VERBOSE(0, verbose_stream() << "failed binary: " << l << " " << l2 << "\n";);
                         TRACE("sat", m_mc.display(tout << "failed binary: " << l << " " << l2 << "\n"););
                         ok = false;
                     }