diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2018-04-08 14:36:20 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-04-08 14:36:20 -0500 |
| commit | 741b11e0a2572e5ddf2e135a11db28154c5face7 (patch) | |
| tree | 01bdbe6c55be84b6446d286fb8d6e3f6af6cfe91 /src/theory/quantifiers/quantifiers_rewriter.cpp | |
| parent | 67d245bfe914ae2594ecad8a9140d468270adf88 (diff) | |
Add quantifier name attribute. (#1756)
Diffstat (limited to 'src/theory/quantifiers/quantifiers_rewriter.cpp')
| -rw-r--r-- | src/theory/quantifiers/quantifiers_rewriter.cpp | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/theory/quantifiers/quantifiers_rewriter.cpp b/src/theory/quantifiers/quantifiers_rewriter.cpp index bc298fa9c..a8089d229 100644 --- a/src/theory/quantifiers/quantifiers_rewriter.cpp +++ b/src/theory/quantifiers/quantifiers_rewriter.cpp @@ -1705,7 +1705,7 @@ Node QuantifiersRewriter::computeAggressiveMiniscoping( std::vector< Node >& arg bool QuantifiersRewriter::doOperation( Node q, int computeOption, QAttributes& qa ){ bool is_strict_trigger = qa.d_hasPattern && options::userPatternsQuant()==USER_PAT_MODE_TRUST; - bool is_std = !qa.d_sygus && !qa.d_quant_elim && !qa.isFunDef() && !is_strict_trigger; + bool is_std = qa.isStandard() && !is_strict_trigger; if (computeOption == COMPUTE_ELIM_SYMBOLS) { return true; |