A few more minor updates to match google repository with CVC4 repository

(mostly whitespace differences).

24 files changed, 345 insertions, 345 deletions

diff --git a/test/regress/regress0/fmf/fc-pigeonhole19.smt2 b/test/regress/regress0/fmf/fc-pigeonhole19.smt2
index 15c36682c..f145013d8 100644
--- a/test/regress/regress0/fmf/fc-pigeonhole19.smt2
+++ b/test/regress/regress0/fmf/fc-pigeonhole19.smt2
@@ -1,20 +1,20 @@
-(set-logic UFC)

-(set-info :status unsat)

-

-(declare-sort P 0)

-(declare-sort H 0)

-

-(declare-fun p () P)

-(declare-fun h () H)

-

-; pigeonhole using native cardinality constraints

-(assert (fmf.card p 19))

-(assert (not (fmf.card p 18)))

-(assert (fmf.card h 18))

-(assert (not (fmf.card h 17)))

-

-; each pigeon has different holes

-(declare-fun f (P) H)

-(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2))))))

-

+(set-logic UFC)
+(set-info :status unsat)
+
+(declare-sort P 0)
+(declare-sort H 0)
+
+(declare-fun p () P)
+(declare-fun h () H)
+
+; pigeonhole using native cardinality constraints
+(assert (fmf.card p 19))
+(assert (not (fmf.card p 18)))
+(assert (fmf.card h 18))
+(assert (not (fmf.card h 17)))
+
+; each pigeon has different holes
+(declare-fun f (P) H)
+(assert (forall ((p1 P) (p2 P)) (=> (not (= p1 p2)) (not (= (f p1) (f p2))))))
+
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/fmf/fc-unsat-pent.smt2 b/test/regress/regress0/fmf/fc-unsat-pent.smt2
index f1721cb04..2d4000e6e 100644
--- a/test/regress/regress0/fmf/fc-unsat-pent.smt2
+++ b/test/regress/regress0/fmf/fc-unsat-pent.smt2
@@ -1,20 +1,20 @@
-(set-logic QF_UFC)

-(set-info :status unsat)

-

-(declare-sort U 0)

-

-(declare-fun a () U)

-(declare-fun b () U)

-(declare-fun c () U)

-(declare-fun d () U)

-(declare-fun e () U)

-

-(assert (not (= a b)))

-(assert (not (= b c)))

-(assert (not (= c d)))

-(assert (not (= d e)))

-(assert (not (= e a)))

-

-(assert (fmf.card c 2))

-

+(set-logic QF_UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+(declare-fun d () U)
+(declare-fun e () U)
+
+(assert (not (= a b)))
+(assert (not (= b c)))
+(assert (not (= c d)))
+(assert (not (= d e)))
+(assert (not (= e a)))
+
+(assert (fmf.card c 2))
+
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2 b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
index d946974ed..0d438f718 100644
--- a/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
+++ b/test/regress/regress0/fmf/fc-unsat-tot-2.smt2
@@ -1,14 +1,14 @@
-(set-logic UFC)

-(set-info :status unsat)

-

-(declare-sort U 0)

-

-(declare-fun a () U)

-(declare-fun b () U)

-(declare-fun c () U)

-

-(assert (not (fmf.card a 2)))

-

-(assert (forall ((x U)) (or (= x a) (= x b))))

-

+(set-logic UFC)
+(set-info :status unsat)
+
+(declare-sort U 0)
+
+(declare-fun a () U)
+(declare-fun b () U)
+(declare-fun c () U)
+
+(assert (not (fmf.card a 2)))
+
+(assert (forall ((x U)) (or (= x a) (= x b))))
+
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/quantifiers/simp-typ-test.smt2 b/test/regress/regress0/quantifiers/simp-typ-test.smt2
index 366559b9d..380a66aac 100644
--- a/test/regress/regress0/quantifiers/simp-typ-test.smt2
+++ b/test/regress/regress0/quantifiers/simp-typ-test.smt2
@@ -1,7 +1,7 @@
-(set-logic UFLIRA)

-(set-info :status unsat)

-; ensure that E-matching matches on sub-types

-(declare-fun P (Real) Bool)

-(assert (forall ((x Real)) (P x)))

-(assert (not (P 5)))

+(set-logic UFLIRA)
+(set-info :status unsat)
+; ensure that E-matching matches on sub-types
+(declare-fun P (Real) Bool)
+(assert (forall ((x Real)) (P x)))
+(assert (not (P 5)))
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/at001.smt2 b/test/regress/regress0/strings/at001.smt2
index 616189d96..2ecbcc993 100644
--- a/test/regress/regress0/strings/at001.smt2
+++ b/test/regress/regress0/strings/at001.smt2
@@ -1,12 +1,12 @@
-(set-logic QF_S)

-(set-info :status sat)

-

-(declare-fun x () String)

-(declare-fun i () Int)

-

-(assert (= (str.at x i) "b"))

-(assert (and (>= i 4) (< i (str.len x))))

-(assert (< (str.len x) 7))

-(assert (> (str.len x) 2))

-

-(check-sat)

+(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun i () Int)
+
+(assert (= (str.at x i) "b"))
+(assert (and (>= i 4) (< i (str.len x))))
+(assert (< (str.len x) 7))
+(assert (> (str.len x) 2))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/bug001.smt2 b/test/regress/regress0/strings/bug001.smt2
index 49568329e..cdeebd20b 100644
--- a/test/regress/regress0/strings/bug001.smt2
+++ b/test/regress/regress0/strings/bug001.smt2
@@ -1,15 +1,15 @@
-(set-logic QF_S)

-(set-info :status sat)

-

-(declare-fun x () String)

-(declare-fun y () String)

-(declare-fun z () String)

-

-(assert (= "\x4a" x))

-(assert (= "\x6a" y))

-

-(assert (= "\x4A" z))

-

-(assert (= x z))

-

-(check-sat)

+(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (= "\x4a" x))
+(assert (= "\x6a" y))
+
+(assert (= "\x4A" z))
+
+(assert (= x z))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/bug002.smt2 b/test/regress/regress0/strings/bug002.smt2
index 15d1ea5a2..f8a481e14 100644
--- a/test/regress/regress0/strings/bug002.smt2
+++ b/test/regress/regress0/strings/bug002.smt2
@@ -1,10 +1,10 @@
-(set-logic ASLIA)

-(set-info :smt-lib-version 2.0)

-(set-option :strings-exp true)

-(set-info :status sat)

-

-; regex = [\*-,\t\*-\|](.{6,}()?)+

-(define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.loop re.allchar 6 ) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) )  ) )

-(assert (not (strinre "6O\1\127\n?")))

-

+(set-logic ASLIA)
+(set-info :smt-lib-version 2.0)
+(set-option :strings-exp true)
+(set-info :status sat)
+
+; regex = [\*-,\t\*-\|](.{6,}()?)+
+(define-fun strinre ((?s String)) Bool (str.in.re ?s (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.union re.nostr (re.range "*" ",") (str.to.re "\t") (re.range "*" "|") ) (re.+ (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") (re.loop re.allchar 6 ) (re.opt (re.union re.nostr (re.++ (str.to.re "") (str.to.re "") ) ) ) ) ) ) ) )  ) )
+(assert (not (strinre "6O\1\127\n?")))
+
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/escchar.smt2 b/test/regress/regress0/strings/escchar.smt2
index aa2afb7e4..67a184ade 100644
--- a/test/regress/regress0/strings/escchar.smt2
+++ b/test/regress/regress0/strings/escchar.smt2
@@ -1,12 +1,12 @@
-(set-logic QF_S)

-(set-info :status sat)

-(set-info :smt-lib-version 2.0)

-

-(declare-fun x () String)

-(declare-const I Int)

-

-(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\\"\t\a\b"))

-(assert (= I (str.len x)))

-

-

-(check-sat)

+(set-logic QF_S)
+(set-info :status sat)
+(set-info :smt-lib-version 2.0)
+
+(declare-fun x () String)
+(declare-const I Int)
+
+(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\\"\t\a\b"))
+(assert (= I (str.len x)))
+
+
+(check-sat)
diff --git a/test/regress/regress0/strings/escchar_25.smt2 b/test/regress/regress0/strings/escchar_25.smt2
index f48995344..af93a7ae5 100644
--- a/test/regress/regress0/strings/escchar_25.smt2
+++ b/test/regress/regress0/strings/escchar_25.smt2
@@ -1,12 +1,12 @@
-(set-logic QF_S)

-(set-info :status sat)

-(set-info :smt-lib-version 2.5)

-

-(declare-fun x () String)

-(declare-const I Int)

-

-(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\""\t\a\b"))

-(assert (= I (str.len x)))

-

-

-(check-sat)

+(set-logic QF_S)
+(set-info :status sat)
+(set-info :smt-lib-version 2.5)
+
+(declare-fun x () String)
+(declare-const I Int)
+
+(assert (= x "\0\1\2\3\04\005\x06\7\8\9ABC\\""\t\a\b"))
+(assert (= I (str.len x)))
+
+
+(check-sat)
diff --git a/test/regress/regress0/strings/fmf001.smt2 b/test/regress/regress0/strings/fmf001.smt2
index 05bbab586..6081c8e06 100644
--- a/test/regress/regress0/strings/fmf001.smt2
+++ b/test/regress/regress0/strings/fmf001.smt2
@@ -1,20 +1,20 @@
-(set-logic QF_S)

-(set-option :strings-exp true)

-(set-option :strings-fmf true)

-(set-info :status sat)

-

-(declare-fun x () String)

-(declare-fun y () String)

-

-(assert (str.in.re x

-		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))

-	))

-

-(assert (str.in.re y

-		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))

-	))

-

-(assert (not (= x y)))

-(assert (= (str.len x) (str.len y)))

-

-(check-sat)

+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-option :strings-fmf true)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+
+(assert (str.in.re x
+		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+	))
+
+(assert (str.in.re y
+		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+	))
+
+(assert (not (= x y)))
+(assert (= (str.len x) (str.len y)))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/fmf002.smt2 b/test/regress/regress0/strings/fmf002.smt2
index 1d41b1085..d52dae2d2 100644
--- a/test/regress/regress0/strings/fmf002.smt2
+++ b/test/regress/regress0/strings/fmf002.smt2
@@ -1,17 +1,17 @@
-(set-logic QF_S)

-(set-option :strings-exp true)

-(set-option :strings-fmf true)

-(set-info :status sat)

-

-(declare-fun x () String)

-(declare-fun y () String)

-(declare-fun z () String)

-

-(assert (str.in.re x

-                (re.+ (re.range "a" "c"))

-				                ))

-

-(assert (= x (str.++ y "c" z "b")))

-(assert (> (str.len z) 1))

-

-(check-sat)

+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-option :strings-fmf true)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+(assert (str.in.re x
+                (re.+ (re.range "a" "c"))
+				                ))
+
+(assert (= x (str.++ y "c" z "b")))
+(assert (> (str.len z) 1))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/leadingzero001.smt2 b/test/regress/regress0/strings/leadingzero001.smt2
index ae61b5f5b..2889348c1 100644
--- a/test/regress/regress0/strings/leadingzero001.smt2
+++ b/test/regress/regress0/strings/leadingzero001.smt2
@@ -1,11 +1,11 @@
-(set-logic QF_S)

-(set-option :strings-exp true)

-(set-info :status sat)

-

-(declare-fun Y () String)

-

-(assert (= Y "0001"))

-;(assert (= (str.to.int Y) (- 1)))

-(assert (= (str.to.int Y) 1))

-

-(check-sat)

+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-info :status sat)
+
+(declare-fun Y () String)
+
+(assert (= Y "0001"))
+;(assert (= (str.to.int Y) (- 1)))
+(assert (= (str.to.int Y) 1))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/loop008.smt2 b/test/regress/regress0/strings/loop008.smt2
index 113577e48..f84ba442b 100644
--- a/test/regress/regress0/strings/loop008.smt2
+++ b/test/regress/regress0/strings/loop008.smt2
@@ -1,10 +1,10 @@
-(set-logic QF_S)

-(set-option :strings-exp true)

-(set-info :status sat)

-

-(declare-fun x () String)

-

-(assert (= (str.++ x "ab") (str.++ "ba" x)))

-(assert (> (str.len x) 5))

-

-(check-sat)

+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-info :status sat)
+
+(declare-fun x () String)
+
+(assert (= (str.++ x "ab") (str.++ "ba" x)))
+(assert (> (str.len x) 5))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/loop009.smt2 b/test/regress/regress0/strings/loop009.smt2
index 9ccc6de6e..30fc6cebc 100644
--- a/test/regress/regress0/strings/loop009.smt2
+++ b/test/regress/regress0/strings/loop009.smt2
@@ -1,10 +1,10 @@
-(set-logic QF_S)

-(set-option :strings-exp true)

-(set-info :status sat)

-

-(declare-fun x () String)

-

-(assert (= (str.++ x "aa") (str.++ "aa" x)))

-(assert (= (str.len x) 7))

-

-(check-sat)

+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-info :status sat)
+
+(declare-fun x () String)
+
+(assert (= (str.++ x "aa") (str.++ "aa" x)))
+(assert (= (str.len x) 7))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/regexp001.smt2 b/test/regress/regress0/strings/regexp001.smt2
index 6a2044ea8..62c142d1d 100644
--- a/test/regress/regress0/strings/regexp001.smt2
+++ b/test/regress/regress0/strings/regexp001.smt2
@@ -1,13 +1,13 @@
-(set-logic QF_S)

-(set-info :status sat)

-(set-option :strings-exp true)

-

-(declare-fun x () String)

-

-(assert (str.in.re x

-		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))

-	))

-

-(assert (= (str.len x) 3))

-

-(check-sat)

+(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun x () String)
+
+(assert (str.in.re x
+		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+	))
+
+(assert (= (str.len x) 3))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/regexp002.smt2 b/test/regress/regress0/strings/regexp002.smt2
index 8c29ccb38..a8bd2187a 100644
--- a/test/regress/regress0/strings/regexp002.smt2
+++ b/test/regress/regress0/strings/regexp002.smt2
@@ -1,24 +1,24 @@
-(set-logic QF_S)

-(set-info :status sat)

-(set-option :strings-exp true)

-; this option requires user to check whether the constraint is in the fragment

-; currently we do not provide only positive membership constraint checking

-; if users use this option but the constraint is not in this fragment, the result will fail

-(set-option :strings-inm true)

-

-(declare-fun x () String)

-(declare-fun y () String)

-

-(assert (str.in.re x

-		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))

-	))

-

-(assert (str.in.re y

-		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))

-	))

-

-(assert (not (= x y)))

-(assert (= (str.len x) (str.len y)))

-(assert (= (str.len y) 3))

-

-(check-sat)

+(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+; this option requires user to check whether the constraint is in the fragment
+; currently we do not provide only positive membership constraint checking
+; if users use this option but the constraint is not in this fragment, the result will fail
+(set-option :strings-inm true)
+
+(declare-fun x () String)
+(declare-fun y () String)
+
+(assert (str.in.re x
+		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+	))
+
+(assert (str.in.re y
+		(re.* (re.++ (re.* (str.to.re "a") ) (str.to.re "b") ))
+	))
+
+(assert (not (= x y)))
+(assert (= (str.len x) (str.len y)))
+(assert (= (str.len y) 3))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/regexp003.smt2 b/test/regress/regress0/strings/regexp003.smt2
index 601689958..7696838fe 100644
--- a/test/regress/regress0/strings/regexp003.smt2
+++ b/test/regress/regress0/strings/regexp003.smt2
@@ -1,13 +1,13 @@
-(set-logic QF_S)

-(set-info :status sat)

-(set-option :strings-exp true)

-

-(declare-const s String)

-

-(assert (str.in.re s (re.inter

-	(re.++ (str.to.re "a") (re.* (str.to.re "b")) 

-		(re.inter (str.to.re "c") (re.* (str.to.re "c"))))

-	(re.++ (str.to.re "a") (re.* (str.to.re "b")) (re.* (str.to.re "c")))

-	)))

-

-(check-sat)

+(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-const s String)
+
+(assert (str.in.re s (re.inter
+	(re.++ (str.to.re "a") (re.* (str.to.re "b")) 
+		(re.inter (str.to.re "c") (re.* (str.to.re "c"))))
+	(re.++ (str.to.re "a") (re.* (str.to.re "b")) (re.* (str.to.re "c")))
+	)))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/reloop.smt2 b/test/regress/regress0/strings/reloop.smt2
index 39b2b76b1..9915504ae 100644
--- a/test/regress/regress0/strings/reloop.smt2
+++ b/test/regress/regress0/strings/reloop.smt2
@@ -1,18 +1,18 @@
-(set-logic QF_S)

-(set-option :strings-exp true)

-(set-info :status sat)

-

-(declare-fun x () String)

-(declare-fun y () String)

-(declare-fun z () String)

-(declare-fun w () String)

-

-(assert (str.in.re x (re.loop (str.to.re "a") 5)))

-(assert (str.in.re y (re.loop (str.to.re "b") 2 5)))

-(assert (str.in.re z (re.loop (str.to.re "c") 5)))

-(assert (> (str.len z) 7))

-(assert (str.in.re w (re.loop (str.to.re "b") 2 7)))

-(assert (> (str.len w) 2))

-(assert (< (str.len w) 5))

-

-(check-sat)

+(set-logic QF_S)
+(set-option :strings-exp true)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun w () String)
+
+(assert (str.in.re x (re.loop (str.to.re "a") 5)))
+(assert (str.in.re y (re.loop (str.to.re "b") 2 5)))
+(assert (str.in.re z (re.loop (str.to.re "c") 5)))
+(assert (> (str.len z) 7))
+(assert (str.in.re w (re.loop (str.to.re "b") 2 7)))
+(assert (> (str.len w) 2))
+(assert (< (str.len w) 5))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/str006.smt2 b/test/regress/regress0/strings/str006.smt2
index 592ef6a7f..2bdf9b1b5 100644
--- a/test/regress/regress0/strings/str006.smt2
+++ b/test/regress/regress0/strings/str006.smt2
@@ -1,14 +1,14 @@
-(set-logic QF_S)

-(set-info :status sat)

-

-(declare-fun x () String)

-(declare-fun y () String)

-(declare-fun z () String)

-

-;plandowski p469 1

-(assert (= (str.++ x "ab" y) (str.++ y "ba" z)))

-(assert (= z (str.++ x y)))

-(assert (not (= (str.++ x "a") (str.++ "a" x))))

-

-(check-sat)

-

+(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+
+;plandowski p469 1
+(assert (= (str.++ x "ab" y) (str.++ y "ba" z)))
+(assert (= z (str.++ x y)))
+(assert (not (= (str.++ x "a") (str.++ "a" x))))
+
+(check-sat)
+
diff --git a/test/regress/regress0/strings/str007.smt2 b/test/regress/regress0/strings/str007.smt2
index 0ca2ec4c3..a7173701a 100644
--- a/test/regress/regress0/strings/str007.smt2
+++ b/test/regress/regress0/strings/str007.smt2
@@ -1,13 +1,13 @@
-(set-logic QF_S)

-(set-info :status unsat)

-

-(declare-fun x () String)

-(declare-fun y () String)

-

-

-(assert (or (= x y) (= x y)))

-

-(assert (= (str.++ x "ba") (str.++ "ab" x)))

-(assert (= (str.++ y "ab") (str.++ "ab" y)))

-

-(check-sat)

+(set-logic QF_S)
+(set-info :status unsat)
+
+(declare-fun x () String)
+(declare-fun y () String)
+
+
+(assert (or (= x y) (= x y)))
+
+(assert (= (str.++ x "ba") (str.++ "ab" x)))
+(assert (= (str.++ y "ab") (str.++ "ab" y)))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/substr001.smt2 b/test/regress/regress0/strings/substr001.smt2
index bdfa33afb..78f3ffee7 100644
--- a/test/regress/regress0/strings/substr001.smt2
+++ b/test/regress/regress0/strings/substr001.smt2
@@ -1,16 +1,16 @@
-(set-logic QF_S)

-(set-info :status sat)

-

-(declare-fun x () String)

-(declare-fun i1 () Int)

-(declare-fun i2 () Int)

-(declare-fun i3 () Int)

-(declare-fun i4 () Int)

-

-(assert (and (>= i1 0) (>= i2 0) (< (+ i1 i2) (str.len x))))

-(assert (and (>= i3 0) (>= i4 0) (< (+ i3 i4) (str.len x))))

-(assert (= "efg" (str.substr x i1 i2) ) )

-(assert (= "bef" (str.substr x i3 i4) ) )

-(assert (> (str.len x) 5))

-

-(check-sat)

+(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun x () String)
+(declare-fun i1 () Int)
+(declare-fun i2 () Int)
+(declare-fun i3 () Int)
+(declare-fun i4 () Int)
+
+(assert (and (>= i1 0) (>= i2 0) (< (+ i1 i2) (str.len x))))
+(assert (and (>= i3 0) (>= i4 0) (< (+ i3 i4) (str.len x))))
+(assert (= "efg" (str.substr x i1 i2) ) )
+(assert (= "bef" (str.substr x i3 i4) ) )
+(assert (> (str.len x) 5))
+
+(check-sat)
diff --git a/test/regress/regress0/strings/type001.smt2 b/test/regress/regress0/strings/type001.smt2
index ca93b00e5..77eabcccc 100644
--- a/test/regress/regress0/strings/type001.smt2
+++ b/test/regress/regress0/strings/type001.smt2
@@ -1,21 +1,21 @@
-(set-logic QF_S)

-(set-info :status sat)

-(set-option :strings-exp true)

-

-(declare-fun x () String)

-(declare-fun y () String)

-(declare-fun i () Int)

-(declare-fun j () Int)

-(declare-fun z () String)

-

-;big num test

-(assert (= x (int.to.str 4785582390527685649)))

-;should be ""

-(assert (= y (int.to.str (- 9))))

-

-;big num

-(assert (= i (str.to.int "783914785582390527685649")))

-;should be -1

-(assert (= j (str.to.int "-783914785582390527685649")))

-

+(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun i () Int)
+(declare-fun j () Int)
+(declare-fun z () String)
+
+;big num test
+(assert (= x (int.to.str 4785582390527685649)))
+;should be ""
+(assert (= y (int.to.str (- 9))))
+
+;big num
+(assert (= i (str.to.int "783914785582390527685649")))
+;should be -1
+(assert (= j (str.to.int "-783914785582390527685649")))
+
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/type002.smt2 b/test/regress/regress0/strings/type002.smt2
index cbad2226a..296057a76 100644
--- a/test/regress/regress0/strings/type002.smt2
+++ b/test/regress/regress0/strings/type002.smt2
@@ -1,18 +1,18 @@
-(set-logic QF_S)

-(set-info :status sat)

-(set-option :strings-exp true)

-

-(declare-fun x () String)

-(declare-fun y () String)

-(declare-fun z () String)

-(declare-fun i () Int)

-

-(assert (>= i 420))

-(assert (= x (u16.to.str i)))

-(assert (= x (str.++ y "0" z)))

-(assert (not (= y "")))

-(assert (not (= z "")))

-

-

-

+(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun x () String)
+(declare-fun y () String)
+(declare-fun z () String)
+(declare-fun i () Int)
+
+(assert (>= i 420))
+(assert (= x (u16.to.str i)))
+(assert (= x (str.++ y "0" z)))
+(assert (not (= y "")))
+(assert (not (= z "")))
+
+
+
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/type003.smt2 b/test/regress/regress0/strings/type003.smt2
index b8f0ac5ae..c2d4792cc 100644
--- a/test/regress/regress0/strings/type003.smt2
+++ b/test/regress/regress0/strings/type003.smt2
@@ -1,12 +1,12 @@
-(set-logic QF_S)

-(set-info :status sat)

-(set-option :strings-exp true)

-

-(declare-fun i () Int)

-(declare-fun s () String)

-

-(assert (< 67 (str.to.int s)))

-(assert (= (str.len s) 2))

-(assert (not (= s "68")))

-

-(check-sat)

+(set-logic QF_S)
+(set-info :status sat)
+(set-option :strings-exp true)
+
+(declare-fun i () Int)
+(declare-fun s () String)
+
+(assert (< 67 (str.to.int s)))
+(assert (= (str.len s) 2))
+(assert (not (= s "68")))
+
+(check-sat)