diff --git a/src/sat/sat_elim_vars.cpp b/src/sat/sat_elim_vars.cpp
index 7e803eaa5..584433cc1 100644
--- a/src/sat/sat_elim_vars.cpp
+++ b/src/sat/sat_elim_vars.cpp
@@ -87,7 +87,7 @@ namespace sat{
         simp.m_neg_cls.reset();
         simp.collect_clauses(pos_l, simp.m_pos_cls, false);
         simp.collect_clauses(neg_l, simp.m_neg_cls, false);
-        VERIFY(!s.is_external(v));
+        //VERIFY(!s.is_external(v));
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
         simp.save_clauses(mc_entry, simp.m_pos_cls);
         simp.save_clauses(mc_entry, simp.m_neg_cls);
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index 674ee9121..6ceb53265 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -1356,7 +1356,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);
@@ -1382,7 +1382,7 @@ namespace sat {
         
         void prepare_block_binary(watch_list::iterator it, literal l1, literal blocked, model_converter::entry*& new_entry, model_converter::kind k) {
             SASSERT(!s.is_external(blocked));
-            VERIFY(!s.is_external(blocked));
+            //VERIFY(!s.is_external(blocked));
             if (new_entry == 0) 
                 new_entry = &(mc.mk(k, blocked.var()));
             literal l2 = it->get_literal();
@@ -1782,7 +1782,7 @@ namespace sat {
 
         // eliminate variable
         ++s.m_stats.m_elim_var_res;
-        VERIFY(!is_external(v));
+        //VERIFY(!is_external(v));
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
         save_clauses(mc_entry, m_pos_cls);
         save_clauses(mc_entry, m_neg_cls);
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index d4a57a9b1..03f56a497 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -1331,7 +1331,7 @@ namespace sat {
     void solver::add_assumption(literal lit) {
         m_assumption_set.insert(lit);
         m_assumptions.push_back(lit);
-        VERIFY(is_external(lit.var()));
+        set_external(lit.var());
     }
 
     void solver::pop_assumption() {
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 2af846f42..6802b7373 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -94,7 +94,7 @@ public:
 
     bool override_incremental() const {
         sat_simplifier_params p(m_params);
-        std::cout << "override: " << p.override_incremental() << "\n";
+        //std::cout << "override: " << p.override_incremental() << "\n";
         return p.override_incremental();
     }