Fix scope issue with pulling ITEs in extended rewriter. (#4547)

Fixes #4476.

diff --git a/src/theory/quantifiers/extended_rewrite.cpp b/src/theory/quantifiers/extended_rewrite.cpp
index 1f42c384fe2b952394d8bf2c5be6ca08ed9ae797..8803a9df89cd430260e09cf9dcda6ba934e050d0 100644 (file)
--- 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;

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2b587c93acd186dea482a135acee0940f97da6a6..b66d4e973ca678c0636b2e08cd4392aea902dea6 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -740,6 +740,7 @@ set(regress_0_tests
   regress0/quantifiers/issue3655.smt2
   regress0/quantifiers/issue4086-infs.smt2
   regress0/quantifiers/issue4275-qcf-cegqi-rep.smt2
+  regress0/quantifiers/issue4476-ext-rew.smt2
   regress0/quantifiers/lra-triv-gn.smt2
   regress0/quantifiers/macros-int-real.smt2
   regress0/quantifiers/macros-real-arg.smt2

diff --git a/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2 b/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2
new file mode 100644 (file)
index 0000000..c54254e
--- /dev/null
+++ b/test/regress/regress0/quantifiers/issue4476-ext-rew.smt2
@@ -0,0 +1,5 @@
+(set-logic NRA)
+(set-info :status sat)
+(set-option :ext-rewrite-quant true)
+(assert (exists ((a Real) (b Real)) (forall ((c Real)) (= (/ b (/ 1 c)) 0))))
+(check-sat)