diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2020-07-28 16:02:41 -0500 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2020-07-28 16:02:41 -0500 |
| commit | c323481d737d82b4b4b2906afec3200fe223707f (patch) | |
| tree | 636834eedc604f26799a7d54c69550e416c291f8 /src/options/arrays_options.toml | |
| parent | e8bbee7afb039834955aee96d181b499550a28fe (diff) | |
Remove arrays lazy rintro option (#4806)
This option has model soundness issues (#4771) and moreover is overall worse performance on SMT-LIB {QF_ABV QF_ABVFP QF_ABVFPLRA QF_ALIA QF_ANIA QF_AUFBV QF_AUFLIA QF_AUFNIA QF_AX}:
Configuration #unsat time #sat time #solved #total
CVC4-072720_def 9428 9405.46 24932 16631.6 34360 35399
CVC4-072720_nalr1 9446 9536.41 24924 16146.3 34370 35399
where def = default, nalr1 = --no-arrays-lazy-rintro1.
Fixes #4771.
FYI @barrettcw
Diffstat (limited to 'src/options/arrays_options.toml')
| -rw-r--r-- | src/options/arrays_options.toml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/options/arrays_options.toml b/src/options/arrays_options.toml index 389bb6e4c..309370163 100644 --- a/src/options/arrays_options.toml +++ b/src/options/arrays_options.toml @@ -11,14 +11,6 @@ header = "options/arrays_options.h" help = "turn on optimization for linear array terms (see de Moura FMCAD 09 arrays paper)" [[option]] - name = "arraysLazyRIntro1" - category = "regular" - long = "arrays-lazy-rintro1" - type = "bool" - default = "true" - help = "turn on optimization to only perform RIntro1 rule lazily (see Jovanovic/Barrett 2012: Being Careful with Theory Combination)" - -[[option]] name = "arraysWeakEquivalence" category = "regular" long = "arrays-weak-equiv" |