mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
fix compilation
This commit is contained in:
parent
96d815b904
commit
b3ebce3966
|
@ -72,9 +72,7 @@ namespace euf {
|
||||||
return true;
|
return true;
|
||||||
if (is_uninterp_const(e))
|
if (is_uninterp_const(e))
|
||||||
return true;
|
return true;
|
||||||
euf::enode* n = m_egraph.find(e);
|
return !m_egraph.find(e);
|
||||||
if (!n)
|
|
||||||
return true;
|
|
||||||
}
|
}
|
||||||
|
|
||||||
void solver::setup_bounds(sat::model const& mdl) {
|
void solver::setup_bounds(sat::model const& mdl) {
|
||||||
|
|
Loading…
Reference in a new issue