diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-12-22 01:49:28 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-12-22 08:49:28 +0100 |
| commit | 85da37188e1b206fb3dccf202633cf4c1d22da7c (patch) | |
| tree | 393b504da1f95943da51eb096b238ca2310228cb /src/options/quantifiers_options.toml | |
| parent | c9747ae3a0577498073a04de97a978e1d9464d5d (diff) | |
Remove preregister instantiation heuristic (#5713)
This was a hack to improve the QF arithmetic solver by ensuring that certain instantiation lemmas were preregistered. This is no longer needed and will be a hindrance to the currently line of refactoring.
Diffstat (limited to 'src/options/quantifiers_options.toml')
| -rw-r--r-- | src/options/quantifiers_options.toml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml index cb5785e6d..4aa612d5b 100644 --- a/src/options/quantifiers_options.toml +++ b/src/options/quantifiers_options.toml @@ -1668,14 +1668,6 @@ header = "options/quantifiers_options.h" help = "use real infinity for vts in counterexample-based quantifier instantiation" [[option]] - name = "cegqiPreRegInst" - category = "regular" - long = "cegqi-prereg-inst" - type = "bool" - default = "false" - help = "preregister ground instantiations in counterexample-based quantifier instantiation" - -[[option]] name = "cegqiMinBounds" category = "regular" long = "cegqi-min-bounds" |