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 | |
| parent | b72ebc42011e4d55b28b807d362694447448c4e8 (diff) | |
Some fixes to recent strings commits.
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/strings/loop007.smt2 | 18 | ||||
| -rw-r--r-- | test/regress/regress0/strings/model001.smt2 | 24 |
2 files changed, 21 insertions, 21 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 diff --git a/test/regress/regress0/strings/model001.smt2 b/test/regress/regress0/strings/model001.smt2 index e4e35f40d..2832b5c96 100644 --- a/test/regress/regress0/strings/model001.smt2 +++ b/test/regress/regress0/strings/model001.smt2 @@ -1,12 +1,12 @@ -(set-logic ALL_SUPPORTED)
-(set-info :status sat)
-(set-option :produce-models true)
-
-(declare-fun x () String)
-(declare-fun y () String)
-
-(assert (not (= x y)))
-(assert (= (str.len x) (str.len y)))
-
-(check-sat)
-;(get-model)
+(set-logic ALL_SUPPORTED) +(set-info :status sat) +(set-option :produce-models true) + +(declare-fun x () String) +(declare-fun y () String) + +(assert (not (= x y))) +(assert (= (str.len x) (str.len y))) + +(check-sat) +;(get-model) |