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

#5778

Browse source
This commit is contained in:
Nikolaj Bjorner 2022-01-16 19:36:00 -08:00
parent a15da8f9ba
commit fcc9f379e7
1 changed files with 9 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/sat/smt/euf_internalize.cpp
View file

@ -167,12 +167,20 @@ namespace euf {
lit = lit2; lit = lit2;
} }
TRACE("euf", tout << "attach " << v << " " << mk_bounded_pp(e, m) << "\n";);
m_bool_var2expr.reserve(v + 1, nullptr); m_bool_var2expr.reserve(v + 1, nullptr);
if (m_bool_var2expr[v] && m_egraph.find(e)) { if (m_bool_var2expr[v] && m_egraph.find(e)) {
if (m_egraph.find(e)->bool_var() != v) {
IF_VERBOSE(0, verbose_stream()
<< "var " << v << "\n"
<< "found var " << m_egraph.find(e)->bool_var() << "\n"
<< mk_pp(m_bool_var2expr[v], m) << "\n"
<< mk_pp(e, m) << "\n");
}
SASSERT(m_egraph.find(e)->bool_var() == v); SASSERT(m_egraph.find(e)->bool_var() == v);
return lit; return lit;
} }
TRACE("euf", tout << "attach " << v << " " << mk_bounded_pp(e, m) << "\n";);
m_bool_var2expr[v] = e; m_bool_var2expr[v] = e;
m_var_trail.push_back(v); m_var_trail.push_back(v);
enode* n = m_egraph.find(e); enode* n = m_egraph.find(e);