diff --git a/src/sat/sat_asymm_branch.cpp b/src/sat/sat_asymm_branch.cpp
index b8ac520b2..193bf59f2 100644
--- a/src/sat/sat_asymm_branch.cpp
+++ b/src/sat/sat_asymm_branch.cpp
@@ -215,7 +215,7 @@ namespace sat {
         sat_asymm_branch_params::collect_param_descrs(d);
     }
     
-    void asymm_branch::collect_statistics(statistics & st) {
+    void asymm_branch::collect_statistics(statistics & st) const {
         st.update("elim literals", m_elim_literals);
     }
 
diff --git a/src/sat/sat_asymm_branch.h b/src/sat/sat_asymm_branch.h
index 6ffd239eb..f10522fab 100644
--- a/src/sat/sat_asymm_branch.h
+++ b/src/sat/sat_asymm_branch.h
@@ -49,7 +49,7 @@ namespace sat {
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
 
-        void collect_statistics(statistics & st);
+        void collect_statistics(statistics & st) const;
         void reset_statistics();
 
         void dec(unsigned c) { m_counter -= c; }
diff --git a/src/sat/sat_cleaner.cpp b/src/sat/sat_cleaner.cpp
index 4b1ac2c92..959f5e94f 100644
--- a/src/sat/sat_cleaner.cpp
+++ b/src/sat/sat_cleaner.cpp
@@ -206,7 +206,7 @@ namespace sat {
         m_elim_literals = 0;
     }
     
-    void cleaner::collect_statistics(statistics & st) {
+    void cleaner::collect_statistics(statistics & st) const {
         st.update("elim clauses", m_elim_clauses);
         st.update("elim literals", m_elim_literals);
     }
diff --git a/src/sat/sat_cleaner.h b/src/sat/sat_cleaner.h
index d4306afcd..d22408926 100644
--- a/src/sat/sat_cleaner.h
+++ b/src/sat/sat_cleaner.h
@@ -42,7 +42,7 @@ namespace sat {
 
         bool operator()(bool force = false);
 
-        void collect_statistics(statistics & st);
+        void collect_statistics(statistics & st) const;
         void reset_statistics();
 
         void dec() { m_cleanup_counter--; }
diff --git a/src/sat/sat_probing.cpp b/src/sat/sat_probing.cpp
index f9741cd7b..165d39ad8 100644
--- a/src/sat/sat_probing.cpp
+++ b/src/sat/sat_probing.cpp
@@ -196,6 +196,7 @@ namespace sat {
         s.propagate(false); // make sure propagation queue is empty
         if (s.inconsistent())
             return true;
+        SASSERT(s.m_qhead == s.m_trail.size());
         CASSERT("probing", s.check_invariant());
         if (!force && m_counter > 0)
             return true;
@@ -259,7 +260,7 @@ namespace sat {
         m_to_assert.finalize();
     }
     
-    void probing::collect_statistics(statistics & st) {
+    void probing::collect_statistics(statistics & st) const {
         st.update("probing assigned", m_num_assigned);
     }
     
diff --git a/src/sat/sat_probing.h b/src/sat/sat_probing.h
index 9f3c1ae87..2061b74bd 100644
--- a/src/sat/sat_probing.h
+++ b/src/sat/sat_probing.h
@@ -71,7 +71,7 @@ namespace sat {
 
         void free_memory();
 
-        void collect_statistics(statistics & st);
+        void collect_statistics(statistics & st) const;
         void reset_statistics();
 
         // return the literals implied by l.
diff --git a/src/sat/sat_scc.cpp b/src/sat/sat_scc.cpp
index 29f3f006f..ffbdb31c6 100644
--- a/src/sat/sat_scc.cpp
+++ b/src/sat/sat_scc.cpp
@@ -223,7 +223,7 @@ namespace sat {
         return to_elim.size();
     }
 
-    void scc::collect_statistics(statistics & st) {
+    void scc::collect_statistics(statistics & st) const {
         st.update("elim bool vars", m_num_elim);
     }
     
diff --git a/src/sat/sat_scc.h b/src/sat/sat_scc.h
index c85cc7d42..5f69e11c6 100644
--- a/src/sat/sat_scc.h
+++ b/src/sat/sat_scc.h
@@ -40,7 +40,7 @@ namespace sat {
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
 
-        void collect_statistics(statistics & st);
+        void collect_statistics(statistics & st) const;
         void reset_statistics();
     };
 };
diff --git a/src/sat/sat_simplifier.cpp b/src/sat/sat_simplifier.cpp
index f20ffa7c7..753075b10 100644
--- a/src/sat/sat_simplifier.cpp
+++ b/src/sat/sat_simplifier.cpp
@@ -918,7 +918,11 @@ namespace sat {
         void process(literal l) {
             TRACE("blocked_clause", tout << "processing: " << l << "\n";);
             model_converter::entry * new_entry = 0;
+            if (s.is_external(l.var()) || s.was_eliminated(l.var())) 
+                return;
+
             {
+
                 m_to_remove.reset();
                 {
                     clause_use_list & occs = s.m_use_list.get(l);
@@ -1339,6 +1343,7 @@ namespace sat {
         }
         TRACE("resolution", tout << "found var to eliminate, before: " << before_clauses << " after: " << after_clauses << "\n";);
 
+        
         // eliminate variable
         model_converter::entry & mc_entry = s.m_mc.mk(model_converter::ELIM_VAR, v);
         save_clauses(mc_entry, m_pos_cls);
@@ -1421,6 +1426,7 @@ namespace sat {
     };
 
     void simplifier::elim_vars() {
+        IF_VERBOSE(10, s.display(verbose_stream()););
         elim_var_report rpt(*this);
         bool_var_vector vars;
         order_vars_for_elim(vars);
@@ -1466,7 +1472,7 @@ namespace sat {
         sat_simplifier_params::collect_param_descrs(r);
     }
 
-    void simplifier::collect_statistics(statistics & st) {
+    void simplifier::collect_statistics(statistics & st) const {
         st.update("subsumed", m_num_subsumed);
         st.update("subsumption resolution", m_num_sub_res);
         st.update("elim literals", m_num_elim_lits);
diff --git a/src/sat/sat_simplifier.h b/src/sat/sat_simplifier.h
index 96d346598..cb6fa9557 100644
--- a/src/sat/sat_simplifier.h
+++ b/src/sat/sat_simplifier.h
@@ -180,7 +180,7 @@ namespace sat {
         
         void free_memory();
 
-        void collect_statistics(statistics & st);
+        void collect_statistics(statistics & st) const;
         void reset_statistics();
     };
 };
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index e7dee83ae..f898130af 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -459,9 +459,6 @@ namespace sat {
     void solver::set_conflict(justification c, literal not_l) {
         if (m_inconsistent)
             return;
-        TRACE("sat_conflict", tout << "conflict\n";);
-        // int * p = 0;
-        // *p = 0;
         m_inconsistent = true;
         m_conflict = c;
         m_not_l    = not_l;
@@ -863,6 +860,7 @@ namespace sat {
         m_next_simplify           = 0;
         m_stopwatch.reset();
         m_stopwatch.start();
+        TRACE("sat", display(tout););
     }
 
     /**
diff --git a/src/util/cmd_context_types.h b/src/util/cmd_context_types.h
index b0a0226e8..e334dc0d2 100644
--- a/src/util/cmd_context_types.h
+++ b/src/util/cmd_context_types.h
@@ -55,12 +55,12 @@ class cmd_exception : public default_exception {
     }
 public:
     cmd_exception(char const * msg):default_exception(msg), m_line(-1), m_pos(-1) {}
-    cmd_exception(std::string const & msg):default_exception(msg.c_str()), m_line(-1), m_pos(-1) {}
-    cmd_exception(std::string const & msg, int line, int pos):default_exception(msg.c_str()), m_line(line), m_pos(pos) {}
+    cmd_exception(std::string const & msg):default_exception(msg), m_line(-1), m_pos(-1) {}
+    cmd_exception(std::string const & msg, int line, int pos):default_exception(msg), m_line(line), m_pos(pos) {}
     cmd_exception(char const * msg, symbol const & s): 
-        default_exception(compose(msg,s).c_str()),m_line(-1),m_pos(-1) {}
+        default_exception(compose(msg,s)),m_line(-1),m_pos(-1) {}
     cmd_exception(char const * msg, symbol const & s, int line, int pos): 
-        default_exception(compose(msg,s).c_str()),m_line(line),m_pos(pos) {}
+        default_exception(compose(msg,s)),m_line(line),m_pos(pos) {}
 
     bool has_pos() const { return m_line >= 0; }
     int line() const { SASSERT(has_pos()); return m_line; }