1 files changed, 5 insertions, 0 deletions
diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 1f42c384f..8803a9df8 100644
--- a/src/theory/quantifiers/extended_rewrite.cpp
+++ b/src/theory/quantifiers/extended_rewrite.cpp
@@ -586,6 +586,11 @@ Node ExtendedRewriter::extendedRewriteAndOr(Node n)
 Node ExtendedRewriter::extendedRewritePullIte(Kind itek, Node n)
 {
   Assert(n.getKind() != ITE);
+  if (n.isClosure())
+  {
+    // don't pull ITE out of quantifiers
+    return n;
+  }
   NodeManager* nm = NodeManager::currentNM();
   TypeNode tn = n.getType();
   std::vector<Node> children;