diff options
Diffstat (limited to 'test/regress/regress0/strings/loop005.smt2')
| -rw-r--r-- | test/regress/regress0/strings/loop005.smt2 | 10 |
1 files changed, 6 insertions, 4 deletions
diff --git a/test/regress/regress0/strings/loop005.smt2 b/test/regress/regress0/strings/loop005.smt2 index 4401ef794..039409ea6 100644 --- a/test/regress/regress0/strings/loop005.smt2 +++ b/test/regress/regress0/strings/loop005.smt2 @@ -5,11 +5,13 @@ (declare-fun y () String) (declare-fun z () String) (declare-fun w () String) -(declare-fun w1 () String) -(declare-fun w2 () String) -(assert (= (str.++ x y z) (str.++ x z y))) -(assert (= (str.++ x w z) (str.++ x z w))) +;(assert (= (str.++ x y z) (str.++ x z y))) +;(assert (= (str.++ x w z) (str.++ x z w))) + +(assert (= (str.++ y z) (str.++ z y))) +(assert (= (str.++ w z) (str.++ z w))) + (assert (not (= y w))) (assert (> (str.len z) 0)) |