merge

1 files changed, 5 insertions, 3 deletions

diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp
index 849e73822..071bd7933 100644
--- a/src/theory/quantifiers/relevant_domain.cpp
+++ b/src/theory/quantifiers/relevant_domain.cpp
@@ -2,9 +2,9 @@
 /*! \file relevant_domain.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andrew Reynolds
+ **   Andrew Reynolds, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -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 );