mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
This commit is contained in:
parent
b5496d823d
commit
e0393f85fa
|
@ -141,8 +141,7 @@ namespace euf {
|
|||
}
|
||||
|
||||
m_bool_var2expr.reserve(v + 1, nullptr);
|
||||
if (m_bool_var2expr[v]) {
|
||||
SASSERT(m_egraph.find(e));
|
||||
if (m_bool_var2expr[v] && m_egraph.find(e)) {
|
||||
SASSERT(m_egraph.find(e)->bool_var() == v);
|
||||
return lit;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue