diff options
Diffstat (limited to 'src/theory/quantifiers/trigger.cpp')
-rw-r--r-- | src/theory/quantifiers/trigger.cpp | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/theory/quantifiers/trigger.cpp b/src/theory/quantifiers/trigger.cpp index 65b976b4a..e953e90b2 100644 --- a/src/theory/quantifiers/trigger.cpp +++ b/src/theory/quantifiers/trigger.cpp @@ -318,6 +318,9 @@ bool Trigger::isSimpleTrigger( Node n ){ return false; } } + if( options::purifyDtTriggers() && n.getKind()==APPLY_SELECTOR_TOTAL ){ + return false; + } return true; }else{ return false; @@ -442,7 +445,7 @@ bool Trigger::isLocalTheoryExt( Node n, std::vector< Node >& vars, std::vector< for( unsigned i=0; i<n.getNumChildren(); i++ ){ if( !isLocalTheoryExt( n[i], vars, patTerms ) ){ return false; - } + } } } return true; |