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

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5d9f083431a4d14f9dd1a9f67fba213caabf7887..69c0dab9c99d86d52bb6b872f513bf01b4deec64 100644 (file)
--- 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()