diff options
| -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() |