mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 19:05:51 +00:00
Code Activity

fix #6451 missing occurrence marking when there is an unsafe equality already

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2022-11-14 19:23:27 -08:00
parent 95e07ffe8e
commit 3eeb59db34
2 changed files with 10 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

11
src/ast/simplifiers/solve_context_eqs.cpp
View file

@ -154,10 +154,12 @@ namespace euf {
return e1.var->get_id() < e2.var->get_id(); });
unsigned j = 0;
expr* last_var = nullptr;
bool was_unsafe = false;
for (auto const& eq : eqs) {
SASSERT(!m.is_bool(eq.var));
if (eq.var != last_var) {
m_contains_v.reset();
@ -167,8 +169,11 @@ namespace euf {
mark_occurs(m_todo, eq.var, m_contains_v);
SASSERT(m_todo.empty());
last_var = eq.var;
if (m_contains_v.is_marked(eq.term))
was_unsafe = false;
if (m_contains_v.is_marked(eq.term)) {
was_unsafe = true;
continue;
}
// then mark occurrences
for (unsigned i = 0; i < m_fmls.size(); ++i)
@ -178,7 +183,9 @@ namespace euf {
}
else if (m_contains_v.is_marked(eq.term))
continue;
else if (was_unsafe)
continue;
// subject to occurrences, check if equality is safe
if (is_safe_eq(eq.orig))
eqs[j++] = eq;

2
src/ast/simplifiers/solve_eqs.cpp
View file

@ -197,7 +197,7 @@ namespace euf {
if (!m.inc())
return;
if (m_config.m_context_solve && false) {
if (m_config.m_context_solve) {
old_fmls.reset();
m_subst_ids.reset();
eqs.reset();