diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-08-11 15:36:38 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-08-11 13:36:38 -0700 |
| commit | 1339e2a3b884d34a9c27eb45bb6847a493fe0365 (patch) | |
| tree | eee01493ebe789c8c1b09e5f977273c360a52bc7 /src/options/quantifiers_options.toml | |
| parent | 1c859fd0f43fa2081bdb247423e81d9174a5f474 (diff) | |
Remove instantiation model true option (#4861)
This was an option that rejected instantiations that are true according to the current
model's equality engine.
This option was never helpful and will be burdensome to maintain with new updates
to equality engine infrastructure.
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 17 |
1 files changed, 0 insertions, 17 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index b62468cdd..4b130158c 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -493,15 +493,6 @@ header = "options/quantifiers_options.h" help = "allow theory combination to happen once initially, before quantifier strategies are run" [[option]] - name = "quantModelEe" - category = "regular" - long = "quant-model-ee" - type = "bool" - default = "false" - read_only = true - help = "use equality engine of model for last call effort" - -[[option]] name = "instMaxLevel" category = "regular" long = "inst-max-level=N" @@ -824,14 +815,6 @@ header = "options/quantifiers_options.h" help = "do not consider instances of quantified formulas that are currently entailed" [[option]] - name = "instNoModelTrue" - category = "regular" - long = "inst-no-model-true" - type = "bool" - default = "false" - help = "do not consider instances of quantified formulas that are currently true in model, if it is available" - -[[option]] name = "qcfEagerTest" category = "regular" long = "qcf-eager-test" |