summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
authorajreynol <andrew.j.reynolds@gmail.com>2014-08-29 15:03:00 +0200
committerajreynol <andrew.j.reynolds@gmail.com>2014-08-29 15:03:08 +0200
commit4397bf2a96fabe124ebd18e9ae9957689852afb3 (patch)
tree0dead911b583fdf33df9dd0291640ab41390ef70 /src/smt
parentb1cb97e9a76bb018e4c9cb7e2d6781dc0412ddad (diff)
Do not use pure theory terms as single triggers. Minor cleanup.
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/smt_engine.cpp5
1 files changed, 5 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 220318b4c..98cc7813d 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1299,6 +1299,11 @@ void SmtEngine::setDefaults() {
options::intWfInduction.set( true );
}
}
+ if( options::dtStcInduction() ){
+ if( !options::dtForceAssignment.wasSetByUser() ){
+ options::dtForceAssignment.set( true );
+ }
+ }
if( options::intWfInduction() ){
if( !options::purifyTriggers.wasSetByUser() ){
options::purifyTriggers.set( true );
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback