summaryrefslogtreecommitdiff
path: root/src/theory/quantifiers/options
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/quantifiers/options')
-rw-r--r--src/theory/quantifiers/options2
1 files changed, 2 insertions, 0 deletions
diff --git a/src/theory/quantifiers/options b/src/theory/quantifiers/options
index 560e29c3b..b47c98aa3 100644
--- a/src/theory/quantifiers/options
+++ b/src/theory/quantifiers/options
@@ -207,5 +207,7 @@ option localTheoryExt --local-t-ext bool :default false
do instantiation based on local theory extensions
option ltePartialInst --lte-partial-inst bool :default false
partially instantiate local theory quantifiers
+option lteRestrictInstClosure --lte-restrict-inst-closure bool :default false
+ treat arguments of inst closure as restricted terms for instantiation
endmodule
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback