diff options
author | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
---|---|---|
committer | PaulMeng <baolmeng@gmail.com> | 2016-04-20 14:43:18 -0500 |
commit | 904ffb6e73402bae537aa89e7fd8f0ab2e9d60e2 (patch) | |
tree | d96bb0c974bdea6170957d3e39d47a98f5c85ca0 /src/options/strings_options | |
parent | a0054e9cc78822416d745e955c30f69cbb2a3aa7 (diff) |
update from the master
Diffstat (limited to 'src/options/strings_options')
-rw-r--r-- | src/options/strings_options | 12 |
1 files changed, 12 insertions, 0 deletions
diff --git a/src/options/strings_options b/src/options/strings_options index 65c293dbc..5c991a1bb 100644 --- a/src/options/strings_options +++ b/src/options/strings_options @@ -53,6 +53,18 @@ option stringInferSym strings-infer-sym --strings-infer-sym bool :default true strings split on empty string option stringEagerLen strings-eager-len --strings-eager-len bool :default true strings eager length lemmas +option stringCheckEntailLen strings-check-entail-len --strings-check-entail-len bool :default true + check entailment between length terms to reduce splitting +option stringProcessLoop strings-process-loop --strings-process-loop bool :default true + reduce looping word equations to regular expressions +option stringAbortLoop strings-abort-loop --strings-abort-loop bool :default false + abort when a looping word equation is encountered +option stringInferAsLemmas strings-infer-as-lemmas --strings-infer-as-lemmas bool :default false + always send lemmas out instead of making internal inferences +option stringRExplainLemmas strings-rexplain-lemmas --strings-rexplain-lemmas bool :default true + regression explanations for string lemmas +option stringMinPrefixExplain strings-min-prefix-explain --strings-min-prefix-explain bool :default true + minimize explanations for prefix of normal forms in strings endmodule |