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.toml20
1 files changed, 0 insertions, 20 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index ab74fbc79..1437e9992 100644
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -439,15 +439,6 @@ header = "options/quantifiers_options.h"
help = "selection mode for representatives in quantifiers engine"
[[option]]
- name = "instRelevantCond"
- category = "regular"
- long = "inst-rlv-cond"
- type = "bool"
- default = "false"
- read_only = true
- help = "add relevancy conditions for instantiations"
-
-[[option]]
name = "fullSaturateQuant"
category = "regular"
long = "full-saturate-quant"
@@ -1450,17 +1441,6 @@ header = "options/quantifiers_options.h"
default = "false"
help = "perform anti-skolemization for quantified formulas"
-### e-unification options
-
-[[option]]
- name = "quantEqualityEngine"
- category = "regular"
- long = "quant-ee"
- type = "bool"
- default = "false"
- read_only = true
- help = "maintain congrunce closure over universal equalities"
-
### Higher-order options
[[option]]
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback