diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 6f200680a..942c070fd 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -236,9 +236,10 @@ namespace q {
     }
 
     binding* ematch::alloc_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top) {
+
         binding* b = tmp_binding(c, pat, _binding);
 
-        if (m_bindings.contains(b))
+        if (m_bindings.contains(b)) 
             return nullptr;
 
         for (unsigned i = c.num_decls(); i-- > 0; )
@@ -260,12 +261,12 @@ namespace q {
         return b;
     }
 
-    euf::enode* const* ematch::alloc_nodes(clause& c, euf::enode* const* _binding) {
+    euf::enode* const* ematch::copy_nodes(clause& c, euf::enode* const* nodes) {
         unsigned sz = sizeof(euf::enode* const*) * c.num_decls();
-        euf::enode** binding = (euf::enode**)ctx.get_region().allocate(sz);
+        euf::enode** new_nodes = (euf::enode**)ctx.get_region().allocate(sz);
         for (unsigned i = 0; i < c.num_decls(); ++i)
-            binding[i] = _binding[i];
-        return binding;
+            new_nodes[i] = nodes[i];
+        return new_nodes;
     }
 
     void ematch::on_binding(quantifier* q, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_gen, unsigned max_gen) {
@@ -277,7 +278,7 @@ namespace q {
         if (!b)
             return;
 
-        if (propagate(false, _binding, max_generation, c, new_propagation))
+        if (false && propagate(false, _binding, max_generation, c, new_propagation))
             return;
 
         binding::push_to_front(c.m_bindings, b);
@@ -305,7 +306,7 @@ namespace q {
         if (ev == l_undef && max_generation > m_generation_propagation_threshold)
             return false;
         if (!is_owned) 
-            binding = alloc_nodes(c, binding); 
+            binding = copy_nodes(c, binding); 
 
         auto j_idx = mk_justification(idx, c, binding);     
 
@@ -568,7 +569,7 @@ namespace q {
                 continue;
 
             do {                
-                if (propagate(true, b->m_nodes, b->m_max_generation, c, propagated)) 
+                if (false && propagate(true, b->m_nodes, b->m_max_generation, c, propagated)) 
                     to_remove.push_back(b);
                 else if (flush) {
                     instantiate(*b);
@@ -613,6 +614,7 @@ namespace q {
         for (unsigned i = 0; i < m_clauses.size(); ++i)
             if (m_clauses[i]->m_bindings)
                 std::cout << "missed propagation " << i << "\n";
+
         TRACE("q", tout << "no more propagation\n";);
         return false;
     }
diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h
index bd79511a8..58037e308 100644
--- a/src/sat/smt/q_ematch.h
+++ b/src/sat/smt/q_ematch.h
@@ -89,7 +89,7 @@ namespace q {
         unsigned_vector               m_clause_queue;
         euf::enode_pair_vector        m_evidence;
 
-        euf::enode* const* alloc_nodes(clause& c, euf::enode* const* _binding);
+        euf::enode* const* copy_nodes(clause& c, euf::enode* const* _binding);
         binding* tmp_binding(clause& c, app* pat, euf::enode* const* _binding);
         binding* alloc_binding(clause& c, app* pat, euf::enode* const* _binding, unsigned max_generation, unsigned min_top, unsigned max_top);
         
@@ -127,7 +127,6 @@ namespace q {
 
         bool unit_propagate();        
 
-        // void init_search();
 
         void add(quantifier* q);
 
diff --git a/src/sat/smt/q_queue.cpp b/src/sat/smt/q_queue.cpp
index 2e8db482f..c534c9f80 100644
--- a/src/sat/smt/q_queue.cpp
+++ b/src/sat/smt/q_queue.cpp
@@ -146,7 +146,7 @@ namespace q {
                 
         unsigned gen = get_new_gen(f, ent.m_cost);
         bool new_propagation = false;
-        if (em.propagate(true, f.nodes(), gen, *f.c, new_propagation))
+        if (false && em.propagate(true, f.nodes(), gen, *f.c, new_propagation))
             return;
 
         auto* ebindings = m_subst(q, num_bindings);
@@ -223,15 +223,14 @@ namespace q {
             }
         }
         bool instantiated = false;
-        unsigned idx = 0;
-        for (entry & e : m_delayed_entries) {
+        for (unsigned idx = 0; idx < m_delayed_entries.size(); ++idx) {
+            entry & e = m_delayed_entries[idx];
             if (!e.m_instantiated && e.m_cost <= cost_limit) {
                 instantiated = true;
                 ctx.push(reset_instantiated(*this, idx));
                 m_stats.m_num_lazy_instances++;
                 instantiate(e);
             }
-            ++idx;
         }
         return instantiated;
     }