diff options
Diffstat (limited to 'test/regress/regress0/strings/loop007.smt2')
| -rw-r--r-- | test/regress/regress0/strings/loop007.smt2 | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2 index bea4037d1..b292de512 100644 --- a/test/regress/regress0/strings/loop007.smt2 +++ b/test/regress/regress0/strings/loop007.smt2 @@ -5,6 +5,7 @@ (declare-fun y () String) (assert (= (str.++ x y "aa") (str.++ "aa" y x))) -(assert (= (str.len x) 1)) +(assert (= (str.len x) (* 2 (str.len y)))) +(assert (> (str.len x) 0)) -(check-sat)
\ No newline at end of file +(check-sat) |