New options for trigger selection, add option --strict-triggers. Do not infer alpha equivalence for quantifiers with annotations, limit rewrite operations when triggers are trusted.

1 files changed, 5 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index ddbb9eef7..bff8e187f 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1846,6 +1846,11 @@ void SmtEngine::setDefaults() {
     }
   }
   //implied options...
+  if( options::strictTriggers() ){
+    if( !options::userPatternsQuant.wasSetByUser() ){
+      options::userPatternsQuant.set( quantifiers::USER_PAT_MODE_TRUST );
+    }
+  }
   if( options::qcfMode.wasSetByUser() || options::qcfTConstraint() ){
     options::quantConflictFind.set( true );
   }