diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp
index 6040c4b4b..99282bf30 100644
--- a/src/sat/smt/q_ematch.cpp
+++ b/src/sat/smt/q_ematch.cpp
@@ -275,16 +275,34 @@ namespace q {
 
         auto j_idx = mk_justification(idx, c, binding);     
 
-        if (ev == l_false) {
+        if (is_owned)
+            propagate(ev == l_false, idx, j_idx);
+        else
+            m_prop_queue.push_back(prop(ev == l_false, idx, j_idx));
+        propagated = true;
+        return true;
+    }
+
+    void ematch::propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx) {
+        if (is_conflict) {
             ++m_stats.m_num_conflicts;
             ctx.set_conflict(j_idx);
         }
         else {
             ++m_stats.m_num_propagations;
-            auto lit = instantiate(c, binding, c[idx]);
-            ctx.propagate(lit, j_idx);            
+            auto& j = justification::from_index(j_idx);
+            auto lit = instantiate(j.m_clause, j.m_binding, j.m_clause[idx]);
+            ctx.propagate(lit, j_idx);
+        }
+    }
+
+    bool ematch::flush_prop_queue() {
+        if (m_prop_queue.empty())
+            return false;
+        for (unsigned i = 0; i < m_prop_queue.size(); ++i) {
+            auto [is_conflict, idx, j_idx] = m_prop_queue[i];
+            propagate(is_conflict, idx, j_idx);
         }
-        propagated = true;
         return true;
     }
 
@@ -508,7 +526,7 @@ namespace q {
 
     bool ematch::propagate(bool flush) {
         m_mam->propagate();
-        bool propagated = false;
+        bool propagated = flush_prop_queue();
         if (m_qhead >= m_clause_queue.size())
             return m_inst_queue.propagate();
         ctx.push(value_trail<unsigned>(m_qhead));
diff --git a/src/sat/smt/q_ematch.h b/src/sat/smt/q_ematch.h
index 0f8add4c1..9c4cf9d98 100644
--- a/src/sat/smt/q_ematch.h
+++ b/src/sat/smt/q_ematch.h
@@ -49,6 +49,13 @@ namespace q {
             }
         };
 
+        struct prop {
+            bool is_conflict;
+            unsigned idx;
+            sat::ext_justification_idx j;
+            prop(bool is_conflict, unsigned idx, sat::ext_justification_idx j) : is_conflict(is_conflict), idx(idx), j(j) {}
+        };
+
         struct remove_binding;
         struct insert_binding;
         struct pop_clause;
@@ -65,6 +72,7 @@ namespace q {
         scoped_ptr<binding>           m_tmp_binding;
         unsigned                      m_tmp_binding_capacity = 0;
         queue                         m_inst_queue;
+        svector<prop>                 m_prop_queue;
         pattern_inference_rw          m_infer_patterns;
         scoped_ptr<q::mam>            m_mam, m_lazy_mam;
         ptr_vector<clause>            m_clauses;
@@ -108,6 +116,9 @@ namespace q {
         fingerprint* add_fingerprint(clause& c, binding& b, unsigned max_generation);
         void set_tmp_binding(fingerprint& fp);
 
+        bool flush_prop_queue();
+        void propagate(bool is_conflict, unsigned idx, sat::ext_justification_idx j_idx);
+
     public:
         
         ematch(euf::solver& ctx, solver& s);