From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 17 Jul 2018 17:07:22 +0000 (+0200)
Subject: Do extended rewrite on results of quantifier elimination. (#2119)
X-Git-Tag: cvc5-1.0.0~4888
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=3fc5f5df9a887469cdd9183ca5793578cfb773cb;p=cvc5.git

Do extended rewrite on results of quantifier elimination. (#2119)
---

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