diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index 8211c4760..0d0e3a682 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -76,12 +76,12 @@ namespace sat {
             s.propagate(false); 
             if (s.m_inconsistent)
                 break;
-            //std::cout << "elim: " << m_elim_literals - elim << "\n";
+            std::cout << "elim: " << m_elim_literals - elim << "\n";
             if (m_elim_literals == elim)
                 break;
         }
-        //std::cout << "elim-literals: " << m_elim_literals - elim0 << "\n";
-        //std::cout << "elim-learned-literals: " << m_elim_learned_literals - eliml0 << "\n";
+        std::cout << "elim-literals: " << m_elim_literals - elim0 << "\n";
+        std::cout << "elim-learned-literals: " << m_elim_learned_literals - eliml0 << "\n";
         return m_elim_literals > elim0;
     }
 
diff --git a/src/sat/sat_integrity_checker.cpp b/src/sat/sat_integrity_checker.cpp
index 03cf00e0b..bdc72602d 100644
--- a/src/sat/sat_integrity_checker.cpp
+++ b/src/sat/sat_integrity_checker.cpp
@@ -155,7 +155,6 @@ namespace sat {
     }
 
     bool integrity_checker::check_watches(literal l, watch_list const& wlist) const {
-        return true;    // TODO: remove
         for (watched const& w : wlist) {
             switch (w.get_kind()) {
             case watched::BINARY:
diff --git a/src/sat/sat_lookahead.cpp b/src/sat/sat_lookahead.cpp
index f3d4a3125..b7694e562 100644
--- a/src/sat/sat_lookahead.cpp
+++ b/src/sat/sat_lookahead.cpp
@@ -2390,7 +2390,7 @@ namespace sat {
                     }
                 }
             }
-            //std::cout << candidates.size() << " -> " << k << "\n";
+            std::cout << candidates.size() << " -> " << k << "\n";
             if (k == candidates.size()) break;
             candidates.shrink(k);
             if (k == 0) break;
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 7010a4536..ce3e5472a 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1360,7 +1360,7 @@ namespace sat {
 
         void prepare_block_clause(clause& c, literal l, model_converter::entry*& new_entry, model_converter::kind k) {
             TRACE("blocked_clause", tout << "new blocked clause: " << c << "\n";);
-            //VERIFY(!s.is_external(l));
+            VERIFY(!s.is_external(l));
             if (new_entry == 0)
                 new_entry = &(mc.mk(k, l.var()));
             m_to_remove.push_back(&c);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index a52ab4c8d..b9d4b0132 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1546,8 +1546,8 @@ namespace sat {
         
         if (!check_clauses(m_model)) {
             IF_VERBOSE(0, verbose_stream() << "failure checking clauses on transformed model\n";);
-            //UNREACHABLE();                                    // TODO: uncomment
-            //throw solver_exception("check model failed");     // TODO: uncomment
+            UNREACHABLE();
+            throw solver_exception("check model failed");
         }
 
         TRACE("sat", for (bool_var v = 0; v < num; v++) tout << v << ": " << m_model[v] << "\n";);