From 0a665b0fa0b6d6f99607992e7f7bc769dd54fab2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 25 Apr 2022 14:27:38 +0100 Subject: [PATCH] #5778 --- src/sat/smt/q_ematch.cpp | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/sat/smt/q_ematch.cpp b/src/sat/smt/q_ematch.cpp index 57841fcbc..29db324f9 100644 --- a/src/sat/smt/q_ematch.cpp +++ b/src/sat/smt/q_ematch.cpp @@ -640,14 +640,13 @@ namespace q { bool ematch::propagate(bool flush) { m_mam->propagate(); bool propagated = flush_prop_queue(); - if (!flush && m_qhead >= m_clause_queue.size()) - return m_inst_queue.propagate() || propagated; - if (flush) { for (auto* c : m_clauses) propagate(*c, flush, propagated); } else { + if (m_qhead >= m_clause_queue.size()) + return m_inst_queue.propagate() || propagated; ctx.push(value_trail(m_qhead)); for (; m_qhead < m_clause_queue.size() && m.inc(); ++m_qhead) { unsigned idx = m_clause_queue[m_qhead];