mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
This commit is contained in:
parent
fcc9f379e7
commit
d777306bb6
|
@ -3531,7 +3531,7 @@ namespace sat {
|
|||
|
||||
for (unsigned i = old_num_vars; i < sz; ++i) {
|
||||
bool_var v = m_active_vars[i];
|
||||
if (is_visited(v) || is_active(v)) {
|
||||
if (is_external(v) || is_visited(v) || is_active(v)) {
|
||||
m_vars_to_reinit.push_back(v);
|
||||
m_active_vars[j++] = v;
|
||||
m_var_scope[v] = new_lvl;
|
||||
|
|
|
@ -182,11 +182,10 @@ namespace euf {
|
|||
}
|
||||
|
||||
m_bool_var2expr[v] = e;
|
||||
m_var_trail.push_back(v);
|
||||
m_var_trail.push_back(v);
|
||||
enode* n = m_egraph.find(e);
|
||||
if (!n) {
|
||||
if (!n)
|
||||
n = mk_enode(e, 0, nullptr);
|
||||
}
|
||||
SASSERT(n->bool_var() == sat::null_bool_var || n->bool_var() == v);
|
||||
m_egraph.set_bool_var(n, v);
|
||||
if (m.is_eq(e) || m.is_or(e) || m.is_and(e) || m.is_not(e))
|
||||
|
|
Loading…
Reference in a new issue