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 /test/regress/regress1/strings | |
| 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 'test/regress/regress1/strings')
| -rw-r--r-- | test/regress/regress1/strings/issue5940-2-skc-len-conc.smt2 | 8 | ||||
| -rw-r--r-- | test/regress/regress1/strings/issue5940-skc-len-conc.smt2 | 9 |
2 files changed, 17 insertions, 0 deletions
diff --git a/test/regress/regress1/strings/issue5940-2-skc-len-conc.smt2 b/test/regress/regress1/strings/issue5940-2-skc-len-conc.smt2 new file mode 100644 index 000000000..793381503 --- /dev/null +++ b/test/regress/regress1/strings/issue5940-2-skc-len-conc.smt2 @@ -0,0 +1,8 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(declare-fun x () String) +(declare-fun y () String) +(declare-fun z () Int) +(assert (not (= (str.prefixof (str.replace x x (str.replace "A" x "")) (str.replace "" x "A")) (= (not (= (not (not (= (= (str.prefixof (str.replace "A" x "") x) (str.prefixof "A" x)) (str.prefixof x x)))) (str.prefixof (str.replace "A" x "") (str.replace "A" "A" "")))) (str.prefixof x "A"))))) +(check-sat) diff --git a/test/regress/regress1/strings/issue5940-skc-len-conc.smt2 b/test/regress/regress1/strings/issue5940-skc-len-conc.smt2 new file mode 100644 index 000000000..f78a12deb --- /dev/null +++ b/test/regress/regress1/strings/issue5940-skc-len-conc.smt2 @@ -0,0 +1,9 @@ +; COMMAND-LINE: --strings-exp +; EXPECT: sat +(set-logic ALL) +(define-fun z () Int 0) +(define-fun y () String "") +(define-fun x () String "") +(assert (= "B" (str.replace (str.substr "A" 0 z) "" + (str.replace "B" (str.substr "B" 0 0) (str.substr "A" 0 z))))) +(check-sat) |