diff --git a/src/opt/maxcore.cpp b/src/opt/maxcore.cpp
index c71a7944e..fc3ad1b91 100644
--- a/src/opt/maxcore.cpp
+++ b/src/opt/maxcore.cpp
@@ -169,6 +169,12 @@ public:
         case s_primal_binary_delay:
             m_trace_id = "maxres-bin-delay";
             break;
+        case s_rc2:
+            m_trace_id = "rc2";
+            break;
+        default:
+            UNREACHABLE();
+            break;
         }        
     }
 
@@ -371,6 +377,7 @@ public:
         case s_primal:
         case s_primal_binary:
         case s_primal_binary_delay:
+        case s_rc2:
             return mus_solver();
         case s_primal_dual:
             return primal_dual_solver();
diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 5f2d4a50e..5675c204c 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -669,8 +669,11 @@ namespace q {
         if (m_inst_queue.lazy_propagate())
             return true;
         for (unsigned i = 0; i < m_clauses.size(); ++i)
-            if (m_clauses[i]->m_bindings)
+            if (m_clauses[i]->m_bindings) {
                 IF_VERBOSE(0, verbose_stream() << "missed propagation " << i << "\n");
+                TRACE("q", display(tout));
+                break;
+            }
         
         TRACE("q", tout << "no more propagation\n";);
         return false;
diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp
index d852d9383..d246dc06f 100644
--- a/src/solver/assertions/asserted_formulas.cpp
+++ b/src/solver/assertions/asserted_formulas.cpp
@@ -190,10 +190,11 @@ void asserted_formulas::push_scope() {
 }
 
 void asserted_formulas::push_scope_core() {
+    std::cout << "push\n";
     reduce();
     commit();
     SASSERT(inconsistent() || m_qhead == m_formulas.size() || m.limit().is_canceled());
-    TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n";);
+    TRACE("asserted_formulas_scopes", tout << "before push: " << m_scopes.size() << "\n");
     m_scoped_substitution.push();
     m_scopes.push_back(scope());
     scope & s = m_scopes.back();
@@ -205,7 +206,7 @@ void asserted_formulas::push_scope_core() {
     m_bv_sharing.push_scope();
     m_macro_manager.push_scope();
     commit();
-    TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n";);
+    TRACE("asserted_formulas_scopes", tout << "after push: " << m_scopes.size() << "\n");
 }
 
 void asserted_formulas::force_push() {
@@ -260,6 +261,7 @@ bool asserted_formulas::check_well_sorted() const {
 }
 
 void asserted_formulas::reduce() {
+    std::cout << "reduce\n";
     if (inconsistent())
         return;
     if (canceled())