Properly handle lambdas in relevant domain (#2853)

diff --git a/src/expr/node.h b/src/expr/node.h
index 750a5547b1a3009b812d88038da12958511efa5f..50add7b1779a30c89676a33935c37cd6ed11db8d 100644 (file)
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -470,10 +470,9 @@ public:
   
   inline bool isClosure() const {
     assertTNodeNotExpired();
-    return getKind() == kind::LAMBDA ||
-           getKind() == kind::FORALL ||
-           getKind() == kind::EXISTS ||
-           getKind() == kind::REWRITE_RULE;
+    return getKind() == kind::LAMBDA || getKind() == kind::FORALL
+           || getKind() == kind::EXISTS || getKind() == kind::REWRITE_RULE
+           || getKind() == kind::CHOICE;
   }
 
   /**

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 849e73822ed0cab02376efea7343974b7363d6ed..76fe892e8f25eed1690b06eb75413561d00c55fb 100644 (file)
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -169,7 +169,9 @@ void RelevantDomain::computeRelevantDomain( Node q, Node n, bool hasPol, bool po
         computeRelevantDomainOpCh( rf, n[i] );
       }
     }
-    if( n[i].getKind()!=FORALL ){
+    // do not recurse under nested closures
+    if (!n[i].isClosure())
+    {
       bool newHasPol;
       bool newPol;
       QuantPhaseReq::getPolarity( n, i, hasPol, pol, newHasPol, newPol );