From 576d50ac7c13233a589771401537b587eb36361e Mon Sep 17 00:00:00 2001 From: ajreynol Date: Mon, 4 Apr 2016 17:18:36 -0500 Subject: 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. --- src/smt/smt_engine.cpp | 5 +++++ 1 file changed, 5 insertions(+) (limited to 'src/smt/smt_engine.cpp') 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 ); } -- cgit v1.2.3