mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 20:18:18 +00:00
Update solve_eqs.cpp
This commit is contained in:
parent
6c12aaad74
commit
d8133a47c2
|
@ -76,7 +76,6 @@ namespace euf {
|
||||||
};
|
};
|
||||||
|
|
||||||
auto is_safe = [&](unsigned lvl, expr* t) {
|
auto is_safe = [&](unsigned lvl, expr* t) {
|
||||||
for (auto* e : subterms::all(expr_ref(t, m)))
|
|
||||||
for (auto* e : subterms::all(expr_ref(t, m), &m_todo, &m_visited))
|
for (auto* e : subterms::all(expr_ref(t, m), &m_todo, &m_visited))
|
||||||
if (is_var(e) && m_id2level[var2id(e)] < lvl)
|
if (is_var(e) && m_id2level[var2id(e)] < lvl)
|
||||||
return false;
|
return false;
|
||||||
|
|
Loading…
Reference in a new issue