diff options
Diffstat (limited to 'src/theory')
| -rw-r--r-- | src/theory/quantifiers/relevant_domain.cpp | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/src/theory/quantifiers/relevant_domain.cpp b/src/theory/quantifiers/relevant_domain.cpp index 849e73822..76fe892e8 100644 --- 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 ); |