diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-08-23 16:59:41 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2019-08-23 16:59:41 -0500 |
| commit | eaf29fee0871f1b7a8c9cc7c208c6b6d5570bae5 (patch) | |
| tree | 06a70eee6db68dd0cf293e5973133f30947f3a14 /src/theory/quantifiers/quant_split.cpp | |
| parent | c11154240248592b5446f1de4743d78ed2fb97bd (diff) | |
Fixes for sygus regressions (#3219)
Diffstat (limited to 'src/theory/quantifiers/quant_split.cpp')
| -rw-r--r-- | src/theory/quantifiers/quant_split.cpp | 8 |
1 files changed, 8 insertions, 0 deletions
diff --git a/src/theory/quantifiers/quant_split.cpp b/src/theory/quantifiers/quant_split.cpp index 4e9441279..54708f6cb 100644 --- a/src/theory/quantifiers/quant_split.cpp +++ b/src/theory/quantifiers/quant_split.cpp @@ -33,6 +33,14 @@ QuantifiersModule( qe ), d_added_split( qe->getUserContext() ){ void QuantDSplit::checkOwnership(Node q) { + // If q is non-standard (marked as sygus, quantifier elimination, etc.), then + // do no split it. + QAttributes qa; + QuantAttributes::computeQuantAttributes(q, qa); + if (!qa.isStandard()) + { + return; + } int max_index = -1; int max_score = -1; Trace("quant-dsplit-debug") << "Check split quantified formula : " << q << std::endl; |