diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-27 18:42:13 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-09-27 18:42:13 -0400 |
| commit | 546e6aca016ea1f9b7da0bcfda5bed833a7a13ec (patch) | |
| tree | f8722044b32d1360357a12034f5b919490f05456 /test/regress/regress0/strings/loop007.smt2 | |
| parent | b72ebc42011e4d55b28b807d362694447448c4e8 (diff) | |
Some fixes to recent strings commits.
Diffstat (limited to 'test/regress/regress0/strings/loop007.smt2')
| -rw-r--r-- | test/regress/regress0/strings/loop007.smt2 | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/test/regress/regress0/strings/loop007.smt2 b/test/regress/regress0/strings/loop007.smt2 index 8d789edb3..0534d8b53 100644 --- a/test/regress/regress0/strings/loop007.smt2 +++ b/test/regress/regress0/strings/loop007.smt2 @@ -1,10 +1,10 @@ -(set-logic ALL_SUPPORTED)
-(set-info :status sat)
-
-(declare-fun x () String)
-(declare-fun y () String)
-
-(assert (= (str.++ x y "aa") (str.++ "aa" y x)))
-(assert (= (str.len x) 1))
-
+(set-logic ALL_SUPPORTED) +(set-info :status sat) + +(declare-fun x () String) +(declare-fun y () String) + +(assert (= (str.++ x y "aa") (str.++ "aa" y x))) +(assert (= (str.len x) 1)) + (check-sat)
\ No newline at end of file |