Add misc trigger options.

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;