mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
This commit is contained in:
parent
9011100df2
commit
4b1419261f
|
@ -262,6 +262,8 @@ namespace q {
|
||||||
m_expanded.push_back(r);
|
m_expanded.push_back(r);
|
||||||
return true;
|
return true;
|
||||||
}
|
}
|
||||||
|
if (r == q)
|
||||||
|
return false;
|
||||||
q = to_quantifier(r);
|
q = to_quantifier(r);
|
||||||
}
|
}
|
||||||
if (is_forall(q))
|
if (is_forall(q))
|
||||||
|
|
Loading…
Reference in a new issue