summaryrefslogtreecommitdiff
path: root/src/options/sep_options
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/sep_options')
-rw-r--r--src/options/sep_options20
1 files changed, 20 insertions, 0 deletions
diff --git a/src/options/sep_options b/src/options/sep_options
new file mode 100644
index 000000000..043355bda
--- /dev/null
+++ b/src/options/sep_options
@@ -0,0 +1,20 @@
+#
+# Option specification file for CVC4
+# See src/options/base_options for a description of this file format
+#
+
+module SEP "options/sep_options.h" Sep
+
+option sepCheckNeg --sep-check-neg bool :default true
+ check negated spatial assertions
+
+option sepExp --sep-exp bool :default false
+ experimental flag for sep
+option sepMinimalRefine --sep-min-refine bool :default false
+ only add refinement lemmas for minimal (innermost) assertions
+option sepPreciseBound --sep-prec-bound bool :default false
+ calculate precise bounds for labels
+option sepDisequalC --sep-deq-c bool :default true
+ assume cardinality elements are distinct
+
+endmodule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback