diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index f484dcf1f..e26aa4403 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -308,7 +308,7 @@ namespace smt {
     }
 
     void context::assign_core(literal l, b_justification j, bool decision) {
-        TRACE("assign_core", tout << (decision?"decision: ":"propagating: ") << l << " ";
+        CTRACE("assign_core", l.var() == 1573 || l.var() == 1253, tout << (decision?"decision: ":"propagating: ") << l << " ";
               display_literal_smt2(tout, l); tout << " level: " << m_scope_lvl << "\n";
               display(tout, j););
         m_assigned_literals.push_back(l);
@@ -2066,6 +2066,7 @@ namespace smt {
         while (i != old_lim) {
             --i;
             literal l                  = m_assigned_literals[i];
+            CTRACE("assign_core", l.var() == 1573 || l.var() == 1253, tout << "unassign " << l << "\n";);
             m_assignment[l.index()]    = l_undef;
             m_assignment[(~l).index()] = l_undef;
             bool_var v                 = l.var();
diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp
index ae1cddbf1..e2b751f8e 100644
--- a/src/smt/theory_bv.cpp
+++ b/src/smt/theory_bv.cpp
@@ -1286,7 +1286,7 @@ namespace smt {
                 continue;
             }
             theory_var v2         = next(v);
-            TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << "\n";);
+            TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v)->get_owner_id() << "[" << idx << "] = " << val << " " << ctx.get_scope_level() << "\n";);
             literal antecedent = bit;
 
             if (val == l_false) {
@@ -1298,7 +1298,7 @@ namespace smt {
                 SASSERT(bit != ~bit2);
                 lbool   val2             = ctx.get_assignment(bit2);
                 TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";);
-                TRACE("bv", tout << bit << " " << bit2 << " " << val << " " << val2 << "\n";);
+                TRACE("bv", tout << bit << " -> " << bit2 << " " << val << " -> " << val2 << " " << ctx.get_scope_level() << "\n";);
                 
                 if (val != val2) {
                     literal consequent = bit2;
@@ -1432,7 +1432,6 @@ namespace smt {
     
     void theory_bv::pop_scope_eh(unsigned num_scopes) {
         m_trail_stack.pop_scope(num_scopes);
-        TRACE("bv", m_find.display(tout << num_scopes << " @ " << get_context().get_scope_level() << "\n"););
         unsigned num_old_vars = get_old_num_vars(num_scopes);
         m_bits.shrink(num_old_vars);
         m_wpos.shrink(num_old_vars);
@@ -1448,6 +1447,8 @@ namespace smt {
         m_diseq_watch_lim.shrink(m_diseq_watch_lim.size()-num_scopes);
 #endif
         theory::pop_scope_eh(num_scopes);
+        TRACE("bv", m_find.display(tout << get_context().get_scope_level() << " - " 
+                                   << num_scopes << " = " << (get_context().get_scope_level() - num_scopes) << "\n"););
     }
 
     final_check_status theory_bv::final_check_eh() {
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index c1d941064..0c2f254a0 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1634,6 +1634,9 @@ public:
         if (vars.empty()) {
             return false;
         }
+        if (!m_use_nra_model) {
+            lp().random_update(vars.size(), vars.c_ptr());
+        }
         init_variable_values();
         TRACE("arith", 
               for (theory_var v = 0; v < sz; ++v) {
@@ -1642,9 +1645,6 @@ public:
                   }
               }
               tout << "\n"; );
-        if (!m_use_nra_model) {
-            lp().random_update(vars.size(), vars.c_ptr());
-        }
         m_model_eqs.reset();
         TRACE("arith", display(tout););