From a7bc4719c08f300f6c08367ec9175344a8d5df3b Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 1 Sep 2021 11:45:21 -0700 Subject: [PATCH] fix #5526 when propagation claims progress, but is a no-op. --- src/solver/assertions/asserted_formulas.cpp | 9 ++++++--- 1 file changed, 6 insertions(+), 3 deletions(-) diff --git a/src/solver/assertions/asserted_formulas.cpp b/src/solver/assertions/asserted_formulas.cpp index be931ccd6..9e9b54140 100644 --- a/src/solver/assertions/asserted_formulas.cpp +++ b/src/solver/assertions/asserted_formulas.cpp @@ -532,14 +532,14 @@ void asserted_formulas::propagate_values() { flush_cache(); unsigned num_prop = 0; - unsigned delta_prop = m_formulas.size(); - while (!inconsistent() && m_formulas.size()/20 < delta_prop) { + unsigned sz = m_formulas.size(); + unsigned delta_prop = sz; + while (!inconsistent() && sz/20 < delta_prop) { m_expr2depth.reset(); m_scoped_substitution.push(); unsigned prop = num_prop; TRACE("propagate_values", display(tout << "before:\n");); unsigned i = m_qhead; - unsigned sz = m_formulas.size(); for (; i < sz; i++) { prop += propagate_values(i); } @@ -558,6 +558,9 @@ void asserted_formulas::propagate_values() { TRACE("propagate_values", tout << "after:\n"; display(tout);); delta_prop = prop - num_prop; num_prop = prop; + if (sz <= m_formulas.size()) + break; + sz = m_formulas.size(); } TRACE("asserted_formulas", tout << num_prop << "\n";); if (num_prop > 0)