diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-03-14 15:47:48 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-03-14 15:47:48 -0500 |
| commit | d4046f5e2e32d07c34b65fbcdfffae6a24d8c399 (patch) | |
| tree | 540ed4261b428b7e34ec32ed8652c07a062c7457 /src/theory/quantifiers | |
| parent | 7247f321dc8d319c5079b31d450c09029506274a (diff) | |
Properly handle lambdas in relevant domain (#2853)
Diffstat (limited to 'src/theory/quantifiers')
| -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 ); |