From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 2 Jun 2020 20:55:49 +0000 (-0500)
Subject: Fix scope issue with pulling ITEs in extended rewriter. (#4547)
X-Git-Tag: cvc5-1.0.0~3271
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=6ae4eda75d5717543f7c847d4b2f58ccbbb611bf;p=cvc5.git

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 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;
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 2b587c93a..b66d4e973 100644
--- 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
index 000000000..c54254e67
--- /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)