From ba6ade0fc3f4cd339885652bb9bf5c87113c498d Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Thu, 5 Mar 2020 17:23:45 -0800 Subject: Remove --apply-to-const preprocessing pass (#3919) Fixes #3914. The pass was only applicable to inputs with UFs that were exclusively applied to single integer values. This limitation seems to make the preprocessing pass not very useful in practice and it is subsumed by our Ackermannization pass, which can remove UFs from more complex inputs. Thus, this commit removes the preprocessing pass. --- src/options/smt_options.toml | 9 --------- 1 file changed, 9 deletions(-) (limited to 'src/options') diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml index 88842faf7..676e01484 100644 --- a/src/options/smt_options.toml +++ b/src/options/smt_options.toml @@ -634,15 +634,6 @@ header = "options/smt_options.h" read_only = true help = "amount of resources spent for each sat conflict (bitvectors)" -[[option]] - name = "rewriteApplyToConst" - category = "expert" - long = "rewrite-apply-to-const" - type = "bool" - default = "false" - read_only = true - help = "eliminate function applications, rewriting e.g. f(5) to a new symbol f_5" - # --replay is currently broken; don't document it for 1.0 [[option]] name = "replayInputFilename" -- cgit v1.2.3