mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-29 03:45:51 +00:00
Code Activity

#6319

Browse source 
using a queue for disequality propagaiton was a regression: values of numerals can change along the same stack so prior passing the filter does not mean it passes later.
This commit is contained in:
Nikolaj Bjorner 2022-09-23 14:47:48 -05:00
parent 79b4357442
commit c41b6da6bb
2 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

7
src/sat/smt/arith_solver.cpp
View file

@ -1114,12 +1114,11 @@ namespace arith {
bool solver::check_delayed_eqs() {
bool found_diseq = false;
if (m_delayed_eqs_qhead == m_delayed_eqs.size())
if (m_delayed_eqs.empty())
return true;
force_push();
ctx.push(value_trail<unsigned>(m_delayed_eqs_qhead));
for (; m_delayed_eqs_qhead < m_delayed_eqs.size(); ++ m_delayed_eqs_qhead) {
auto p = m_delayed_eqs[m_delayed_eqs_qhead];
for (unsigned i; i < m_delayed_eqs.size(); ++i) {
auto p = m_delayed_eqs[i];
auto const& e = p.first;
if (p.second)
new_eq_eh(e);

1
src/sat/smt/arith_solver.h
View file

@ -218,7 +218,6 @@ namespace arith {
svector<euf::enode_pair> m_equalities; // asserted rows corresponding to equalities.
svector<theory_var> m_definitions; // asserted rows corresponding to definitions
svector<std::pair<euf::th_eq, bool>> m_delayed_eqs;
unsigned m_delayed_eqs_qhead = 0;
literal_vector m_asserted;
expr* m_not_handled{ nullptr };