summaryrefslogtreecommitdiff
path: root/src/theory/arrays/options
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/arrays/options')
-rw-r--r--src/theory/arrays/options6
1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/arrays/options b/src/theory/arrays/options
index 755cf239c..8a971cfe8 100644
--- a/src/theory/arrays/options
+++ b/src/theory/arrays/options
@@ -11,4 +11,10 @@ option arraysOptimizeLinear --arrays-optimize-linear bool :default true :read-wr
option arraysLazyRIntro1 --arrays-lazy-rintro1 bool :default true :read-write
turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination)
+option arraysModelBased --arrays-model-based bool :default false :read-write
+ turn on model-based arrray solver
+
+option arraysEagerIndexSplitting --arrays-eager-index bool :default true :read-write
+ turn on eager index splitting for generated array lemmas
+
endmodule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback