diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-22 14:15:43 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-22 14:15:43 -0600 |
| commit | ddf647904de838e8e6ee266ad13de8a6a90250c8 (patch) | |
| tree | 12105cab2b35dd303e04e7735d7923587b758af0 /src/options | |
| parent | 85d96c3668495fb087f059e5662072ae66d69e22 (diff) | |
Require length-in-conclusion form for strings inferences (#5953)
Previously, it was optional whether to put length constraints in conclusion for deq string inferences. However, due to optimizations in skolem caching, it is now required to guard these length constraints.
It furthermore changes the policy to not ignore the lengths for the registered skolem, since it may be shared elsewhere.
Fixes #5940.
Notice that proof-new already requires this option to be enabled when proofs are enabled. Hence, this will simplify proof-new when merged.
Diffstat (limited to 'src/options')
| -rw-r--r-- | src/options/strings_options.toml | 8 |
1 files changed, 0 insertions, 8 deletions
diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml index f9893ef3a..75da2a35b 100644 --- a/src/options/strings_options.toml +++ b/src/options/strings_options.toml @@ -216,14 +216,6 @@ header = "options/strings_options.h" help = "use a single skolem for the variable splitting rule" [[option]] - name = "stringLenConc" - category = "regular" - long = "strings-len-conc" - type = "bool" - default = "false" - help = "add skolem length constraints in conclusions of inferences" - -[[option]] name = "stringEagerEval" category = "regular" long = "strings-eager-eval" |