mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 18:05:21 +00:00
Code Activity

fix #5526

Browse source 
when propagation claims progress, but is a no-op.
This commit is contained in:
Nikolaj Bjorner 2021-09-01 11:45:21 -07:00
parent 8bdc8d0e1a
commit a7bc4719c0
1 changed files with 6 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/solver/assertions/asserted_formulas.cpp
View file

@ -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)