diff --git a/src/sat/sat_unit_walk.cpp b/src/sat/sat_unit_walk.cpp
index 314c275f3..8c7a6c6f9 100644
--- a/src/sat/sat_unit_walk.cpp
+++ b/src/sat/sat_unit_walk.cpp
@@ -99,6 +99,7 @@ namespace sat {
         while (s.rlimit().inc() && st == l_undef) {
             if (inconsistent() && !m_decisions.empty()) do_pop();
             else if (inconsistent()) st = l_false; 
+            else if (should_restart()) restart();
             else if (should_backjump()) st = do_backjump();
             else st = decide();
         }
@@ -276,9 +277,6 @@ namespace sat {
             init_runs();
             init_phase();
         }
-        if (false && should_restart()) {
-            restart();
-        }
     }
 
     bool unit_walk::should_restart() {
@@ -287,9 +285,7 @@ namespace sat {
             ++m_luby_index;
             return true;
         }
-        else {
-            return false;
-        }
+        return false;        
     }
 
     void unit_walk::restart() {
@@ -328,9 +324,9 @@ namespace sat {
     }
 
     void unit_walk::propagate() {
-        while (m_qhead < m_trail.size() && !inconsistent()) 
-            propagate(choose_literal());            
-        // IF_VERBOSE(1, verbose_stream() << m_trail.size() << " " << inconsistent() << "\n";);
+        while (m_qhead < m_trail.size() && !inconsistent()) {
+            propagate(m_trail[m_qhead++]);         
+        }
     }
 
     std::ostream& unit_walk::display(std::ostream& out) const {
@@ -495,10 +491,6 @@ namespace sat {
                    << ")\n";);        
     }
 
-    literal unit_walk::choose_literal() {
-        return m_trail[m_qhead++];
-    }
-
     void unit_walk::set_conflict(literal l1, literal l2) {
         set_conflict();
     }
diff --git a/src/sat/sat_unit_walk.h b/src/sat/sat_unit_walk.h
index 2aead871f..14588a63c 100644
--- a/src/sat/sat_unit_walk.h
+++ b/src/sat/sat_unit_walk.h
@@ -91,7 +91,6 @@ namespace sat {
         void flip_phase(literal l); 
         void propagate();
         void propagate(literal lit);
-        literal choose_literal();
         void set_conflict(literal l1, literal l2);
         void set_conflict(literal l1, literal l2, literal l3);
         void set_conflict(clause const& c);
diff --git a/src/smt/smt_kernel.cpp b/src/smt/smt_kernel.cpp
index 571032039..adcda3979 100644
--- a/src/smt/smt_kernel.cpp
+++ b/src/smt/smt_kernel.cpp
@@ -156,6 +156,14 @@ namespace smt {
         }
 
         void set_activity(expr* lit, double act) {
+            SASSERT(m().is_bool(lit));
+            m().is_not(lit, lit);
+            if (!m_kernel.b_internalized(lit)) {
+                m_kernel.internalize(lit, false);
+            }
+            if (!m_kernel.b_internalized(lit)) {
+                return;
+            }
             auto v = m_kernel.get_bool_var(lit);
             double old_act = m_kernel.get_activity(v);
             m_kernel.set_activity(v, act);