diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-04 17:18:36 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-04-04 17:18:47 -0500 |
commit | 576d50ac7c13233a589771401537b587eb36361e (patch) | |
tree | 3f044ce37d5b3dc0f20db52339b3f1ae8cb59c8d /src/smt | |
parent | 0f69a8ba2286bd5d9b807c10ad350705952e93d6 (diff) |
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.
Diffstat (limited to 'src/smt')
-rw-r--r-- | src/smt/smt_engine.cpp | 5 |
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 ); } |