Fixes some initialization and desctruction problems in quantifiers. Also restricts the desctructors of some components to not throw exceptions for pickier compiliers. Also changes some formatting of regression scripts.

16 files changed, 460 insertions, 460 deletions

diff --git a/test/regress/regress0/bug605.cvc b/test/regress/regress0/bug605.cvc
index 1ccf7fa9e..564464931 100644
--- a/test/regress/regress0/bug605.cvc
+++ b/test/regress/regress0/bug605.cvc
@@ -1,30 +1,30 @@
-% EXPECT: sat

-OPTION "produce-models";

-

-% GeoLocation

-GeoLocation: TYPE = [# longitude: INT, latitude: INT #];

-

-% Stationary object

-StationaryObject: TYPE = [# geoLoc: SET OF GeoLocation #];

-Facet: TYPE = [# base: StationaryObject #];

-

-Segment: TYPE = [# s_f: Facet #];

-A : TYPE = ARRAY INT OF Segment;

-a : A;

-

-p1: GeoLocation = (# longitude := 0, latitude := 0 #);

-

-s1: StationaryObject = (# geoLoc := {p1} #);

-

-

-f0: Facet = (# base := s1 #);

-

-

-init: (A, INT, Facet) -> BOOLEAN

-  = LAMBDA (v: A, i: INT, f: Facet): 

-    v[0].s_f = f;

-    

-    

-ASSERT (init(a, 2, f0));

-

-CHECKSAT TRUE;

+% EXPECT: sat
+OPTION "produce-models";
+
+% GeoLocation
+GeoLocation: TYPE = [# longitude: INT, latitude: INT #];
+
+% Stationary object
+StationaryObject: TYPE = [# geoLoc: SET OF GeoLocation #];
+Facet: TYPE = [# base: StationaryObject #];
+
+Segment: TYPE = [# s_f: Facet #];
+A : TYPE = ARRAY INT OF Segment;
+a : A;
+
+p1: GeoLocation = (# longitude := 0, latitude := 0 #);
+
+s1: StationaryObject = (# geoLoc := {p1} #);
+
+
+f0: Facet = (# base := s1 #);
+
+
+init: (A, INT, Facet) -> BOOLEAN
+  = LAMBDA (v: A, i: INT, f: Facet): 
+    v[0].s_f = f;
+    
+    
+ASSERT (init(a, 2, f0));
+
+CHECKSAT TRUE;
diff --git a/test/regress/regress0/datatypes/cdt-model-cade15.smt2 b/test/regress/regress0/datatypes/cdt-model-cade15.smt2
index 5b570a915..c23a9d594 100755
--- a/test/regress/regress0/datatypes/cdt-model-cade15.smt2
+++ b/test/regress/regress0/datatypes/cdt-model-cade15.smt2
@@ -1,17 +1,17 @@
-(set-logic ALL_SUPPORTED)

-(set-info :status sat)

-(declare-codatatypes () ((Stream (C (c Stream)) (D (d Stream)) (E (e Stream)))))

-

-(declare-const z Stream)

-(declare-const x Stream)

-(declare-const y Stream)

-(declare-const u Stream)

-(declare-const v Stream)

-(declare-const w Stream)

-

-(assert (= u (C z)))

-(assert (= v (D z)))

-(assert (= w (E y)))

-(assert (= x (C v)))

-(assert (distinct x y z u v w))

+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(declare-codatatypes () ((Stream (C (c Stream)) (D (d Stream)) (E (e Stream)))))
+
+(declare-const z Stream)
+(declare-const x Stream)
+(declare-const y Stream)
+(declare-const u Stream)
+(declare-const v Stream)
+(declare-const w Stream)
+
+(assert (= u (C z)))
+(assert (= v (D z)))
+(assert (= w (E y)))
+(assert (= x (C v)))
+(assert (distinct x y z u v w))
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/quantifiers/floor.smt2 b/test/regress/regress0/quantifiers/floor.smt2
index cb20c1056..47aea95bf 100755
--- a/test/regress/regress0/quantifiers/floor.smt2
+++ b/test/regress/regress0/quantifiers/floor.smt2
@@ -1,4 +1,4 @@
-(set-logic LIRA)

-(set-info :status unsat)

-(assert (forall ((X Real)) (not (>= (+ (to_int (* 2 X)) (* (- 2) (to_int X))) 1)) ))

+(set-logic LIRA)
+(set-info :status unsat)
+(assert (forall ((X Real)) (not (>= (+ (to_int (* 2 X)) (* (- 2) (to_int X))) 1)) ))
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/quantifiers/is-int.smt2 b/test/regress/regress0/quantifiers/is-int.smt2
index 07e8dd246..fc7fbb180 100755
--- a/test/regress/regress0/quantifiers/is-int.smt2
+++ b/test/regress/regress0/quantifiers/is-int.smt2
@@ -1,4 +1,4 @@
-(set-logic LIRA)

-(set-info :status unsat)

-(assert (forall ((X Real) (Y Real)) (or (not (is_int X)) (not (>= (+ X (* (- (/ 2 3)) Y)) (- (/ 1 6)))) (not (>= (+ (* (- 1) X) (* (- (/ 1 4)) Y)) (- (/ 61 8)))) (not (>= (+ (* (- 1) X) (* (/ 5 2) Y)) 13))) ))

+(set-logic LIRA)
+(set-info :status unsat)
+(assert (forall ((X Real) (Y Real)) (or (not (is_int X)) (not (>= (+ X (* (- (/ 2 3)) Y)) (- (/ 1 6)))) (not (>= (+ (* (- 1) X) (* (- (/ 1 4)) Y)) (- (/ 61 8)))) (not (>= (+ (* (- 1) X) (* (/ 5 2) Y)) 13))) ))
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/bug686dd.smt2 b/test/regress/regress0/strings/bug686dd.smt2
index 7db4b86f0..688cecec1 100644
--- a/test/regress/regress0/strings/bug686dd.smt2
+++ b/test/regress/regress0/strings/bug686dd.smt2
@@ -1,13 +1,13 @@
-(set-logic UFDTSLIA)

-(set-info :status sat)

-

-(declare-datatypes () ( (T (TC (TCb String))) ) )

-

-(declare-fun root5 () String)

-(declare-fun root6 () T)

-

-(assert (and 

-(str.in.re root5 (re.loop (re.range "0" "9") 4 4) )

-(str.in.re (TCb root6) (re.loop (re.range "0" "9") 4 4) )

-) )

-(check-sat)

+(set-logic UFDTSLIA)
+(set-info :status sat)
+
+(declare-datatypes () ( (T (TC (TCb String))) ) )
+
+(declare-fun root5 () String)
+(declare-fun root6 () T)
+
+(assert (and 
+(str.in.re root5 (re.loop (re.range "0" "9") 4 4) )
+(str.in.re (TCb root6) (re.loop (re.range "0" "9") 4 4) )
+) )
+(check-sat)
diff --git a/test/regress/regress0/strings/chapman150408.smt2 b/test/regress/regress0/strings/chapman150408.smt2
index 546c46e32..f03718556 100644
--- a/test/regress/regress0/strings/chapman150408.smt2
+++ b/test/regress/regress0/strings/chapman150408.smt2
@@ -1,10 +1,10 @@
-(set-logic SLIA)

-(set-info :status sat)

-(set-option :strings-exp true)

-(set-option :rewrite-divk true)

-(declare-fun string () String)

-(assert (and

-     (and (not (not (not (= (ite (> (str.indexof string ";" 0) 0) 1 0)

-     0)))) (not (= (ite (not (= (str.len string) 0)) 1 0) 0))) (not

-     (not (= (ite (str.contains string "]") 1 0) 0)))))

-(check-sat)

+(set-logic SLIA)
+(set-info :status sat)
+(set-option :strings-exp true)
+(set-option :rewrite-divk true)
+(declare-fun string () String)
+(assert (and
+     (and (not (not (not (= (ite (> (str.indexof string ";" 0) 0) 1 0)
+     0)))) (not (= (ite (not (= (str.len string) 0)) 1 0) 0))) (not
+     (not (= (ite (str.contains string "]") 1 0) 0)))))
+(check-sat)
diff --git a/test/regress/regress0/strings/crash-1019.smt2 b/test/regress/regress0/strings/crash-1019.smt2
index 1a41ba715..9f2e99b02 100755
--- a/test/regress/regress0/strings/crash-1019.smt2
+++ b/test/regress/regress0/strings/crash-1019.smt2
@@ -1,10 +1,10 @@
-(set-logic ALL_SUPPORTED)

-(set-option :strings-exp true)

-(set-option :rewrite-divk true)

-(set-info :status unsat)

- 

-(declare-fun s () String)

- 

-(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (= (str.++ (str.replace (str.substr s 0 (- (+ (str.indexof s "o" 0) 1) 0)) "o" "a") (str.++ (str.replace (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) 0 (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) "o" "a") (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))))) "faa") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) "o") 1 0) 0)))) (not (= (ite (str.contains (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o") 1 0) 0))) (not (= (ite (str.contains s "o") 1 0) 0))) (>= 0 0)) (> (- (+ (str.indexof s "o" 0) 1) 0) 0)) (> (str.len s) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= 0 0)) (> (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))))

- 

-(check-sat)

+(set-logic ALL_SUPPORTED)
+(set-option :strings-exp true)
+(set-option :rewrite-divk true)
+(set-info :status unsat)
+ 
+(declare-fun s () String)
+ 
+(assert (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (and (not (not (not (= (ite (= (str.++ (str.replace (str.substr s 0 (- (+ (str.indexof s "o" 0) 1) 0)) "o" "a") (str.++ (str.replace (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) 0 (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) "o" "a") (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))))) "faa") 1 0) 0)))) (not (not (= (ite (str.contains (str.substr (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) "o") 1 0) 0)))) (not (= (ite (str.contains (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o") 1 0) 0))) (not (= (ite (str.contains s "o") 1 0) 0))) (>= 0 0)) (> (- (+ (str.indexof s "o" 0) 1) 0) 0)) (> (str.len s) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= 0 0)) (> (- (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) 0)) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))) (>= (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1) 0)) (> (- (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1)) 0)) (> (str.len (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1)))) (+ (str.indexof (str.substr s (+ (str.indexof s "o" 0) 1) (- (str.len s) (+ (str.indexof s "o" 0) 1))) "o" 0) 1))) (>= (+ (str.indexof s "o" 0) 1) 0)) (> (- (str.len s) (+ (str.indexof s "o" 0) 1)) 0)) (> (str.len s) (+ (str.indexof s "o" 0) 1))))
+ 
+(check-sat)
diff --git a/test/regress/regress0/strings/ilc-l-nt.smt2 b/test/regress/regress0/strings/ilc-l-nt.smt2
index 32dfc0b1b..9e1cc2bc5 100755
--- a/test/regress/regress0/strings/ilc-l-nt.smt2
+++ b/test/regress/regress0/strings/ilc-l-nt.smt2
@@ -1,14 +1,14 @@
-(set-logic ALL_SUPPORTED)

-(set-info :status unsat)

-(set-option :strings-exp true)

- 

-(declare-fun s () String)

-(assert (or (= s "Id like cookies.") (= s "Id not like cookies.")))

- 

-(declare-fun target () String)

-(assert (or (= target "l") (= target "m")))

- 

-(declare-fun location () Int)

-(assert (= (* 2 location) (str.indexof s target 0)))

- 

+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :strings-exp true)
+ 
+(declare-fun s () String)
+(assert (or (= s "Id like cookies.") (= s "Id not like cookies.")))
+ 
+(declare-fun target () String)
+(assert (or (= target "l") (= target "m")))
+ 
+(declare-fun location () Int)
+(assert (= (* 2 location) (str.indexof s target 0)))
+ 
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/ilc-like.smt2 b/test/regress/regress0/strings/ilc-like.smt2
index a711c215c..bb708ee5c 100755
--- a/test/regress/regress0/strings/ilc-like.smt2
+++ b/test/regress/regress0/strings/ilc-like.smt2
@@ -1,14 +1,14 @@
-(set-logic ALL_SUPPORTED)

-(set-info :status sat)

-(set-option :strings-exp true)

- 

-(declare-fun s () String)

-(assert (= s "I like cookies."))

- 

-(declare-fun target () String)

-(assert (= target "like"))

- 

-(declare-fun location () Int)

-(assert (= location (str.indexof s target 0)))

- 

+(set-logic ALL_SUPPORTED)
+(set-info :status sat)
+(set-option :strings-exp true)
+ 
+(declare-fun s () String)
+(assert (= s "I like cookies."))
+ 
+(declare-fun target () String)
+(assert (= target "like"))
+ 
+(declare-fun location () Int)
+(assert (= location (str.indexof s target 0)))
+ 
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/indexof-sym-simp.smt2 b/test/regress/regress0/strings/indexof-sym-simp.smt2
index 7ae60f2db..f4cf5c055 100755
--- a/test/regress/regress0/strings/indexof-sym-simp.smt2
+++ b/test/regress/regress0/strings/indexof-sym-simp.smt2
@@ -1,10 +1,10 @@
-(set-logic ALL_SUPPORTED)

-(set-info :status unsat)

-(set-option :strings-exp true)

-(declare-fun s () String)

-(declare-fun t () String)

-(declare-fun r () String)

-; solvable if we do equality reasoning over str.indexof

-(assert (= t s))

-(assert (not (= (str.indexof t r 0) (str.indexof s r 0))))

+(set-logic ALL_SUPPORTED)
+(set-info :status unsat)
+(set-option :strings-exp true)
+(declare-fun s () String)
+(declare-fun t () String)
+(declare-fun r () String)
+; solvable if we do equality reasoning over str.indexof
+(assert (= t s))
+(assert (not (= (str.indexof t r 0) (str.indexof s r 0))))
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/kaluza-fl.smt2 b/test/regress/regress0/strings/kaluza-fl.smt2
index ce3af9e74..04775d61c 100755
--- a/test/regress/regress0/strings/kaluza-fl.smt2
+++ b/test/regress/regress0/strings/kaluza-fl.smt2
@@ -1,97 +1,97 @@
-(set-logic QF_S)

-(set-info :status sat)

-

-(declare-fun I0_15 () Int)

-(declare-fun I0_18 () Int)

-(declare-fun I0_2 () Int)

-(declare-fun I0_4 () Int)

-(declare-fun I0_6 () Int)

-(declare-fun PCTEMP_LHS_1 () Int)

-(declare-fun PCTEMP_LHS_2 () Int)

-(declare-fun PCTEMP_LHS_3 () Int)

-(declare-fun PCTEMP_LHS_4 () Int)

-(declare-fun PCTEMP_LHS_5 () Int)

-(declare-fun T0_15 () String)

-(declare-fun T0_18 () String)

-(declare-fun T0_2 () String)

-(declare-fun T0_4 () String)

-(declare-fun T0_6 () String)

-(declare-fun T1_15 () String)

-(declare-fun T1_18 () String)

-(declare-fun T1_2 () String)

-(declare-fun T1_4 () String)

-(declare-fun T1_6 () String)

-(declare-fun T2_15 () String)

-(declare-fun T2_18 () String)

-(declare-fun T2_2 () String)

-(declare-fun T2_4 () String)

-(declare-fun T2_6 () String)

-(declare-fun T3_15 () String)

-(declare-fun T3_18 () String)

-(declare-fun T3_2 () String)

-(declare-fun T3_4 () String)

-(declare-fun T3_6 () String)

-(declare-fun T4_15 () String)

-(declare-fun T4_18 () String)

-(declare-fun T4_2 () String)

-(declare-fun T4_4 () String)

-(declare-fun T4_6 () String)

-(declare-fun T5_15 () String)

-(declare-fun T5_18 () String)

-(declare-fun T5_2 () String)

-(declare-fun T5_4 () String)

-(declare-fun T5_6 () String)

-(declare-fun T_4 () Bool)

-(declare-fun T_5 () Bool)

-(declare-fun T_6 () Bool)

-(declare-fun T_7 () Bool)

-(declare-fun T_8 () Bool)

-(declare-fun T_9 () Bool)

-(declare-fun T_SELECT_1 () Bool)

-(declare-fun T_SELECT_2 () Bool)

-(declare-fun T_SELECT_3 () Bool)

-(declare-fun T_SELECT_4 () Bool)

-(declare-fun T_SELECT_5 () Bool)

-(declare-fun T_a () Bool)

-(declare-fun T_c () Bool)

-(declare-fun T_e () Bool)

-(declare-fun var_0xINPUT_12454 () String)

-

-(assert (= T_SELECT_1 (not (= PCTEMP_LHS_1 (- 1)))))

-(assert (ite T_SELECT_1 

-  (and (= PCTEMP_LHS_1 (+ I0_2 0))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= I0_2 (str.len T4_2))(= 0 (str.len T0_2))(= T1_2 (str.++ T2_2 T3_2))(= T2_2 (str.++ T4_2 T5_2))(= T5_2 "__utma=169413169.")(not (str.in.re T4_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "."))))) 

-  (and (= PCTEMP_LHS_1 (- 1))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= 0 (str.len T0_2))(not (str.in.re T1_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re ".")))))))

-(assert (= T_SELECT_2 (not (= PCTEMP_LHS_2 (- 1)))))

-(assert (ite T_SELECT_2 

-  (and (= PCTEMP_LHS_2 (+ I0_4 0))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= I0_4 (str.len T4_4))(= 0 (str.len T0_4))(= T1_4 (str.++ T2_4 T3_4))(= T2_4 (str.++ T4_4 T5_4))(= T5_4 "__utmb=169413169")(not (str.in.re T4_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) 

-  (and (= PCTEMP_LHS_2 (- 1))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= 0 (str.len T0_4))(not (str.in.re T1_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))

-(assert (= T_SELECT_3 (not (= PCTEMP_LHS_3 (- 1)))))

-(assert (ite T_SELECT_3 

-  (and (= PCTEMP_LHS_3 (+ I0_6 0))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= I0_6 (str.len T4_6))(= 0 (str.len T0_6))(= T1_6 (str.++ T2_6 T3_6))(= T2_6 (str.++ T4_6 T5_6))(= T5_6 "__utmc=169413169")(not (str.in.re T4_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) 

-  (and (= PCTEMP_LHS_3 (- 1))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= 0 (str.len T0_6))(not (str.in.re T1_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))

-(assert (= T_4 (<= 0 PCTEMP_LHS_1)))

-(assert T_4)

-(assert (= T_5 (<= 0 PCTEMP_LHS_2)))

-(assert T_5)

-(assert (= T_6 (<= 0 PCTEMP_LHS_3)))

-(assert T_6)

-(assert (= T_7 (= "" var_0xINPUT_12454)))

-(assert (= T_8 (not T_7)))

-(assert T_8)

-(assert (= T_9 (= var_0xINPUT_12454 "")))

-(assert (= T_a (not T_9)))

-(assert T_a)

-(assert (= T_SELECT_4 (not (= PCTEMP_LHS_4 (- 1)))))

-(assert (ite T_SELECT_4 

-  (and (= PCTEMP_LHS_4 (+ I0_15 0))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= I0_15 (str.len T4_15))(= 0 (str.len T0_15))(= T1_15 (str.++ T2_15 T3_15))(= T2_15 (str.++ T4_15 T5_15))(= T5_15 "__utmb=169413169")(not (str.in.re T4_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) 

-  (and (= PCTEMP_LHS_4 (- 1))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= 0 (str.len T0_15))(not (str.in.re T1_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))

-(assert (= T_c (< (- 1) PCTEMP_LHS_4)))

-(assert T_c)

-(assert (= T_SELECT_5 (not (= PCTEMP_LHS_5 (- 1)))))

-(assert (ite T_SELECT_5 

-  (and (= PCTEMP_LHS_5 (+ I0_18 PCTEMP_LHS_4))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= I0_18 (str.len T4_18))(= PCTEMP_LHS_4 (str.len T0_18))(= T1_18 (str.++ T2_18 T3_18))(= T2_18 (str.++ T4_18 T5_18))(= T5_18 ";")(not (str.in.re T4_18 (str.to.re ";")))) 

-  (and (= PCTEMP_LHS_5 (- 1))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= PCTEMP_LHS_4 (str.len T0_18))(not (str.in.re T1_18 (str.to.re ";"))))))

-(assert (= T_e (< PCTEMP_LHS_5 0)))

-(assert T_e)

-

-(check-sat)

+(set-logic QF_S)
+(set-info :status sat)
+
+(declare-fun I0_15 () Int)
+(declare-fun I0_18 () Int)
+(declare-fun I0_2 () Int)
+(declare-fun I0_4 () Int)
+(declare-fun I0_6 () Int)
+(declare-fun PCTEMP_LHS_1 () Int)
+(declare-fun PCTEMP_LHS_2 () Int)
+(declare-fun PCTEMP_LHS_3 () Int)
+(declare-fun PCTEMP_LHS_4 () Int)
+(declare-fun PCTEMP_LHS_5 () Int)
+(declare-fun T0_15 () String)
+(declare-fun T0_18 () String)
+(declare-fun T0_2 () String)
+(declare-fun T0_4 () String)
+(declare-fun T0_6 () String)
+(declare-fun T1_15 () String)
+(declare-fun T1_18 () String)
+(declare-fun T1_2 () String)
+(declare-fun T1_4 () String)
+(declare-fun T1_6 () String)
+(declare-fun T2_15 () String)
+(declare-fun T2_18 () String)
+(declare-fun T2_2 () String)
+(declare-fun T2_4 () String)
+(declare-fun T2_6 () String)
+(declare-fun T3_15 () String)
+(declare-fun T3_18 () String)
+(declare-fun T3_2 () String)
+(declare-fun T3_4 () String)
+(declare-fun T3_6 () String)
+(declare-fun T4_15 () String)
+(declare-fun T4_18 () String)
+(declare-fun T4_2 () String)
+(declare-fun T4_4 () String)
+(declare-fun T4_6 () String)
+(declare-fun T5_15 () String)
+(declare-fun T5_18 () String)
+(declare-fun T5_2 () String)
+(declare-fun T5_4 () String)
+(declare-fun T5_6 () String)
+(declare-fun T_4 () Bool)
+(declare-fun T_5 () Bool)
+(declare-fun T_6 () Bool)
+(declare-fun T_7 () Bool)
+(declare-fun T_8 () Bool)
+(declare-fun T_9 () Bool)
+(declare-fun T_SELECT_1 () Bool)
+(declare-fun T_SELECT_2 () Bool)
+(declare-fun T_SELECT_3 () Bool)
+(declare-fun T_SELECT_4 () Bool)
+(declare-fun T_SELECT_5 () Bool)
+(declare-fun T_a () Bool)
+(declare-fun T_c () Bool)
+(declare-fun T_e () Bool)
+(declare-fun var_0xINPUT_12454 () String)
+
+(assert (= T_SELECT_1 (not (= PCTEMP_LHS_1 (- 1)))))
+(assert (ite T_SELECT_1 
+  (and (= PCTEMP_LHS_1 (+ I0_2 0))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= I0_2 (str.len T4_2))(= 0 (str.len T0_2))(= T1_2 (str.++ T2_2 T3_2))(= T2_2 (str.++ T4_2 T5_2))(= T5_2 "__utma=169413169.")(not (str.in.re T4_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "."))))) 
+  (and (= PCTEMP_LHS_1 (- 1))(= var_0xINPUT_12454 (str.++ T0_2 T1_2))(= 0 (str.len T0_2))(not (str.in.re T1_2 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "a") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re ".")))))))
+(assert (= T_SELECT_2 (not (= PCTEMP_LHS_2 (- 1)))))
+(assert (ite T_SELECT_2 
+  (and (= PCTEMP_LHS_2 (+ I0_4 0))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= I0_4 (str.len T4_4))(= 0 (str.len T0_4))(= T1_4 (str.++ T2_4 T3_4))(= T2_4 (str.++ T4_4 T5_4))(= T5_4 "__utmb=169413169")(not (str.in.re T4_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) 
+  (and (= PCTEMP_LHS_2 (- 1))(= var_0xINPUT_12454 (str.++ T0_4 T1_4))(= 0 (str.len T0_4))(not (str.in.re T1_4 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))
+(assert (= T_SELECT_3 (not (= PCTEMP_LHS_3 (- 1)))))
+(assert (ite T_SELECT_3 
+  (and (= PCTEMP_LHS_3 (+ I0_6 0))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= I0_6 (str.len T4_6))(= 0 (str.len T0_6))(= T1_6 (str.++ T2_6 T3_6))(= T2_6 (str.++ T4_6 T5_6))(= T5_6 "__utmc=169413169")(not (str.in.re T4_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) 
+  (and (= PCTEMP_LHS_3 (- 1))(= var_0xINPUT_12454 (str.++ T0_6 T1_6))(= 0 (str.len T0_6))(not (str.in.re T1_6 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "c") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))
+(assert (= T_4 (<= 0 PCTEMP_LHS_1)))
+(assert T_4)
+(assert (= T_5 (<= 0 PCTEMP_LHS_2)))
+(assert T_5)
+(assert (= T_6 (<= 0 PCTEMP_LHS_3)))
+(assert T_6)
+(assert (= T_7 (= "" var_0xINPUT_12454)))
+(assert (= T_8 (not T_7)))
+(assert T_8)
+(assert (= T_9 (= var_0xINPUT_12454 "")))
+(assert (= T_a (not T_9)))
+(assert T_a)
+(assert (= T_SELECT_4 (not (= PCTEMP_LHS_4 (- 1)))))
+(assert (ite T_SELECT_4 
+  (and (= PCTEMP_LHS_4 (+ I0_15 0))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= I0_15 (str.len T4_15))(= 0 (str.len T0_15))(= T1_15 (str.++ T2_15 T3_15))(= T2_15 (str.++ T4_15 T5_15))(= T5_15 "__utmb=169413169")(not (str.in.re T4_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9"))))) 
+  (and (= PCTEMP_LHS_4 (- 1))(= var_0xINPUT_12454 (str.++ T0_15 T1_15))(= 0 (str.len T0_15))(not (str.in.re T1_15 (re.++ (str.to.re "_") (str.to.re "_") (str.to.re "u") (str.to.re "t") (str.to.re "m") (str.to.re "b") (str.to.re "=") (str.to.re "1") (str.to.re "6") (str.to.re "9") (str.to.re "4") (str.to.re "1") (str.to.re "3") (str.to.re "1") (str.to.re "6") (str.to.re "9")))))))
+(assert (= T_c (< (- 1) PCTEMP_LHS_4)))
+(assert T_c)
+(assert (= T_SELECT_5 (not (= PCTEMP_LHS_5 (- 1)))))
+(assert (ite T_SELECT_5 
+  (and (= PCTEMP_LHS_5 (+ I0_18 PCTEMP_LHS_4))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= I0_18 (str.len T4_18))(= PCTEMP_LHS_4 (str.len T0_18))(= T1_18 (str.++ T2_18 T3_18))(= T2_18 (str.++ T4_18 T5_18))(= T5_18 ";")(not (str.in.re T4_18 (str.to.re ";")))) 
+  (and (= PCTEMP_LHS_5 (- 1))(= var_0xINPUT_12454 (str.++ T0_18 T1_18))(= PCTEMP_LHS_4 (str.len T0_18))(not (str.in.re T1_18 (str.to.re ";"))))))
+(assert (= T_e (< PCTEMP_LHS_5 0)))
+(assert T_e)
+
+(check-sat)
diff --git a/test/regress/regress0/strings/norn-ab.smt2 b/test/regress/regress0/strings/norn-ab.smt2
index db7aac732..48d889847 100755
--- a/test/regress/regress0/strings/norn-ab.smt2
+++ b/test/regress/regress0/strings/norn-ab.smt2
@@ -1,25 +1,25 @@
-(set-logic QF_SLIA)

-(set-info :status unsat)

-(set-option :strings-exp true)

-

-(declare-fun var_0 () String)

-(declare-fun var_1 () String)

-(declare-fun var_2 () String)

-(declare-fun var_3 () String)

-(declare-fun var_4 () String)

-(declare-fun var_5 () String)

-(declare-fun var_6 () String)

-(declare-fun var_7 () String)

-(declare-fun var_8 () String)

-(declare-fun var_9 () String)

-(declare-fun var_10 () String)

-(declare-fun var_11 () String)

-(declare-fun var_12 () String)

-

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

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

-(assert (str.in.re var_4 (re.* (re.range "a" "u"))))

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

-(assert (not (str.in.re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))))

-(assert (and (<= 0  (str.len var_4)) (not (not (exists ((v Int)) (= (* v 2 ) (+ (str.len var_4) 2 )))))))

+(set-logic QF_SLIA)
+(set-info :status unsat)
+(set-option :strings-exp true)
+
+(declare-fun var_0 () String)
+(declare-fun var_1 () String)
+(declare-fun var_2 () String)
+(declare-fun var_3 () String)
+(declare-fun var_4 () String)
+(declare-fun var_5 () String)
+(declare-fun var_6 () String)
+(declare-fun var_7 () String)
+(declare-fun var_8 () String)
+(declare-fun var_9 () String)
+(declare-fun var_10 () String)
+(declare-fun var_11 () String)
+(declare-fun var_12 () String)
+
+(assert (str.in.re var_4 (re.++ (str.to.re "a") (re.* (str.to.re "b")))))
+(assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (str.to.re "b"))))
+(assert (str.in.re var_4 (re.* (re.range "a" "u"))))
+(assert (str.in.re var_4 (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
+(assert (not (str.in.re (str.++ "a" var_4 "b" ) (re.++ (re.* (str.to.re "a")) (re.++ (str.to.re "b") (re.* (str.to.re "b")))))))
+(assert (and (<= 0  (str.len var_4)) (not (not (exists ((v Int)) (= (* v 2 ) (+ (str.len var_4) 2 )))))))
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/norn-simp-rew.smt2 b/test/regress/regress0/strings/norn-simp-rew.smt2
index d0cd69cb0..45f7ede94 100755
--- a/test/regress/regress0/strings/norn-simp-rew.smt2
+++ b/test/regress/regress0/strings/norn-simp-rew.smt2
@@ -1,29 +1,29 @@
-(set-logic QF_SLIA)

-(set-option :strings-exp true)

-(set-info :status unsat)

-

-(declare-fun var_0 () String)

-(declare-fun var_1 () String)

-(declare-fun var_2 () String)

-(declare-fun var_3 () String)

-(declare-fun var_4 () String)

-(declare-fun var_5 () String)

-(declare-fun var_6 () String)

-(declare-fun var_7 () String)

-(declare-fun var_8 () String)

-(declare-fun var_9 () String)

-(declare-fun var_10 () String)

-(declare-fun var_11 () String)

-(declare-fun var_12 () String)

-

-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "a")) (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "b")) (re.union (str.to.re "z") (str.to.re "a")))))) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))

-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "b") (str.to.re "a"))) (str.to.re "z"))))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "b") (str.to.re "a")))))))

-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "z") (str.to.re "b"))) (str.to.re "a")))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "z") (str.to.re "b")))))))

-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to.re "z") (re.++ (re.union (str.to.re "b") (str.to.re "a")) (re.union (str.to.re "z") (str.to.re "b"))))) (re.union (str.to.re "b") (str.to.re "a")))))

-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.* (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "z")) (str.to.re "b"))))))

-(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (str.to.re "z"))) (str.to.re "b"))))

-(assert (str.in.re (str.++ "a" var_8 ) (re.* (re.range "a" "u"))))

-(assert (str.in.re var_8 (re.* (re.range "a" "u"))))

-(assert (str.in.re var_7 (re.* (re.range "a" "u"))))

-(assert (not (str.in.re (str.++ "b" var_7 ) (re.* (re.range "a" "u")))))

+(set-logic QF_SLIA)
+(set-option :strings-exp true)
+(set-info :status unsat)
+
+(declare-fun var_0 () String)
+(declare-fun var_1 () String)
+(declare-fun var_2 () String)
+(declare-fun var_3 () String)
+(declare-fun var_4 () String)
+(declare-fun var_5 () String)
+(declare-fun var_6 () String)
+(declare-fun var_7 () String)
+(declare-fun var_8 () String)
+(declare-fun var_9 () String)
+(declare-fun var_10 () String)
+(declare-fun var_11 () String)
+(declare-fun var_12 () String)
+
+(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (re.union (str.to.re "z") (str.to.re "a")) (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "b")) (re.union (str.to.re "z") (str.to.re "a")))))) (re.++ (str.to.re "b") (re.* (str.to.re "b"))))))
+(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to.re "a") (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "b") (str.to.re "a"))) (str.to.re "z"))))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "b") (str.to.re "a")))))))
+(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (re.++ (re.* (re.union (str.to.re "z") (str.to.re "b"))) (str.to.re "a")))) (re.++ (str.to.re "b") (re.* (re.union (str.to.re "z") (str.to.re "b")))))))
+(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.union (str.to.re "z") (re.++ (re.union (str.to.re "b") (str.to.re "a")) (re.union (str.to.re "z") (str.to.re "b"))))) (re.union (str.to.re "b") (str.to.re "a")))))
+(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.* (re.++ (str.to.re "b") (re.++ (re.* (str.to.re "z")) (str.to.re "b"))))))
+(assert (str.in.re (str.++ var_7 "z" var_8 ) (re.++ (re.* (re.++ (str.to.re "b") (str.to.re "z"))) (str.to.re "b"))))
+(assert (str.in.re (str.++ "a" var_8 ) (re.* (re.range "a" "u"))))
+(assert (str.in.re var_8 (re.* (re.range "a" "u"))))
+(assert (str.in.re var_7 (re.* (re.range "a" "u"))))
+(assert (not (str.in.re (str.++ "b" var_7 ) (re.* (re.range "a" "u")))))
 (check-sat)
\ No newline at end of file
diff --git a/test/regress/regress0/strings/unsound-0908.smt2 b/test/regress/regress0/strings/unsound-0908.smt2
index cbaf5f5e4..2b25e6dc8 100755
--- a/test/regress/regress0/strings/unsound-0908.smt2
+++ b/test/regress/regress0/strings/unsound-0908.smt2
@@ -1,12 +1,12 @@
-(set-logic QF_S)

-(set-info :status sat)

-(declare-const x String)

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

-;(assert (= x "X"))

-(assert

-    (or 

-      (not (> (str.len x) 1))

-      (= (str.at x 1) "Z")

-    )

-)

-(check-sat)

+(set-logic QF_S)
+(set-info :status sat)
+(declare-const x String)
+(assert (= (str.len x) 1))
+;(assert (= x "X"))
+(assert
+    (or 
+      (not (> (str.len x) 1))
+      (= (str.at x 1) "Z")
+    )
+)
+(check-sat)
diff --git a/test/regress/regress0/uf/cnf-and-neg.smt2 b/test/regress/regress0/uf/cnf-and-neg.smt2
index 711740f67..470a88809 100755
--- a/test/regress/regress0/uf/cnf-and-neg.smt2
+++ b/test/regress/regress0/uf/cnf-and-neg.smt2
@@ -1,11 +1,11 @@
-(set-logic QF_UF)

-(set-info :status unsat)

-(declare-sort I 0)

-(declare-fun a () I)

-(declare-fun b () I)

-(declare-fun c () I)

-(declare-fun f (I) I)

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

-(assert (not (= (f a) (f c))))

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

-(check-sat)

+(set-logic QF_UF)
+(set-info :status unsat)
+(declare-sort I 0)
+(declare-fun a () I)
+(declare-fun b () I)
+(declare-fun c () I)
+(declare-fun f (I) I)
+(assert (not (= (f a) (f b))))
+(assert (not (= (f a) (f c))))
+(assert (not (and (not (= a b)) (not (= a c)))))
+(check-sat)
diff --git a/test/regress/regress0/uf/cnf_abc.smt2 b/test/regress/regress0/uf/cnf_abc.smt2
index 5d011f44c..46a4b7dbf 100755
--- a/test/regress/regress0/uf/cnf_abc.smt2
+++ b/test/regress/regress0/uf/cnf_abc.smt2
@@ -1,168 +1,168 @@
-(set-logic QF_UF)

-(set-info :status unsat)

-

-(declare-sort I 0)

-(declare-fun f (I I) I)

-(declare-fun a () I)

-(declare-fun b () I)

-(declare-fun c () I)

-

-

-

-(assert

- (or

-  (= (f a a) a)

-  (= (f a a) b)

-  (= (f a a) c)

-  ))

-

-(assert

- (or

-  (= (f a b) a)

-  (= (f a b) b)

-  (= (f a b) c)

-  ))

-

-(assert

- (or

-  (= (f a c) a)

-  (= (f a c) b)

-  (= (f a c) c)

-  ))

-

-(assert

- (or

-  (= (f b a) a)

-  (= (f b a) b)

-  (= (f b a) c)

-  ))

-

-(assert

- (or

-  (= (f b b) a)

-  (= (f b b) b)

-  (= (f b b) c)

-  ))

-

-(assert

- (or

-  (= (f b c) a)

-  (= (f b c) b)

-  (= (f b c) c)

-  ))

-

-

-(assert

- (or

-  (= (f c a) a)

-  (= (f c a) b)

-  (= (f c a) c)

-  ))

-

-(assert

- (or

-  (= (f c b) a)

-  (= (f c b) b)

-  (= (f c b) c)

-  ))

-

-(assert

- (or

-  (= (f c c) a)

-  (= (f c c) b)

-  (= (f c c) c)

-  ))

-

-

-

-(assert

- (or

-  (= (f a a) a)

-  (= (f b b) a)

-  (= (f c c) a)

-  ))

-

-(assert

- (or

-  (= (f a a) b)

-  (= (f b b) b)

-  (= (f c c) b)

-  ))

-

-(assert

- (or

-  (= (f a a) c)

-  (= (f b b) c)

-  (= (f c c) c)

-  ))

-

-

-

-(assert

- (or

-  (= (f a a) a)

-  (= (f b a) b)

-  (= (f c a) c)

-  ))

-

-(assert

- (or

-  (= (f a b) a)

-  (= (f b b) b)

-  (= (f c b) c)

-  ))

-

-(assert

- (or

-  (= (f a c) a)

-  (= (f b c) b)

-  (= (f c c) c)

-  ))

-

-

-

-

-(assert (not (= (f a a) a)))

-(assert (not (= (f b b) b)))

-(assert (not (= (f c c) c)))                

-

-

-(assert

- (or

-  (not (= (f a (f a a)) a))

-  (not (= (f a (f a b)) b))

-  (not (= (f a (f a c)) c))

-  ))

-

-(assert

- (or

-  (not (= (f b (f b a)) a)) 

-  (not (= (f b (f b b)) b))

-  (not (= (f b (f b c)) c))

-  ))

-

-(assert

- (or

-  (not (= (f c (f c a)) a)) 

-  (not (= (f c (f c b)) b))

-  (not (= (f c (f c c)) c))

-  ))

-

-

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

-(assert  (not (= (f a a) (f c a))))

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

-

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

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

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

-

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

-(assert  (not (= (f a c) (f c c))))

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

-

-

-

-(check-sat)

-

-(exit)

+(set-logic QF_UF)
+(set-info :status unsat)
+
+(declare-sort I 0)
+(declare-fun f (I I) I)
+(declare-fun a () I)
+(declare-fun b () I)
+(declare-fun c () I)
+
+
+
+(assert
+ (or
+  (= (f a a) a)
+  (= (f a a) b)
+  (= (f a a) c)
+  ))
+
+(assert
+ (or
+  (= (f a b) a)
+  (= (f a b) b)
+  (= (f a b) c)
+  ))
+
+(assert
+ (or
+  (= (f a c) a)
+  (= (f a c) b)
+  (= (f a c) c)
+  ))
+
+(assert
+ (or
+  (= (f b a) a)
+  (= (f b a) b)
+  (= (f b a) c)
+  ))
+
+(assert
+ (or
+  (= (f b b) a)
+  (= (f b b) b)
+  (= (f b b) c)
+  ))
+
+(assert
+ (or
+  (= (f b c) a)
+  (= (f b c) b)
+  (= (f b c) c)
+  ))
+
+
+(assert
+ (or
+  (= (f c a) a)
+  (= (f c a) b)
+  (= (f c a) c)
+  ))
+
+(assert
+ (or
+  (= (f c b) a)
+  (= (f c b) b)
+  (= (f c b) c)
+  ))
+
+(assert
+ (or
+  (= (f c c) a)
+  (= (f c c) b)
+  (= (f c c) c)
+  ))
+
+
+
+(assert
+ (or
+  (= (f a a) a)
+  (= (f b b) a)
+  (= (f c c) a)
+  ))
+
+(assert
+ (or
+  (= (f a a) b)
+  (= (f b b) b)
+  (= (f c c) b)
+  ))
+
+(assert
+ (or
+  (= (f a a) c)
+  (= (f b b) c)
+  (= (f c c) c)
+  ))
+
+
+
+(assert
+ (or
+  (= (f a a) a)
+  (= (f b a) b)
+  (= (f c a) c)
+  ))
+
+(assert
+ (or
+  (= (f a b) a)
+  (= (f b b) b)
+  (= (f c b) c)
+  ))
+
+(assert
+ (or
+  (= (f a c) a)
+  (= (f b c) b)
+  (= (f c c) c)
+  ))
+
+
+
+
+(assert (not (= (f a a) a)))
+(assert (not (= (f b b) b)))
+(assert (not (= (f c c) c)))                
+
+
+(assert
+ (or
+  (not (= (f a (f a a)) a))
+  (not (= (f a (f a b)) b))
+  (not (= (f a (f a c)) c))
+  ))
+
+(assert
+ (or
+  (not (= (f b (f b a)) a)) 
+  (not (= (f b (f b b)) b))
+  (not (= (f b (f b c)) c))
+  ))
+
+(assert
+ (or
+  (not (= (f c (f c a)) a)) 
+  (not (= (f c (f c b)) b))
+  (not (= (f c (f c c)) c))
+  ))
+
+
+(assert  (not (= (f a a) (f b a))))
+(assert  (not (= (f a a) (f c a))))
+(assert  (not (= (f b a) (f c a))))
+
+(assert  (not (= (f a b) (f b b))))
+(assert  (not (= (f a b) (f c b))))
+(assert  (not (= (f b b) (f c b))))
+
+(assert  (not (= (f a c) (f b c))))
+(assert  (not (= (f a c) (f c c))))
+(assert  (not (= (f b c) (f c c))))
+
+
+
+(check-sat)
+
+(exit)