summaryrefslogtreecommitdiff
path: root/src/options/quantifiers_options.toml
diff options
context:
space:
mode:
Diffstat (limited to 'src/options/quantifiers_options.toml')
-rw-r--r--src/options/quantifiers_options.toml18
1 files changed, 18 insertions, 0 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index 0a69178b3..03ffade46 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1784,6 +1784,24 @@ header = "options/quantifiers_options.h"
read_only = true
help = "merge term indices modulo equality"
+[[option]]
+ name = "hoElim"
+ category = "regular"
+ long = "ho-elim"
+ type = "bool"
+ default = "false"
+ read_only = true
+ help = "eagerly eliminate higher-order constraints"
+
+[[option]]
+ name = "hoElimStoreAx"
+ category = "regular"
+ long = "ho-elim-store-ax"
+ type = "bool"
+ default = "true"
+ read_only = false
+ help = "use store axiom during ho-elim"
+
### Proof options
[[option]]
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback