summaryrefslogtreecommitdiff
path: root/src/options
diff options
context:
space:
mode:
authorGuy <katz911@gmail.com>2016-06-08 15:24:44 -0700
committerGuy <katz911@gmail.com>2016-06-08 15:24:44 -0700
commitf948414b8b9979f3e680abdedf8e3e6fbbbdd226 (patch)
tree73592bb1c62f16a269bfa0983db93d2f204ea860 /src/options
parent2db4844c1f0c307071ea94d0d58d1f322a0b1a6b (diff)
parentc60db311c3e1ccd7b311fcea444865d1d5d32031 (diff)
Merge branch 'master' of https://github.com/CVC4/CVC4
Diffstat (limited to 'src/options')
-rw-r--r--src/options/datatypes_options2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/options/datatypes_options b/src/options/datatypes_options
index e9578f8d7..bb92b4e05 100644
--- a/src/options/datatypes_options
+++ b/src/options/datatypes_options
@@ -27,5 +27,7 @@ option dtInferAsLemmas --dt-infer-as-lemmas bool :default false
always send lemmas out instead of making internal inferences
#option dtRExplainLemmas --dt-rexplain-lemmas bool :default true
# regression explanations for datatype lemmas
+option dtBlastSplits --dt-blast-splits bool :default false
+ when applicable, blast splitting lemmas for all variables at once
endmodule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback