diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-07-17 19:07:22 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-07-17 19:07:22 +0200 |
| commit | 3fc5f5df9a887469cdd9183ca5793578cfb773cb (patch) | |
| tree | b7d4dec8f62ac5fb69f5563ab688ec75c60e9997 | |
| parent | 490f664c35d717d5bd01f43f3026fb2abf3e99ff (diff) | |
Do extended rewrite on results of quantifier elimination. (#2119)
| -rw-r--r-- | src/smt/smt_engine.cpp | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 5d9f08343..69c0dab9c 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -5743,6 +5743,9 @@ Expr SmtEngine::doQuantifierElimination(const Expr& e, bool doFull, bool strict) }else{ ret_n = NodeManager::currentNM()->mkConst(n_e.getKind() != kind::EXISTS); } + // do extended rewrite to minimize the size of the formula aggressively + theory::quantifiers::ExtendedRewriter extr(true); + ret_n = extr.extendedRewrite(ret_n); return ret_n.toExpr(); }else { return NodeManager::currentNM() |