From 3fc5f5df9a887469cdd9183ca5793578cfb773cb Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 17 Jul 2018 19:07:22 +0200 Subject: [PATCH] Do extended rewrite on results of quantifier elimination. (#2119) --- src/smt/smt_engine.cpp | 3 +++ 1 file changed, 3 insertions(+) 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() -- 2.30.2