mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
This commit is contained in:
parent
90fd3d82fc
commit
bf3c213fd3
|
@ -228,12 +228,13 @@ namespace q {
|
|||
}
|
||||
|
||||
bool solver::expand(quantifier* q) {
|
||||
expr_ref r(m);
|
||||
expr_ref r(q, m);
|
||||
proof_ref pr(m);
|
||||
m_der(q, r, pr);
|
||||
ctx.rewrite(r);
|
||||
m_der(r, r, pr);
|
||||
m_expanded.reset();
|
||||
if (r != q) {
|
||||
ctx.get_rewriter()(r);
|
||||
ctx.rewrite(r);
|
||||
m_expanded.push_back(r);
|
||||
return true;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue