summaryrefslogtreecommitdiff
path: root/test/regress
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress')
-rw-r--r--test/regress/regress0/strings/loop007.smt218
-rw-r--r--test/regress/regress0/strings/model001.smt224
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)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback