From 3cec3fc63dd2e41e72fba19235bd5682b3c6e76c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 4 Feb 2024 15:26:17 -0800 Subject: [PATCH] bypass replaying new clause within propagation Signed-off-by: Nikolaj Bjorner --- src/smt/theory_user_propagator.cpp | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 395be3e68..93faf9e4e 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -345,6 +345,9 @@ void theory_user_propagator::propagate_consequence(prop_info const& prop) { for (auto lit : m_lits) clause.push_back(ctx.literal2expr(lit)); m_clauses_to_replay.push_back(clause); + if (m_replay_qhead + 1 < m_clauses_to_replay.size()) + std::swap(m_clauses_to_replay[m_replay_qhead], m_clauses_to_replay[m_clauses_to_replay.size()-1]); + ++m_replay_qhead; } else { ctx.mk_th_lemma(get_id(), m_lits);