diff options
Diffstat (limited to 'test/regress/regress0/strings/rewrites-v2.smt2')
| -rw-r--r-- | test/regress/regress0/strings/rewrites-v2.smt2 | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/test/regress/regress0/strings/rewrites-v2.smt2 b/test/regress/regress0/strings/rewrites-v2.smt2 index 15954525f..be9f18681 100644 --- a/test/regress/regress0/strings/rewrites-v2.smt2 +++ b/test/regress/regress0/strings/rewrites-v2.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --strings-exp ; EXPECT: unsat -(set-info :smt-lib-version 2.5) +(set-info :smt-lib-version 2.6) (set-logic SLIA) (set-info :status unsat) (declare-fun x () String) @@ -9,8 +9,8 @@ ; these should all rewrite to false (assert (or -(str.contains "abcdef0ghij1abced" (str.++ "g" (int.to.str (str.len z)) x "a" y (int.to.str (+ (str.len z) 1)))) -(str.contains "abc23cd" (str.++ (int.to.str (str.len z)) (int.to.str (str.len z)) (int.to.str (str.len z)))) +(str.contains "abcdef0ghij1abced" (str.++ "g" (str.from_int (str.len z)) x "a" y (str.from_int (+ (str.len z) 1)))) +(str.contains "abc23cd" (str.++ (str.from_int (str.len z)) (str.from_int (str.len z)) (str.from_int (str.len z)))) (not (str.contains (str.++ x "ab" y) (str.++ "b" (str.substr y 0 4)))) (not (str.contains (str.++ x "ab" y) (str.++ (str.substr x 5 (str.len x)) "a"))) (str.contains (str.++ x y) (str.++ x "a" y)) |