Convert V1 Sygus files to V2. (#4136)

100 files changed, 720 insertions, 753 deletions

diff --git a/test/regress/regress1/rr-verify/bool-crci.sy b/test/regress/regress1/rr-verify/bool-crci.sy
index 955245f87..75837695d 100644
--- a/test/regress/regress1/rr-verify/bool-crci.sy
+++ b/test/regress/regress1/rr-verify/bool-crci.sy
@@ -1,11 +1,12 @@
-; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=3 --sygus-rr-verify-abort --no-sygus-sym-break
 ; EXPECT: (error "Maximum term size (3) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1
 
 (set-logic BV)
 
-(synth-fun f ( (x Bool) (y Bool) (z Bool) (w Bool) ) Bool 
+(synth-fun f ( (x Bool) (y Bool) (z Bool) (w Bool) ) Bool
+ ( (Start Bool) (depth1 Bool) (depth2 Bool) (depth3 Bool) (depth4 Bool) )
  ((Start Bool (
    (and depth1 depth1)
    (not depth1)
diff --git a/test/regress/regress1/rr-verify/bv-term-32.sy b/test/regress/regress1/rr-verify/bv-term-32.sy
index 6c07bd8aa..9dfb19451 100644
--- a/test/regress/regress1/rr-verify/bv-term-32.sy
+++ b/test/regress/regress1/rr-verify/bv-term-32.sy
@@ -1,13 +1,14 @@
-; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1
 
 (set-logic BV)
 
-(synth-fun f ((s (BitVec 32)) (t (BitVec 32))) (BitVec 32)
+(synth-fun f ((s (_ BitVec 32)) (t (_ BitVec 32))) (_ BitVec 32)
+  ((Start (_ BitVec 32)))
   (
-   (Start (BitVec 32) (
+   (Start (_ BitVec 32) (
      s
      t
      #x00000000
diff --git a/test/regress/regress1/rr-verify/bv-term.sy b/test/regress/regress1/rr-verify/bv-term.sy
index f310396d2..9a11128d7 100644
--- a/test/regress/regress1/rr-verify/bv-term.sy
+++ b/test/regress/regress1/rr-verify/bv-term.sy
@@ -1,14 +1,15 @@
-; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break
-; COMMAND-LINE: --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr-synth --sygus-samples=1000 --sygus-abort-size=2 --sygus-rr-verify-abort --sygus-rr-synth-check
 ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite|\(rewrite)'
 ; EXIT: 1
 
 (set-logic BV)
 
-(synth-fun f ((s (BitVec 4)) (t (BitVec 4))) (BitVec 4)
+(synth-fun f ((s (_ BitVec 4)) (t (_ BitVec 4))) (_ BitVec 4)
+  ((Start (_ BitVec 4)))
   (
-   (Start (BitVec 4) (
+   (Start (_ BitVec 4) (
      s
      t
      #x0
diff --git a/test/regress/regress1/rr-verify/fp-arith.sy b/test/regress/regress1/rr-verify/fp-arith.sy
index e8b97d610..30828ca76 100644
--- a/test/regress/regress1/rr-verify/fp-arith.sy
+++ b/test/regress/regress1/rr-verify/fp-arith.sy
@@ -1,5 +1,5 @@
 ; REQUIRES: symfpu
-; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
 ; EXIT: 1
@@ -13,6 +13,7 @@
 (define-fun fp_nan () Float16 (_ NaN 5 11))
 
 (synth-fun f ( (r RoundingMode) (x Float16) (y Float16)) Float16
+((Start Float16))
 (
  (Start Float16 (
   (fp.abs Start)
diff --git a/test/regress/regress1/rr-verify/fp-bool.sy b/test/regress/regress1/rr-verify/fp-bool.sy
index bf0692f7d..6704198c3 100644
--- a/test/regress/regress1/rr-verify/fp-bool.sy
+++ b/test/regress/regress1/rr-verify/fp-bool.sy
@@ -1,5 +1,5 @@
 ; REQUIRES: symfpu
-; COMMAND-LINE: --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=0 --sygus-rr-synth-check --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break --fp-exp
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(rewrite)'
 ; EXIT: 1
@@ -13,6 +13,7 @@
 (define-fun fp_nan () Float16 (_ NaN 5 11))
 
 (synth-fun f ( (r RoundingMode) (x Float16) (y Float16)) Bool
+((Start Bool) (FpOp Float16))
 (
  (Start Bool (
   (fp.isNaN FpOp)
diff --git a/test/regress/regress1/rr-verify/string-term.sy b/test/regress/regress1/rr-verify/string-term.sy
index 8f6593148..404719f6c 100644
--- a/test/regress/regress1/rr-verify/string-term.sy
+++ b/test/regress/regress1/rr-verify/string-term.sy
@@ -1,24 +1,25 @@
-; COMMAND-LINE: --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
+; COMMAND-LINE: --lang=sygus2 --sygus-rr --sygus-samples=1000 --sygus-abort-size=1 --sygus-rr-verify-abort --no-sygus-sym-break
 ; EXPECT: (error "Maximum term size (1) for enumerative SyGuS exceeded.")
 ; SCRUBBER: grep -v -E '(\(define-fun|\(candidate-rewrite)'
 ; EXIT: 1
 
 (set-logic SLIA)
 
-(synth-fun f ((x String) (y String) (z Int)) String (
+(synth-fun f ((x String) (y String) (z Int)) String
+((Start String) (StartInt Int)) (
 (Start String (
   x y "A" "B" ""
   (str.++ Start Start)
   (str.replace Start Start Start)
   (str.at Start StartInt)
-  (int.to.str StartInt)
+  (str.from_int StartInt)
   (str.substr Start StartInt StartInt)))
 (StartInt Int (
   0 1 z
   (+ StartInt StartInt)
   (- StartInt StartInt)
   (str.len Start)
-  (str.to.int Start)
+  (str.to_int Start)
   (str.indexof Start Start StartInt)))
 ))
 
diff --git a/test/regress/regress1/sygus/Base16_1.sy b/test/regress/regress1/sygus/Base16_1.sy
index b54c7688b..b84e5bb48 100644
--- a/test/regress/regress1/sygus/Base16_1.sy
+++ b/test/regress/regress1/sygus/Base16_1.sy
@@ -1,17 +1,18 @@
 ; EXPECT: unsat
-; COMMAND-LINE:  --sygus-qe-preproc --cbqi-full --sygus-out=status --cegqi-si=all
+; COMMAND-LINE: --lang=sygus2 --sygus-qe-preproc --cbqi-full --sygus-out=status --cegqi-si=all
 (set-logic BV)
 
-(define-fun B ((h (BitVec 8)) (l (BitVec 8)) (v (BitVec 8))) (BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l))))
+(define-fun B ((h (_ BitVec 8)) (l (_ BitVec 8)) (v (_ BitVec 8))) (_ BitVec 8) (bvlshr (bvshl v (bvsub #x07 h)) (bvsub #x07 (bvsub h l))))
 
-(define-fun E ((x (BitVec 8))) (BitVec 8)  (bvadd x #x41))
+(define-fun E ((x (_ BitVec 8))) (_ BitVec 8)  (bvadd x #x41))
 
-(define-fun f ((x (BitVec 8))) (BitVec 8) (bvsub x #x41))
+(define-fun f ((x (_ BitVec 8))) (_ BitVec 8) (bvsub x #x41))
 
-(define-fun d ((x (BitVec 8))) Bool (bvule x #x3f))
+(define-fun d ((x (_ BitVec 8))) Bool (bvule x #x3f))
 
-(synth-fun D ((x (BitVec 8)) (y (BitVec 8)) ) (BitVec 8)
-    	((Start (BitVec 8) (
+(synth-fun D ((x (_ BitVec 8)) (y (_ BitVec 8)) ) (_ BitVec 8)
+		((Start (_ BitVec 8)) (Const (_ BitVec 8)))
+		((Start (_ BitVec 8) (
 			(f Start) x y Const
 				(bvshl Start Start) 	 (bvnot Start)
 						 (bvand Start Start)
@@ -22,13 +23,11 @@
 						 (bvlshr Start Start)
 						 (bvsub Start Start)
 			))
-	 (Const (BitVec 8) (#x01 #x03 #x06 #x07 #x04 #x05 #x02 #x00))
+	 (Const (_ BitVec 8) (#x01 #x03 #x06 #x07 #x04 #x05 #x02 #x00))
 ))
 
-(declare-var x (BitVec 8))
+(declare-var x (_ BitVec 8))
 (constraint  (= x (D (E (B #x07 #x04 x) ) (E  (B #x03 #x00 x))  )) )
 
 ; notice we don't have solution reconstruction for this
-(check-synth)    
-
-
+(check-synth)
diff --git a/test/regress/regress1/sygus/VC22_a.sy b/test/regress/regress1/sygus/VC22_a.sy
index ce437bc34..f60f661dd 100644
--- a/test/regress/regress1/sygus/VC22_a.sy
+++ b/test/regress/regress1/sygus/VC22_a.sy
@@ -1,9 +1,10 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
-; COMMAND-LINE: --sygus-out=status --cegis-sample=use
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegis-sample=use
 (set-logic LIA)
 
 (synth-fun f ((x1 Int) (x2 Int)) Int
+	((Start Int) (StartBool Bool))
 	((Start Int (0 1 x1 x2
 				(ite StartBool Start Start)))
 		(StartBool Bool ((= Start Start)))))
@@ -24,7 +25,6 @@
 (define-fun InVorZero ((v Int)) Bool
 	(or (InV1 v) (Zero v)))
 
-
 (define-fun UnsafeSame ((x1 Int) (x2 Int) (v1 Int) (v2 Int)) Bool
 	(or (and (>= x1 x2) (>= (+ x2 v2) (+ x1 v1)))
 		(and (>= x2 x1) (>= (+ x1 v1) (+ x2 v2)))))
@@ -58,4 +58,3 @@
 (constraint (or (Bad x1 x2) (not (Zero (f x1 x2)))))
 
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/abv.sy b/test/regress/regress1/sygus/abv.sy
index d9a8a019c..d42553c1b 100644
--- a/test/regress/regress1/sygus/abv.sy
+++ b/test/regress/regress1/sygus/abv.sy
@@ -1,61 +1,66 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic ABV)
 
-(define-sort AddrSort () (BitVec 32))
-(define-sort ValSort () (BitVec 8))
+(define-sort AddrSort () (_ BitVec 32))
+(define-sort ValSort () (_ BitVec 8))
 (define-sort MemSort () (Array AddrSort ValSort))
 
 ; Write the value y to index x
-(define-fun WriteArr 
-	; Args
-	((x AddrSort) (y ValSort) (arrIn MemSort)) 
-	
-	; Return value
-	MemSort
-	
-	; Function Body
-	(store arrIn x y)
+(define-fun WriteArr
+    ; Args
+    ((x AddrSort) (y ValSort) (arrIn MemSort))
+
+    ; Return value
+    MemSort
+
+    ; Function Body
+    (store arrIn x y)
 )
 
 ; Read from index x
-(define-fun ReadArr 
-	; Args
-	((x AddrSort) (arrIn MemSort)) 
-	
-	; Return value
-	ValSort
-	
-	; Function Body
-	(select arrIn x)
+(define-fun ReadArr
+    ; Args
+    ((x AddrSort) (arrIn MemSort))
+
+    ; Return value
+    ValSort
+
+    ; Function Body
+    (select arrIn x)
 )
 
 (define-fun letf ((m MemSort) (v1 AddrSort) (v2 AddrSort)) ValSort
-  (bvadd 
-    (ReadArr v1 m) 
+  (bvadd
+    (ReadArr v1 m)
     (ReadArr v2 m)))
 
-(synth-fun f 
-	; Args
-	((x0 ValSort) (x1 ValSort) (idx0 AddrSort) (idx1 AddrSort) (mem MemSort))
-	
-	; Return value
-	ValSort
-    
-    	; Grammar
-    	(
-	(StartArray MemSort (
-		(WriteArr (Variable AddrSort) (Variable ValSort) StartArray)
-		(WriteArr (Variable AddrSort) (Variable ValSort) mem)))
-
-	(Start ValSort (
-		(letf StartArray (Variable AddrSort) (Variable AddrSort))))
+(synth-fun f
+    ; Args
+    ((x0 ValSort) (x1 ValSort) (idx0 AddrSort) (idx1 AddrSort) (mem MemSort))
+
+    ; Return value
+    ValSort
+
+    ; Grammar
+    ((Start ValSort) (StartArray MemSort) (ASVar AddrSort) (VSVar ValSort))
+    (
+    (Start ValSort (
+        (letf StartArray ASVar ASVar)))
+
+    (StartArray MemSort (
+        (WriteArr ASVar VSVar StartArray)
+        (WriteArr ASVar VSVar mem)))
+
+    ; "Hack" to avoid parse errors in V2 format.
+    (ASVar AddrSort ((Variable AddrSort)))
+    (VSVar ValSort ((Variable ValSort)))
 ))
 
-(declare-var a (BitVec 8))
-(declare-var b (BitVec 8))
-(declare-var c (BitVec 32))
-(declare-var d (BitVec 32))
-(declare-var e (Array (BitVec 32) (BitVec 8)))
+(declare-var a (_ BitVec 8))
+(declare-var b (_ BitVec 8))
+(declare-var c (_ BitVec 32))
+(declare-var d (_ BitVec 32))
+(declare-var e (Array (_ BitVec 32) (_ BitVec 8)))
 (constraint (=> (not (= c d)) (= (bvadd a b) (f a b c d e))))
 (check-synth)
diff --git a/test/regress/regress1/sygus/array_search_2.sy b/test/regress/regress1/sygus/array_search_2.sy
index 93cbf9ce9..1a7c5888c 100644
--- a/test/regress/regress1/sygus/array_search_2.sy
+++ b/test/regress/regress1/sygus/array_search_2.sy
@@ -1,8 +1,8 @@
 ; REQUIRES: proof
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status --cegqi-si-sol-min-core --proof
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --cegqi-si-sol-min-core --proof
 (set-logic LIA)
-(synth-fun findIdx ( (y1 Int) (y2 Int) (k1 Int)) Int ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
+(synth-fun findIdx ((y1 Int) (y2 Int) (k1 Int)) Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 k1 (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)
 (declare-var x2 Int)
 (declare-var k Int)
diff --git a/test/regress/regress1/sygus/array_search_5-Q-easy.sy b/test/regress/regress1/sygus/array_search_5-Q-easy.sy
index 8be52a577..dd1783d85 100644
--- a/test/regress/regress1/sygus/array_search_5-Q-easy.sy
+++ b/test/regress/regress1/sygus/array_search_5-Q-easy.sy
@@ -1,8 +1,12 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status --decision=justification
-( set-logic LIA )
-( synth-fun findIdx  (         ( y1  Int )  ( y2  Int )  ( y3  Int )  ( y4  Int )  ( y5  Int )  ( k1  Int ) )  Int (
-  (Start  Int (    NT1
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification
+(set-logic LIA)
+
+(synth-fun findIdx  ((y1 Int) (y2 Int) (y3 Int) (y4 Int) (y5 Int) (k1 Int)) Int
+  ((Start Int) (NT1 Int) (NT2 Bool) (NT3 Int) (NT4 Int) (NT5 Bool) (NT6 Bool) (NT7 Int) (NT8 Int) (NT9 Int) (NT10 Int)
+   (NT11 Int) (NT12 Bool) (NT13 Int) (NT14 Int) (NT15 Bool) (NT16 Bool) (NT17 Bool) (NT18 Bool) (NT19 Bool)) (
+  (Start Int (
+    NT1
     NT3
     NT4
     NT7
@@ -13,7 +17,8 @@
     NT13
     NT14
 ))
-  (NT1  Int (    y5
+  (NT1 Int (
+    y5
     k1
     1
     y2
@@ -26,22 +31,27 @@
     y3
     3
 ))
-  (NT2  Bool (    (< NT1 NT1)
+  (NT2 Bool (
+    (< NT1 NT1)
     (> NT1 NT1)
     (>= NT1 NT1)
     (<= NT1 NT1)
 ))
-  (NT3  Int (    (ite NT2 NT1 NT1)
+  (NT3 Int (
+    (ite NT2 NT1 NT1)
 ))
-  (NT4  Int (    (ite NT5 NT1 NT1)
+  (NT4  Int (
+    (ite NT5 NT1 NT1)
     (ite NT2 NT3 NT1)
 ))
-  (NT5  Bool (    (< NT3 NT1)
+  (NT5 Bool (
+    (< NT3 NT1)
     (<= NT3 NT1)
     (>= NT3 NT1)
     (> NT3 NT1)
 ))
-  (NT6  Bool (    (<= NT4 NT1)
+  (NT6 Bool (
+    (<= NT4 NT1)
     (> NT4 NT1)
     (<= NT3 NT3)
     (> NT3 NT3)
@@ -50,33 +60,39 @@
     (< NT3 NT3)
     (>= NT3 NT3)
 ))
-  (NT7  Int (    (ite NT6 NT1 NT1)
+  (NT7 Int (
+    (ite NT6 NT1 NT1)
     (ite NT2 NT4 NT1)
 ))
-  (NT8  Int (    (ite NT2 NT7 NT1)
+  (NT8 Int (
+    (ite NT2 NT7 NT1)
     (ite NT5 NT4 NT1)
     (ite NT15 NT1 NT1)
     (ite NT5 NT1 NT4)
 ))
-  (NT9  Int (    (ite NT2 NT8 NT1)
+  (NT9 Int (
+    (ite NT2 NT8 NT1)
     (ite NT12 NT1 NT1)
     (ite NT6 NT1 NT4)
     (ite NT6 NT4 NT1)
     (ite NT5 NT7 NT1)
 ))
-  (NT10  Int (    (ite NT5 NT8 NT1)
+  (NT10 Int (
+    (ite NT5 NT8 NT1)
     (ite NT16 NT1 NT1)
     (ite NT2 NT9 NT1)
     (ite NT6 NT7 NT1)
     (ite NT5 NT4 NT4)
 ))
-  (NT11  Int (    (ite NT6 NT8 NT1)
+  (NT11 Int (
+    (ite NT6 NT8 NT1)
     (ite NT2 NT10 NT1)
     (ite NT5 NT9 NT1)
     (ite NT17 NT1 NT1)
     (ite NT6 NT4 NT4)
 ))
-  (NT12  Bool (    (< NT4 NT4)
+  (NT12 Bool (
+    (< NT4 NT4)
     (> NT4 NT4)
     (<= NT8 NT1)
     (< NT8 NT1)
@@ -85,31 +101,36 @@
     (>= NT8 NT1)
     (>= NT4 NT4)
 ))
-  (NT13  Int (    (ite NT18 NT1 NT1)
+  (NT13 Int (
+    (ite NT18 NT1 NT1)
     (ite NT12 NT7 NT1)
     (ite NT5 NT10 NT1)
     (ite NT6 NT9 NT1)
     (ite NT12 NT1 NT7)
     (ite NT2 NT11 NT1)
 ))
-  (NT14  Int (    (ite NT12 NT1 NT8)
+  (NT14 Int (
+    (ite NT12 NT1 NT8)
     (ite NT6 NT10 NT1)
     (ite NT5 NT11 NT1)
     (ite NT19 NT1 NT1)
     (ite NT12 NT8 NT1)
     (ite NT2 NT13 NT1)
 ))
-  (NT15  Bool (    (>= NT7 NT1)
+  (NT15 Bool (
+    (>= NT7 NT1)
     (< NT7 NT1)
     (> NT7 NT1)
     (<= NT7 NT1)
 ))
-  (NT16  Bool (    (< NT9 NT1)
+  (NT16 Bool (
+    (< NT9 NT1)
     (>= NT9 NT1)
     (> NT9 NT1)
     (<= NT9 NT1)
 ))
-  (NT17  Bool (    (< NT7 NT7)
+  (NT17 Bool (
+    (< NT7 NT7)
     (<= NT10 NT1)
     (>= NT10 NT1)
     (> NT10 NT1)
@@ -118,12 +139,14 @@
     (>= NT7 NT7)
     (<= NT7 NT7)
 ))
-  (NT18  Bool (    (< NT11 NT1)
+  (NT18 Bool (
+    (< NT11 NT1)
     (> NT11 NT1)
     (>= NT11 NT1)
     (<= NT11 NT1)
 ))
-  (NT19  Bool (    (>= NT13 NT1)
+  (NT19 Bool (
+    (>= NT13 NT1)
     (>= NT8 NT8)
     (< NT13 NT1)
     (> NT13 NT1)
@@ -133,12 +156,13 @@
     (<= NT13 NT1)
 ))
 ))
-  ( declare-var x1  Int )
-  ( declare-var x2  Int )
-  ( declare-var x3  Int )
-  ( declare-var x4  Int )
-  ( declare-var x5  Int )
-  ( declare-var k  Int )
-  ( constraint  ( =>     ( and     ( <     x1  x2 )  ( and     ( <     x2  x3 )  ( and     ( <     x3  x4 )  ( <     x4  x5 ) ) ) )  ( =>     ( <     k  x1 )  ( =     ( findIdx         x1  x2  x3  x4  x5  k )   0 ) ) ) )
-  ( check-synth )
 
+(declare-var x1 Int)
+(declare-var x2 Int)
+(declare-var x3 Int)
+(declare-var x4 Int)
+(declare-var x5 Int)
+(declare-var k Int)
+
+(constraint (=> (and (< x1 x2) (and (< x2 x3) (and (< x3 x4) (< x4 x5)))) (=> (< k x1) (= (findIdx x1 x2 x3 x4 x5 k) 0))))
+(check-synth)
diff --git a/test/regress/regress1/sygus/array_sum_2_5.sy b/test/regress/regress1/sygus/array_sum_2_5.sy
index 84a75d086..84046f30a 100644
--- a/test/regress/regress1/sygus/array_sum_2_5.sy
+++ b/test/regress/regress1/sygus/array_sum_2_5.sy
@@ -1,7 +1,7 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
 (set-logic LIA)
-(synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int ( 0 1 2 y1 y2 (+ Start Start)    (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
+(synth-fun findSum ( (y1 Int) (y2 Int) )Int ((Start Int) (BoolExpr Bool)) ((Start Int ( 0 1 2 y1 y2 (+ Start Start)    (ite BoolExpr Start Start))) (BoolExpr Bool ((< Start Start) (<= Start Start) (> Start Start) (>= Start Start)))))
 (declare-var x1 Int)
 (declare-var x2 Int)
 (constraint (=> (> (+ x1 x2) 5) (= (findSum x1 x2 ) (+ x1 x2))))
diff --git a/test/regress/regress1/sygus/bvudiv-by-2.sy b/test/regress/regress1/sygus/bvudiv-by-2.sy
index d6491972a..2bd8fc0dc 100644
--- a/test/regress/regress1/sygus/bvudiv-by-2.sy
+++ b/test/regress/regress1/sygus/bvudiv-by-2.sy
@@ -1,9 +1,10 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic BV)
 
-(synth-fun f ((x (BitVec 32))) (BitVec 32) 
-((Start (BitVec 32)
+(synth-fun f ((x (_ BitVec 32))) (_ BitVec 32)
+((Start (_ BitVec 32)) (StartBool Bool))
+((Start (_ BitVec 32)
    (
              (bvudiv Start Start)
              (bvurem Start Start)
@@ -16,7 +17,7 @@
     			(bvugt Start Start)
     			(= Start Start)
              ))))
-(declare-var x (BitVec 32) )
+(declare-var x (_ BitVec 32) )
 
 ; property
 (constraint (= (f #x00000008) #x00000004))
diff --git a/test/regress/regress1/sygus/car_3.lus.sy b/test/regress/regress1/sygus/car_3.lus.sy
index 9432d3131..3b58a997c 100755
--- a/test/regress/regress1/sygus/car_3.lus.sy
+++ b/test/regress/regress1/sygus/car_3.lus.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=cond-enum-igain --decision=justification
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-unif-pi=cond-enum-igain --decision=justification
 
 (set-logic LIA)
 
diff --git a/test/regress/regress1/sygus/cegar1.sy b/test/regress/regress1/sygus/cegar1.sy
index ee85db88a..d3b2030de 100644
--- a/test/regress/regress1/sygus/cegar1.sy
+++ b/test/regress/regress1/sygus/cegar1.sy
@@ -1,15 +1,12 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-inv-templ=post --sygus-out=status
 (set-logic LIA)
 
 (synth-inv inv-f ((x Int) (y Int)))
 
-(declare-primed-var x Int)
-(declare-primed-var y Int)
-
 (define-fun pre-f ((x Int) (y Int)) Bool
 (and (and (>= x 0)
-(and (<= x 2)  
+(and (<= x 2)
 (<= y 2))) (>= y 0)))
 
 (define-fun trans-f ((x Int) (y Int) (x! Int) (y! Int)) Bool
diff --git a/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy
index df0214316..c3b09011c 100644
--- a/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy
+++ b/test/regress/regress1/sygus/cegis-unif-inv-eq-fair.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-unif-pi=complete --sygus-bool-ite-return-const --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-bool-ite-return-const --sygus-out=status
 (set-logic LIA)
 
 (define-fun
@@ -187,9 +187,9 @@
   ) Bool
   
   (let
-   ((X1 Bool top.res.abs_10@0))
+   ((X1 top.res.abs_10@0))
    (let
-    ((X2 Int top.res.abs_4@0))
+    ((X2 top.res.abs_4@0))
     (and
      (= top.usr.OK@0 (=> X1 (< X2 4)))
      (__node_init_voiture_0
@@ -258,9 +258,9 @@
   ) Bool
   
   (let
-   ((X1 Bool top.res.abs_10@1))
+   ((X1 top.res.abs_10@1))
    (let
-    ((X2 Int top.res.abs_4@1))
+    ((X2 top.res.abs_4@1))
     (and
      (= top.usr.OK@1 (=> X1 (< X2 4)))
      (__node_trans_voiture_0
@@ -334,25 +334,6 @@
 ))
 
 
-(declare-primed-var top.usr.m Bool)
-(declare-primed-var top.usr.s Bool)
-(declare-primed-var top.usr.OK Bool)
-(declare-primed-var top.res.init_flag Bool)
-(declare-primed-var top.res.abs_0 Bool)
-(declare-primed-var top.res.abs_1 Bool)
-(declare-primed-var top.res.abs_2 Bool)
-(declare-primed-var top.res.abs_3 Int)
-(declare-primed-var top.res.abs_4 Int)
-(declare-primed-var top.res.abs_5 Int)
-(declare-primed-var top.res.abs_6 Bool)
-(declare-primed-var top.res.abs_7 Bool)
-(declare-primed-var top.res.abs_8 Bool)
-(declare-primed-var top.res.abs_9 Bool)
-(declare-primed-var top.res.abs_10 Bool)
-(declare-primed-var top.res.inst_3 Bool)
-(declare-primed-var top.res.inst_2 Bool)
-(declare-primed-var top.res.inst_1 Bool)
-(declare-primed-var top.res.inst_0 Bool)
 
 (define-fun
   init (
@@ -378,9 +359,9 @@
   ) Bool
   
   (let
-   ((X1 Bool top.res.abs_10))
+   ((X1 top.res.abs_10))
    (let
-    ((X2 Int top.res.abs_4))
+    ((X2 top.res.abs_4))
     (and
      (= top.usr.OK (=> X1 (< X2 4)))
      (__node_init_voiture_0
@@ -454,9 +435,9 @@
   ) Bool
   
   (let
-   ((X1 Bool top.res.abs_10!))
+   ((X1 top.res.abs_10!))
    (let
-    ((X2 Int top.res.abs_4!))
+    ((X2 top.res.abs_4!))
     (and
      (= top.usr.OK! (=> X1 (< X2 4)))
      (__node_trans_voiture_0
diff --git a/test/regress/regress1/sygus/cegisunif-depth1.sy b/test/regress/regress1/sygus/cegisunif-depth1.sy
index 9f6f65907..06c4d3a78 100644
--- a/test/regress/regress1/sygus/cegisunif-depth1.sy
+++ b/test/regress/regress1/sygus/cegisunif-depth1.sy
@@ -1,8 +1,9 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-out=status
 (set-logic LIA)
 
 (synth-fun f ((x Int) (y Int)) Int
+  ((Start Int) (CBool Bool))
   (
     (Start Int
       (0 1 x y
diff --git a/test/regress/regress1/sygus/cggmp.sy b/test/regress/regress1/sygus/cggmp.sy
index a3247e4f4..551528633 100644
--- a/test/regress/regress1/sygus/cggmp.sy
+++ b/test/regress/regress1/sygus/cggmp.sy
@@ -1,15 +1,12 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inv-templ=pre --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-inv-templ=pre --sygus-out=status
 
 (set-logic LIA)
 
 (synth-inv inv-f ((i Int) (j Int)))
 
-(declare-primed-var i Int)
-(declare-primed-var j Int)
-
 (define-fun pre-f ((i Int) (j Int)) Bool
-(and (= i 1)  
+(and (= i 1)
 (= j 10)))
 
 (define-fun trans-f ((i Int) (j Int) (i! Int) (j! Int)) Bool
diff --git a/test/regress/regress1/sygus/clock-inc-tuple.sy b/test/regress/regress1/sygus/clock-inc-tuple.sy
index 65b17605d..c9705f7b8 100644
--- a/test/regress/regress1/sygus/clock-inc-tuple.sy
+++ b/test/regress/regress1/sygus/clock-inc-tuple.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status --decision=justification
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --decision=justification
 
 (set-logic ALL_SUPPORTED)
 (declare-var m Int)
@@ -8,7 +8,7 @@
 (declare-datatypes ((tuple2 0)) ( ((tuple2 (_m Int) (_s Int))) ))
 
 (synth-fun x12 ((m Int) (s Int) (inc Int)) tuple2)
-(constraint (=> 
-(and (>= m 0) (>= s 0) (< s 3) (> inc 0)) 
+(constraint (=>
+(and (>= m 0) (>= s 0) (< s 3) (> inc 0))
 (and (>= (_m (x12 m s inc)) 0) (>= (_s (x12 m s inc)) 0) (< (_s (x12 m s inc)) 3) (= (+ (* (_m (x12 m s inc)) 3) (_s (x12 m s inc))) (+ (+ (* m 3) s) inc)))))
 (check-synth)
diff --git a/test/regress/regress1/sygus/commutative-stream.sy b/test/regress/regress1/sygus/commutative-stream.sy
index 8203fd9cf..5febabc42 100644
--- a/test/regress/regress1/sygus/commutative-stream.sy
+++ b/test/regress/regress1/sygus/commutative-stream.sy
@@ -3,11 +3,12 @@
 ; EXPECT: (error "Maximum term size (2) for enumerative SyGuS exceeded.")
 ; EXIT: 1
 
-; COMMAND-LINE: --sygus-stream --sygus-abort-size=2 --sygus-active-gen=none --decision=justification
+; COMMAND-LINE: --lang=sygus2 --sygus-stream --sygus-abort-size=2 --sygus-active-gen=none --decision=justification
 
 (set-logic LIA)
 
 (synth-fun comm ((x Int) (y Int)) Int
+    ((Start Int))
     ((Start Int (x
                  y
                  (+ Start Start)
diff --git a/test/regress/regress1/sygus/commutative.sy b/test/regress/regress1/sygus/commutative.sy
index 24201b453..7fe07c3fa 100644
--- a/test/regress/regress1/sygus/commutative.sy
+++ b/test/regress/regress1/sygus/commutative.sy
@@ -1,9 +1,10 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic LIA)
 
 (synth-fun comm ((x Int) (y Int)) Int
+    ((Start Int))
     ((Start Int (x
                  y
                  (+ Start Start)
diff --git a/test/regress/regress1/sygus/constant-bool-si-all.sy b/test/regress/regress1/sygus/constant-bool-si-all.sy
index 45d49e75b..18a60f176 100644
--- a/test/regress/regress1/sygus/constant-bool-si-all.sy
+++ b/test/regress/regress1/sygus/constant-bool-si-all.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
 (synth-fun f () Bool)
 (synth-fun g () Bool)
diff --git a/test/regress/regress1/sygus/constant-dec-tree-bug.sy b/test/regress/regress1/sygus/constant-dec-tree-bug.sy
index e20520a4a..ddbf07d61 100644
--- a/test/regress/regress1/sygus/constant-dec-tree-bug.sy
+++ b/test/regress/regress1/sygus/constant-dec-tree-bug.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-unif-pi=complete
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-unif-pi=complete
 
 (set-logic LIA)
 (synth-fun u ((x Int)) Int)
diff --git a/test/regress/regress1/sygus/constant-ite-bv.sy b/test/regress/regress1/sygus/constant-ite-bv.sy
index 330ef026e..356c71d1d 100644
--- a/test/regress/regress1/sygus/constant-ite-bv.sy
+++ b/test/regress/regress1/sygus/constant-ite-bv.sy
@@ -1,16 +1,17 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --sygus-repair-const
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --sygus-repair-const
 (set-logic BV)
-(synth-fun f ( (x (BitVec 64))) (BitVec 64)
+(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64)
+((Start (_ BitVec 64)) (StartBool Bool))
 (
-(Start (BitVec 64) (
+(Start (_ BitVec 64) (
         #x0000000000000000 
         #x0000000000000001 
         x 
         (bvnot Start)
 		    (bvadd Start Start)
 		    (ite StartBool Start Start)
-		    (Constant (BitVec 64))
+		    (Constant (_ BitVec 64))
  ))
 (StartBool Bool ((bvule Start Start)))
 )
diff --git a/test/regress/regress1/sygus/constant.sy b/test/regress/regress1/sygus/constant.sy
index 1bb3e59fa..1416d566d 100644
--- a/test/regress/regress1/sygus/constant.sy
+++ b/test/regress/regress1/sygus/constant.sy
@@ -1,9 +1,10 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic LIA)
 
 (synth-fun constant ((x Int)) Int
+    ((Start Int))
     ((Start Int (x
                  0
                  1
diff --git a/test/regress/regress1/sygus/crci-ssb-unk.sy b/test/regress/regress1/sygus/crci-ssb-unk.sy
index f2b28db9c..d59fd297d 100644
--- a/test/regress/regress1/sygus/crci-ssb-unk.sy
+++ b/test/regress/regress1/sygus/crci-ssb-unk.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic BV)
 
@@ -10,6 +10,7 @@
 
 
 (synth-fun skel ( (LN4 Bool) (LN91 Bool)  )  Bool    
+          ((Start Bool) (depth1 Bool) (depth2 Bool) (depth3 Bool) (depth4 Bool))
           ((Start Bool (
                                   (and depth1 depth1)
                                   (xor depth1 depth1)
diff --git a/test/regress/regress1/sygus/crcy-si-rcons.sy b/test/regress/regress1/sygus/crcy-si-rcons.sy
index 6e2f54c31..70aec7c4c 100644
--- a/test/regress/regress1/sygus/crcy-si-rcons.sy
+++ b/test/regress/regress1/sygus/crcy-si-rcons.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --cegqi-si-abort --decision=internal --cegqi-si-rcons=try --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --cegqi-si-abort --decision=internal --cegqi-si-rcons=try --sygus-out=status
 
 (set-logic BV)
 
@@ -10,6 +10,8 @@
 
 
 (synth-fun skel ( (LN24 Bool) (k3 Bool) (LN129 Bool) (LN141 Bool)  )  Bool    
+          ((Start Bool) (depth1 Bool) (depth2 Bool) (depth3 Bool) (depth4 Bool)
+           (depth5 Bool) (depth6 Bool) (depth7 Bool) (depth8 Bool))
           ((Start Bool (
 		                                  (and depth1 depth1)
 		                                  (not depth1)
diff --git a/test/regress/regress1/sygus/crcy-si.sy b/test/regress/regress1/sygus/crcy-si.sy
index 46500ee4d..1c0abc4fe 100644
--- a/test/regress/regress1/sygus/crcy-si.sy
+++ b/test/regress/regress1/sygus/crcy-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic BV)
 
@@ -8,6 +8,7 @@
 )
  
 (synth-fun Imp ((k1 Bool) (k2 Bool) (k3 Bool)) Bool
+ ((Start Bool) (d1 Bool) (d2 Bool))
  ((Start Bool ( (and d1 d1) (or d1 d1) (xor d1 d1) (not d1) ) )
  (d1 Bool ( (and d2 d2) (or d2 d2) (xor d2 d2) (not d2) ) )
  (d2 Bool ( k1 k2 k3) ) )
diff --git a/test/regress/regress1/sygus/cube-nia.sy b/test/regress/regress1/sygus/cube-nia.sy
index da7d98e66..ef57840fe 100644
--- a/test/regress/regress1/sygus/cube-nia.sy
+++ b/test/regress/regress1/sygus/cube-nia.sy
@@ -1,24 +1,23 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic NIA)
 
 (synth-fun cube ((x Int)) Int
+  ((ntInt Int) (ntBool Bool))
   (
-    (Start Int (ntInt))
-  
-    (ntBool Bool
-      ( 
-        (> ntInt ntInt)
-        (= ntInt ntInt)
-      )
-    )
     (ntInt Int
       (1 x
         (* ntInt ntInt)
         (ite ntBool ntInt ntInt)
       )
     )
+    (ntBool Bool
+      ( 
+        (> ntInt ntInt)
+        (= ntInt ntInt)
+      )
+    )
   )
 )
 
diff --git a/test/regress/regress1/sygus/double.sy b/test/regress/regress1/sygus/double.sy
index f3fea3122..0ba822278 100644
--- a/test/regress/regress1/sygus/double.sy
+++ b/test/regress/regress1/sygus/double.sy
@@ -1,12 +1,12 @@
 ; EXPECT: unsat

-; COMMAND-LINE: --sygus-out=status

+; COMMAND-LINE: --lang=sygus2 --sygus-out=status

 

 (set-logic SLIA)

 (declare-datatype Ex ((Ex2 (ex Int))))

 

 (synth-fun double ((x1 Ex)) Int

+	((ntInt Int) (ntEx Ex))

 	(

-		(Start Int (ntInt))

 		(ntInt Int

 			(

 				(ex ntEx)

diff --git a/test/regress/regress1/sygus/dt-test-ns.sy b/test/regress/regress1/sygus/dt-test-ns.sy
index a6e8ac5c2..3d078cc25 100644
--- a/test/regress/regress1/sygus/dt-test-ns.sy
+++ b/test/regress/regress1/sygus/dt-test-ns.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
@@ -11,4 +11,3 @@
 (constraint (is-cons (f x)))
 (constraint (and (= (head (f x)) x) (= (head (f x)) (+ 5 (head (tail (f x)))))))
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/dup-op.sy b/test/regress/regress1/sygus/dup-op.sy
index e2c69282e..517849b2a 100644
--- a/test/regress/regress1/sygus/dup-op.sy
+++ b/test/regress/regress1/sygus/dup-op.sy
@@ -1,11 +1,11 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
+    ((Start Int) (Con Int))
     ((Start Int ((+ Con Con) (+ Start Start) x))
      (Con Int (0 1))))
 
 (declare-var x Int)
 (constraint (= (f x) (* 2 x)))
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/enum-test.sy b/test/regress/regress1/sygus/enum-test.sy
index 7364747fc..55b2eb69e 100644
--- a/test/regress/regress1/sygus/enum-test.sy
+++ b/test/regress/regress1/sygus/enum-test.sy
@@ -1,9 +1,9 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 ;; this is the custom enumeration datatype syntax from an early proposal of the sygus standard
 (define-sort D (Enum (a b)))
 (define-fun f ((x D)) Int (ite (= x D::a) 3 7))
-(synth-fun g () D ((Start D (D::a D::b))))
+(synth-fun g () D ((Start D)) ((Start D (D::a D::b))))
 (constraint (= (f g) 7))
 (check-synth)
diff --git a/test/regress/regress1/sygus/error1-dt.sy b/test/regress/regress1/sygus/error1-dt.sy
index 67f73aded..1ae8cabd9 100644
--- a/test/regress/regress1/sygus/error1-dt.sy
+++ b/test/regress/regress1/sygus/error1-dt.sy
@@ -1,21 +1,21 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --cegqi-si=none --sygus-active-gen=enum
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none --sygus-active-gen=enum
 
 (set-logic ALL_SUPPORTED)
 
-(declare-datatypes ((IntRange 0)) 
+(declare-datatypes ((IntRange 0))
    (((IntRange (lower Int) (upper Int)))))
 
-(declare-datatypes ((Loc 0)) 
+(declare-datatypes ((Loc 0))
    (((Loc (x Int) (y Int)))))
 
-(declare-datatypes ((LocRange 0)) 
+(declare-datatypes ((LocRange 0))
    (((LocRange (xD IntRange) (yD IntRange)))))
 
-(declare-datatypes ((Ship 0)) 
+(declare-datatypes ((Ship 0))
    (((Ship (shipCapacity Int) (shipLoc Loc)))))
 
-(declare-datatypes ((ShipRange 0)) 
+(declare-datatypes ((ShipRange 0))
    (((ShipRange (shipCapacityD IntRange) (shipLocD LocRange)))))
 
 (define-fun betweenInt ((x Int) (r IntRange)) Bool
@@ -61,10 +61,10 @@
 (declare-var prior ShipRange)
 (declare-var response Bool)
 
-(constraint 
-  (=> (betweenShip secret (f secret prior response)) 
-          (= response 
-             (and (atLeast secret) 
+(constraint
+  (=> (betweenShip secret (f secret prior response))
+          (= response
+             (and (atLeast secret)
                   (subsetShip (f secret prior response) prior))))
 )
 
diff --git a/test/regress/regress1/sygus/extract.sy b/test/regress/regress1/sygus/extract.sy
index d1541fa87..f3cfa09a2 100644
--- a/test/regress/regress1/sygus/extract.sy
+++ b/test/regress/regress1/sygus/extract.sy
@@ -1,18 +1,19 @@
 ; EXPECT: unsat

-; COMMAND-LINE: --sygus-out=status

+; COMMAND-LINE: --lang=sygus2 --sygus-out=status

 

 (set-logic ALL_SUPPORTED)

 (declare-datatype Ex ((Ex2 (ex Int))))

 

 (synth-fun ident ((x1 Ex)) Int

+	((Start Int) (ntInt Int) (ntEx Ex))

 	(

 		(Start Int (ntInt))

 		(ntInt Int

 			(

 				(ex ntEx)

- 			)

+			)

 		)

-		(ntEx Ex ( x1 ) )

+		(ntEx Ex ( x1 ))

 	)

 )

 (constraint (= (ident (Ex2 1)) 1))

diff --git a/test/regress/regress1/sygus/fg_polynomial3.sy b/test/regress/regress1/sygus/fg_polynomial3.sy
index d70516bf1..2da3809a8 100644
--- a/test/regress/regress1/sygus/fg_polynomial3.sy
+++ b/test/regress/regress1/sygus/fg_polynomial3.sy
@@ -1,13 +1,11 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic LIA)
 
-(synth-fun addExpr1 ((x Int) (y Int)) Int
-)
+(synth-fun addExpr1 ((x Int) (y Int)) Int)
 
-(synth-fun addExpr2 ((x Int) (y Int)) Int
-)
+(synth-fun addExpr2 ((x Int) (y Int)) Int)
 
 (declare-var x Int)
 (declare-var y Int)
@@ -15,4 +13,3 @@
 (constraint (= (+ (addExpr1 x y) (addExpr2 y x)) (- x (+ x y))))
 
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy b/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy
index efec0e0e7..145064141 100644
--- a/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy
+++ b/test/regress/regress1/sygus/find_sc_bvult_bvnot.sy
@@ -1,11 +1,12 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
-; COMMAND-LINE: --sygus-out=status --cegis-sample=trust --no-check-synth-sol
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegis-sample=trust --no-check-synth-sol
 (set-logic BV)
 
 ; we test --cegis-sample=trust since we can exhaustively sample BV4
 
-(synth-fun SC ((s (BitVec 4)) (t (BitVec 4))) Bool
+(synth-fun SC ((s (_ BitVec 4)) (t (_ BitVec 4))) Bool
+  ((Start Bool) (StartBv (_ BitVec 4)))
   ((Start Bool (
      true
      false
@@ -19,7 +20,7 @@
      (bvuge StartBv StartBv)
      (bvsge StartBv StartBv)
    ))
-   (StartBv (BitVec 4) (
+   (StartBv (_ BitVec 4) (
      s
      t
      #x0
@@ -36,15 +37,15 @@
    ))
 ))
 
-(declare-var s (BitVec 4))
-(declare-var t (BitVec 4))
+(declare-var s (_ BitVec 4))
+(declare-var t (_ BitVec 4))
 (define-fun udivtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4)
   (ite (= b #x0) #xF (bvudiv a b))
 )
 (define-fun uremtotal ((a (_ BitVec 4)) (b (_ BitVec 4))) (_ BitVec 4)
   (ite (= b #x0) a (bvurem a b))
 )
-(define-fun case ((x (BitVec 4)) (s (BitVec 4)) (t (BitVec 4))) Bool
+(define-fun case ((x (_ BitVec 4)) (s (_ BitVec 4)) (t (_ BitVec 4))) Bool
 (bvult (bvnot x) t)
 )
 (constraint
diff --git a/test/regress/regress1/sygus/hd-01-d1-prog.sy b/test/regress/regress1/sygus/hd-01-d1-prog.sy
index bbdbda1bd..9a28d6d79 100644
--- a/test/regress/regress1/sygus/hd-01-d1-prog.sy
+++ b/test/regress/regress1/sygus/hd-01-d1-prog.sy
@@ -1,22 +1,23 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic BV)
 
-(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x (bvsub x #x00000001)))
+(define-fun hd01 ((x (_ BitVec 32))) (_ BitVec 32) (bvand x (bvsub x #x00000001)))
 
-(synth-fun f ((x (BitVec 32))) (BitVec 32)
-    ((Start (BitVec 32) ((bvand Start Start)
-                         (bvsub Start Start)
-             (bvor Start Start)
-             (bvadd Start Start)
-             (bvxor Start Start)
-                         x
-             #x00000000
-             #xFFFFFFFF
-                         #x00000001))))
+(synth-fun f ((x (_ BitVec 32))) (_ BitVec 32)
+    ((Start (_ BitVec 32)))
+    ((Start (_ BitVec 32) (
+        (bvand Start Start)
+        (bvsub Start Start)
+        (bvor Start Start)
+        (bvadd Start Start)
+        (bvxor Start Start)
+        x
+        #x00000000
+        #xFFFFFFFF
+        #x00000001))))
 
-(declare-var x (BitVec 32))
+(declare-var x (_ BitVec 32))
 (constraint (= (hd01 x) (f x)))
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/hd-sdiv.sy b/test/regress/regress1/sygus/hd-sdiv.sy
index 37e1daf88..c4c90c6f6 100644
--- a/test/regress/regress1/sygus/hd-sdiv.sy
+++ b/test/regress/regress1/sygus/hd-sdiv.sy
@@ -1,16 +1,16 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
 (set-logic BV)
 
-(define-fun hd01 ((x (BitVec 32))) (BitVec 32) (bvand x #x00000001))
+(define-fun hd01 ((x (_ BitVec 32))) (_ BitVec 32) (bvand x #x00000001))
 
-(synth-fun f ((x (BitVec 32))) (BitVec 32)
-    ((Start (BitVec 32) ((bvsdiv Start Start)
-						             (bvand Start Start)
+(synth-fun f ((x (_ BitVec 32))) (_ BitVec 32)
+    ((Start (_ BitVec 32)))
+    ((Start (_ BitVec 32) ((bvsdiv Start Start)
+                         (bvand Start Start)
                          x
                          #x00000001))))
 
-(declare-var y (BitVec 32))
+(declare-var y (_ BitVec 32))
 (constraint (= (hd01 y) (f y)))
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/ho-sygus.sy b/test/regress/regress1/sygus/ho-sygus.sy
index c66485817..893c2034e 100644
--- a/test/regress/regress1/sygus/ho-sygus.sy
+++ b/test/regress/regress1/sygus/ho-sygus.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --uf-ho
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --uf-ho
 (set-logic ALL)
 (synth-fun f ((y (-> Int Int)) (z Int)) Int)
 (declare-var z (-> Int Int))
diff --git a/test/regress/regress1/sygus/icfp_14.12-flip-args.sy b/test/regress/regress1/sygus/icfp_14.12-flip-args.sy
index a1e93cc44..96851045c 100644
--- a/test/regress/regress1/sygus/icfp_14.12-flip-args.sy
+++ b/test/regress/regress1/sygus/icfp_14.12-flip-args.sy
@@ -1,28 +1,26 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic BV)
 
-(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
-(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
-(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
-(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
-(define-fun if0 ((y (BitVec 64)) (x (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))
+(define-fun shr1 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000001))
+(define-fun shr4 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000004))
+(define-fun shr16 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000010))
+(define-fun shl1 ((x (_ BitVec 64))) (_ BitVec 64) (bvshl x #x0000000000000001))
+(define-fun if0 ((y (_ BitVec 64)) (x (_ BitVec 64)) (z (_ BitVec 64))) (_ BitVec 64) (ite (= x #x0000000000000001) y z))
 
-(synth-fun f ( (x (BitVec 64))) (BitVec 64)
-(
-
-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
-                    (shl1 Start)
- 		    (shr1 Start)
-		    (shr4 Start)
-		    (shr16 Start)
-		    (bvand Start Start)
-		    (bvor Start Start)
-		    (bvxor Start Start)
-		    (bvadd Start Start)
-		    (if0 Start Start Start)
- ))
-)
+(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64)
+((Start (_ BitVec 64)))
+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+            (shl1 Start)
+            (shr1 Start)
+            (shr4 Start)
+            (shr16 Start)
+            (bvand Start Start)
+            (bvor Start Start)
+            (bvxor Start Start)
+            (bvadd Start Start)
+            (if0 Start Start Start)
+)))
 )
 (constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57))
 (constraint (= (f #xFDA75AD598A27135) #x812C529533AEC765))
diff --git a/test/regress/regress1/sygus/icfp_14.12.sy b/test/regress/regress1/sygus/icfp_14.12.sy
index 51b86f0f5..6f76346d5 100644
--- a/test/regress/regress1/sygus/icfp_14.12.sy
+++ b/test/regress/regress1/sygus/icfp_14.12.sy
@@ -1,28 +1,26 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic BV)
 
-(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
-(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
-(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
-(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
-(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))
+(define-fun shr1 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000001))
+(define-fun shr4 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000004))
+(define-fun shr16 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000010))
+(define-fun shl1 ((x (_ BitVec 64))) (_ BitVec 64) (bvshl x #x0000000000000001))
+(define-fun if0 ((x (_ BitVec 64)) (y (_ BitVec 64)) (z (_ BitVec 64))) (_ BitVec 64) (ite (= x #x0000000000000001) y z))
 
-(synth-fun f ( (x (BitVec 64))) (BitVec 64)
-(
-
-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
-                    (shl1 Start)
- 		    (shr1 Start)
-		    (shr4 Start)
-		    (shr16 Start)
-		    (bvand Start Start)
-		    (bvor Start Start)
-		    (bvxor Start Start)
-		    (bvadd Start Start)
-		    (if0 Start Start Start)
- ))
-)
+(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64)
+((Start (_ BitVec 64)))
+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+            (shl1 Start)
+            (shr1 Start)
+            (shr4 Start)
+            (shr16 Start)
+            (bvand Start Start)
+            (bvor Start Start)
+            (bvxor Start Start)
+            (bvadd Start Start)
+            (if0 Start Start Start)
+)))
 )
 (constraint (= (f #x6E393354DFFAAB51) #xC8E366559002AA57))
 (constraint (= (f #xFDA75AD598A27135) #x812C529533AEC765))
diff --git a/test/regress/regress1/sygus/icfp_14_12_diff_types.sy b/test/regress/regress1/sygus/icfp_14_12_diff_types.sy
index f83277757..212943cab 100644
--- a/test/regress/regress1/sygus/icfp_14_12_diff_types.sy
+++ b/test/regress/regress1/sygus/icfp_14_12_diff_types.sy
@@ -1,23 +1,21 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic BV)
 
-(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))
+(define-fun if0 ((x (_ BitVec 64)) (y (_ BitVec 64)) (z (_ BitVec 64))) (_ BitVec 64) (ite (= x #x0000000000000001) y z))
 
-(synth-fun f ( (x (BitVec 64))) (BitVec 64)
-(
-
-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
-		    (bvand Start Start)
-		    (bvor Start Start)
-		    (bvxor Start Start)
-		    (bvadd Start Start)
-		    (if0 Start Start2 Start2)
-		    (ite StartBool Start Start2)
+(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64)
+((Start (_ BitVec 64)) (Start2 (_ BitVec 64)) (StartBool Bool))
+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+            (bvand Start Start)
+            (bvor Start Start)
+            (bvxor Start Start)
+            (bvadd Start Start)
+            (if0 Start Start2 Start2)
+            (ite StartBool Start Start2)
  ))
-(Start2 (BitVec 64) (#x0000000000000000 #x0000000000000002))
-(StartBool Bool ((= Start Start)))
-)
+ (Start2 (_ BitVec 64) (#x0000000000000000 #x0000000000000002))
+ (StartBool Bool ((= Start Start))))
 )
 (constraint (= (f #x0000000000000001) #x0000000000000001))
 (constraint (= (f #x1ED2E25068744C80) #x0000000000000000))
diff --git a/test/regress/regress1/sygus/icfp_28_10.sy b/test/regress/regress1/sygus/icfp_28_10.sy
index 212ae37f5..4ca73b87f 100644
--- a/test/regress/regress1/sygus/icfp_28_10.sy
+++ b/test/regress/regress1/sygus/icfp_28_10.sy
@@ -1,19 +1,18 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic BV)
 
-(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
-(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
-(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
-(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
-(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))
+(define-fun shr1 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000001))
+(define-fun shr4 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000004))
+(define-fun shr16 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000010))
+(define-fun shl1 ((x (_ BitVec 64))) (_ BitVec 64) (bvshl x #x0000000000000001))
+(define-fun if0 ((x (_ BitVec 64)) (y (_ BitVec 64)) (z (_ BitVec 64))) (_ BitVec 64) (ite (= x #x0000000000000001) y z))
 
-(synth-fun f ( (x (BitVec 64))) (BitVec 64)
-(
-
-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
-                    (shl1 Start)
+(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64)
+((Start (_ BitVec 64)))
+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+        (shl1 Start)
         (shr1 Start)
         (shr4 Start)
         (shr16 Start)
@@ -21,8 +20,7 @@
         (bvor Start Start)
         (bvxor Start Start)
         (bvadd Start Start)
-        (if0 Start Start Start)
- ))
+        (if0 Start Start Start)))
 )
 )
 
diff --git a/test/regress/regress1/sygus/icfp_easy-ite.sy b/test/regress/regress1/sygus/icfp_easy-ite.sy
index f0cbbdc53..63cc4736c 100644
--- a/test/regress/regress1/sygus/icfp_easy-ite.sy
+++ b/test/regress/regress1/sygus/icfp_easy-ite.sy
@@ -1,28 +1,27 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic BV)
 
-(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))
-(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))
-(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))
-(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))
-(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))
+(define-fun shr1 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000001))
+(define-fun shr4 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000004))
+(define-fun shr16 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000010))
+(define-fun shl1 ((x (_ BitVec 64))) (_ BitVec 64) (bvshl x #x0000000000000001))
+(define-fun if0 ((x (_ BitVec 64)) (y (_ BitVec 64)) (z (_ BitVec 64))) (_ BitVec 64) (ite (= x #x0000000000000001) y z))
 
-(synth-fun f ( (x (BitVec 64))) (BitVec 64)
-(
-
-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
-                    (shl1 Start)
- 		    (shr1 Start)
-		    (shr4 Start)
-		    (shr16 Start)
-		    (bvand Start Start)
-		    (bvor Start Start)
-		    (bvxor Start Start)
-		    (bvadd Start Start)
-		    (ite StartBool Start Start)
+(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64)
+((Start (_ BitVec 64)) (StartBool Bool))
+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)
+            (shl1 Start)
+            (shr1 Start)
+            (shr4 Start)
+            (shr16 Start)
+            (bvand Start Start)
+            (bvor Start Start)
+            (bvxor Start Start)
+            (bvadd Start Start)
+            (ite StartBool Start Start)
  ))
-(StartBool Bool ((= Start #x0000000000000001)))
+ (StartBool Bool ((= Start #x0000000000000001)))
 )
 )
 (constraint (= (f #x0000000000000001) #x0000000000000001))
diff --git a/test/regress/regress1/sygus/int-any-const.sy b/test/regress/regress1/sygus/int-any-const.sy
index b5de57533..18e7ed06e 100644
--- a/test/regress/regress1/sygus/int-any-const.sy
+++ b/test/regress/regress1/sygus/int-any-const.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise
 
 (set-logic LIA)
 (synth-fun f ((x Int) (y Int)) Int)
diff --git a/test/regress/regress1/sygus/inv-example.sy b/test/regress/regress1/sygus/inv-example.sy
index ff68bc06c..bcc6c0aa8 100644
--- a/test/regress/regress1/sygus/inv-example.sy
+++ b/test/regress/regress1/sygus/inv-example.sy
@@ -1,10 +1,7 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
 (synth-inv inv-f ((x Int) (y Int) (b Bool)))
-(declare-primed-var x Int)
-(declare-primed-var y Int)
-(declare-primed-var b Bool)
 (define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (and (>= x 5) (<= x 9)) (and (>= y 1) (<= y 3))))
 (define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (and (and (= b! b) (= y! x)) (ite b (= x! (+ x 10)) (= x! (+ x 12)))))
 (define-fun post-f ((x Int) (y Int) (b Bool)) Bool (<= y x))
diff --git a/test/regress/regress1/sygus/inv-missed-sol-true.sy b/test/regress/regress1/sygus/inv-missed-sol-true.sy
index b04022766..f8a3136f2 100644
--- a/test/regress/regress1/sygus/inv-missed-sol-true.sy
+++ b/test/regress/regress1/sygus/inv-missed-sol-true.sy
@@ -1,12 +1,9 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
 
 (synth-inv inv-f ((x Int) (z Int)))
 
-(declare-primed-var x Int)
-(declare-primed-var z Int)
-
 (define-fun pre-f ((x Int) (z Int)) Bool
   (and (> x (- 0 100)) (< x 200)
        (> z 100) (< z 200)))
@@ -22,4 +19,4 @@
 
 (inv-constraint inv-f pre-f trans-f post-f)
 
-(check-synth)
\ No newline at end of file
+(check-synth)
diff --git a/test/regress/regress1/sygus/inv-unused.sy b/test/regress/regress1/sygus/inv-unused.sy
index 91ba95d39..a5eb41b26 100644
--- a/test/regress/regress1/sygus/inv-unused.sy
+++ b/test/regress/regress1/sygus/inv-unused.sy
@@ -1,10 +1,7 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
 (synth-inv inv-f ((x Int) (y Int) (b Bool)))
-(declare-primed-var x Int)
-(declare-primed-var y Int)
-(declare-primed-var b Bool)
 (define-fun pre-f ((x Int) (y Int) (b Bool)) Bool (and (>= x 5) (<= x 9)))
 (define-fun trans-f ((x Int) (y Int) (b Bool) (x! Int) (y! Int) (b! Bool)) Bool (= x! (+ x 1)))
 (define-fun post-f ((x Int) (y Int) (b Bool)) Bool (> x 0))
diff --git a/test/regress/regress1/sygus/inv_gen_fig8.sy b/test/regress/regress1/sygus/inv_gen_fig8.sy
index 19c36e4dc..5c1aa4852 100644
--- a/test/regress/regress1/sygus/inv_gen_fig8.sy
+++ b/test/regress/regress1/sygus/inv_gen_fig8.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
 (synth-fun inv ((l Int)) Bool
     (
@@ -8,9 +8,9 @@
         (AtomicFormula Bool ((<= Sum Const) (= Sum Const)))
         (Sum Int ((+ Term Term)))
         (Term Int ((* Sign Var)))
-        (Sign Int (0 1 -1))
+        (Sign Int (0 1 (- 1)))
         (Var Int (l))
-        (Const Int (-3 -2 -1 0 1 2 3))
+        (Const Int ((- 3) (- 2) (- 1) 0 1 2 3))
     )
 )
 
@@ -36,11 +36,11 @@
 (declare-var x4p Int)
 
 (constraint (implies (and6 (= l 0) (or (= x0p (+ x0 1)) (= x0p (- x0 1))) 
-				  (or (= x1p (+ x1 1)) (= x1p (- x1 1)))
-				  (or (= x2p (+ x2 1)) (= x2p (- x2 1)))
-				  (or (= x3p (+ x3 1)) (= x3p (- x3 1)))
-				  (or (= x4p (+ x4 1)) (= x4p (- x4 1)))) 
-		     (inv l)))
+                  (or (= x1p (+ x1 1)) (= x1p (- x1 1)))
+                  (or (= x2p (+ x2 1)) (= x2p (- x2 1)))
+                  (or (= x3p (+ x3 1)) (= x3p (- x3 1)))
+                  (or (= x4p (+ x4 1)) (= x4p (- x4 1)))) 
+             (inv l)))
 (constraint (implies (and (inv l) (not (= l 0))) false))
 
 (check-synth)
diff --git a/test/regress/regress1/sygus/issue2914.sy b/test/regress/regress1/sygus/issue2914.sy
index 0f125a870..71a5a5987 100644
--- a/test/regress/regress1/sygus/issue2914.sy
+++ b/test/regress/regress1/sygus/issue2914.sy
@@ -1,18 +1,12 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
-(declare-datatype JSIdentifier ((JSString (jsString String)) (Error )))
 
-(synth-fun substring ((x1 String) (x3 Int))String
-	((Start String (ntString))
-		(ntInt Int
-			(0 x3)
-		)
-		(ntJSIdentifier JSIdentifier
-			( 
-				Error
-			)
-		)
+(declare-datatype JSIdentifier ((JSString (jsString String)) (Error)))
+
+(synth-fun substring ((x1 String) (x3 Int)) String
+	((ntString String) (ntInt Int) (ntJSIdentifier JSIdentifier))
+	(
 		(ntString String
 			(x1
 				(str.substr ntString ntInt ntInt)
@@ -20,7 +14,16 @@
 				(str.++ ntString ntString)
 			)
 		)
+		(ntInt Int
+			(0 x3)
+		)
+		(ntJSIdentifier JSIdentifier
+			(
+				Error
+			)
+		)
 	)
 )
+
 (constraint (= (substring "ey" 1) "e"))
 (check-synth)
diff --git a/test/regress/regress1/sygus/issue2935.sy b/test/regress/regress1/sygus/issue2935.sy
index 5616d19f5..ea8011a5e 100644
--- a/test/regress/regress1/sygus/issue2935.sy
+++ b/test/regress/regress1/sygus/issue2935.sy
@@ -1,10 +1,18 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
-(declare-datatype JSIdentifier ((JSInt (jsInt Int)) (JSString (jsString String)) ))
+
+(declare-datatype JSIdentifier ((JSInt (jsInt Int)) (JSString (jsString String))))
 
 (synth-fun f ((x1_ JSIdentifier)(x2_ String)) JSIdentifier
-	((Start JSIdentifier (ntJSIdentifier))
+	((ntJSIdentifier JSIdentifier) (ntInt Int) (ntString String) (ntBool Bool))
+	(
+		(ntJSIdentifier JSIdentifier
+			(x1_
+			(ite ntBool ntJSIdentifier ntJSIdentifier)
+			(JSString ntString)
+			)
+		)
 		(ntInt Int
 			(1
 				(+ ntInt ntInt)
@@ -18,19 +26,15 @@
 			)
 		)
 		(ntBool Bool
-			( 
+			(
 				(= ntString ntString)
 			)
 		)
-		(ntJSIdentifier JSIdentifier
-			( x1_  
-			(ite ntBool ntJSIdentifier ntJSIdentifier)
-			(JSString ntString)
-			)
-		)
 	)
 )
+
 (constraint (= (f (JSString "") "") (JSString "")))
 (constraint (= (f (JSString "M") "W") (JSString "M")))
 (constraint (= (f (JSString "Moon") "") (JSString "on")))
+
 (check-synth)
diff --git a/test/regress/regress1/sygus/issue3320-quant.sy b/test/regress/regress1/sygus/issue3320-quant.sy
index a7b76182e..2d99ba5cf 100644
--- a/test/regress/regress1/sygus/issue3320-quant.sy
+++ b/test/regress/regress1/sygus/issue3320-quant.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
 (declare-var x Int)
 (declare-var y Int)
diff --git a/test/regress/regress1/sygus/issue3649.sy b/test/regress/regress1/sygus/issue3649.sy
index 12949c55a..b650c4ca6 100644
--- a/test/regress/regress1/sygus/issue3649.sy
+++ b/test/regress/regress1/sygus/issue3649.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unknown
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic ALL)
 (synth-fun inv-fn ((i Int) (x (Array Int Int)) (c Int)) Bool)
 
@@ -18,7 +18,6 @@
 (declare-var i! Int)
 (declare-var c Int)
 
-	
 (constraint (=> (init-fn i x c) (inv-fn i x c)))
 (constraint (=> (inv-fn i x c) (post-fn i x c)))
 (check-synth)
diff --git a/test/regress/regress1/sygus/large-const-simp.sy b/test/regress/regress1/sygus/large-const-simp.sy
index 31f660b2a..d93644197 100644
--- a/test/regress/regress1/sygus/large-const-simp.sy
+++ b/test/regress/regress1/sygus/large-const-simp.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-add-const-grammar
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-add-const-grammar
 (set-logic LIA)
 
 (synth-fun lc ((x Int)) Int)
diff --git a/test/regress/regress1/sygus/let-bug-simp.sy b/test/regress/regress1/sygus/let-bug-simp.sy
index 5c2dccff0..1f383ab43 100644
--- a/test/regress/regress1/sygus/let-bug-simp.sy
+++ b/test/regress/regress1/sygus/let-bug-simp.sy
@@ -1,15 +1,19 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
-(define-fun letf ((z Int) (v1 Int) (v2 Int)) Bool  
-  (or 
-    (= v1 z) 
+(define-fun letf ((z Int) (v1 Int) (v2 Int)) Bool
+  (or
+    (= v1 z)
     (= v2 z)))
 (synth-fun f ((x0 Int) (x1 Int)) Bool
+((Start Bool) (StartInt Int) (IntVar Int))
 (
-	(StartInt Int (5))
+  (Start Bool ( (letf StartInt IntVar IntVar) ))
 
-	(Start Bool (  (letf StartInt (Variable Int) (Variable Int)) ))
+  (StartInt Int (5))
+
+  ; "Hack" to avoid parse errors in V2 format.
+  (IntVar Int ((Variable Int)))
 )
 )
 
diff --git a/test/regress/regress1/sygus/list-head-x.sy b/test/regress/regress1/sygus/list-head-x.sy
index 6c5c1a97b..83ac8290d 100644
--- a/test/regress/regress1/sygus/list-head-x.sy
+++ b/test/regress/regress1/sygus/list-head-x.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
 (set-logic ALL_SUPPORTED)
 
 (declare-datatypes ((List 0)) (((cons (head Int) (tail List)) (nil))))
diff --git a/test/regress/regress1/sygus/logiccell_help.sy b/test/regress/regress1/sygus/logiccell_help.sy
index 1ba05e648..d6e8a75a4 100644
--- a/test/regress/regress1/sygus/logiccell_help.sy
+++ b/test/regress/regress1/sygus/logiccell_help.sy
@@ -1,119 +1,118 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-repair-const
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-repair-const
 (set-logic BV)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ; Utils
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(define-sort Bit () (BitVec 1))
+(define-sort Bit () (_ BitVec 1))
 
-(define-fun bit2bool ((b Bit)) Bool 
+(define-fun bit2bool ((b Bit)) Bool
     (= b #b1)
 )
 
-(define-fun extend ((i (BitVec 4))) (BitVec 16)
+(define-fun extend ((i (_ BitVec 4))) (_ BitVec 16)
     (concat #b000000000000 i)
 )
 
-(define-fun extractBit ((i (BitVec 4)) (x (BitVec 16))) Bit
-	((_ extract 0 0) (bvlshr x (extend i)))
+(define-fun extractBit ((i (_ BitVec 4)) (x (_ BitVec 16))) Bit
+    ((_ extract 0 0) (bvlshr x (extend i)))
 )
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ; Arch
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(define-fun lut4 ((i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (lut_val (BitVec 16))) Bit
+(define-fun lut4 ((i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (lut_val (_ BitVec 16))) Bit
     (extractBit (concat i0 i1 i2 i3) lut_val)
 )
 
 (define-fun carry ((i0 Bit) (i1 Bit) (ci Bit)) Bit
-	(bvor (bvand i0 i1) (bvand i0 ci) (bvand i1 ci))
+    (bvor (bvand i0 i1) (bvand i0 ci) (bvand i1 ci))
 )
 
 (define-fun mux2 ((s Bit) (i0 Bit) (i1 Bit)) Bit
     ;(ite (bit2bool s) i0 i1)
-	(bvor (bvand s i0) (bvand (bvnot s) i1))
+    (bvor (bvand s i0) (bvand (bvnot s) i1))
 )
 
 (define-fun logic-cell (
-		(i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (c_in Bit) ; inputs
-		(s Bit) (lut_val (BitVec 16)) ;configs
-	) (BitVec 2) ; Cout O
-	(let (
-		(c_out Bit (carry i1 i2 c_in)) 
-		(l_out Bit (lut4 i0 i1 i2 (mux2 s i3 c_in) lut_val))
-	)
-	(concat c_out l_out)
+        (i0 Bit) (i1 Bit) (i2 Bit) (i3 Bit) (c_in Bit) ; inputs
+        (s Bit) (lut_val (_ BitVec 16)) ;configs
+    ) (_ BitVec 2) ; Cout O
+    (let (
+        (c_out (carry i1 i2 c_in))
+        (l_out (lut4 i0 i1 i2 (mux2 s i3 c_in) lut_val))
+    )
+    (concat c_out l_out)
 ))
 
 (define-fun plb2 (
-		(i_0_0 Bit) (i_0_1 Bit) (i_0_2 Bit) (i_0_3 Bit)
-		(i_1_0 Bit) (i_1_1 Bit) (i_1_2 Bit) (i_1_3 Bit)
-		(c_in Bit)
-		(s_0 Bit) (lut_val_0 (BitVec 16)) ;configs
-		(s_1 Bit) (lut_val_1 (BitVec 16)) ;configs
-	) (BitVec 3)
-	(let ((lc0 (BitVec 2) (logic-cell i_0_0 i_0_1 i_0_2 i_0_3 c_in s_0 lut_val_0)))
-	(let ((lc1 (BitVec 2) (logic-cell i_1_0 i_1_1 i_1_2 i_1_3 ((_ extract 1 1) lc0) s_1 lut_val_1)))
-	(concat lc1 ((_ extract 0 0) lc0))
-	))
+        (i_0_0 Bit) (i_0_1 Bit) (i_0_2 Bit) (i_0_3 Bit)
+        (i_1_0 Bit) (i_1_1 Bit) (i_1_2 Bit) (i_1_3 Bit)
+        (c_in Bit)
+        (s_0 Bit) (lut_val_0 (_ BitVec 16)) ;configs
+        (s_1 Bit) (lut_val_1 (_ BitVec 16)) ;configs
+    ) (_ BitVec 3)
+    (let ((lc0 (logic-cell i_0_0 i_0_1 i_0_2 i_0_3 c_in s_0 lut_val_0)))
+    (let ((lc1 (logic-cell i_1_0 i_1_1 i_1_2 i_1_3 ((_ extract 1 1) lc0) s_1 lut_val_1)))
+    (concat lc1 ((_ extract 0 0) lc0))
+    ))
 )
-	
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ; synth
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(define-fun extract2 ((i (BitVec 1)) (x (BitVec 2))) Bit
-	((_ extract 0 0) (bvlshr x (concat #b0 i)))
+(define-fun extract2 ((i (_ BitVec 1)) (x (_ BitVec 2))) Bit
+    ((_ extract 0 0) (bvlshr x (concat #b0 i)))
 )
 
-(synth-fun f ((x (BitVec 2)) (y (BitVec 2)) (c_in Bit)) (BitVec 3) (
-	(Start (BitVec 3) (
-		(plb2 #b0 (extract2 #b0 x) (extract2 #b0 y) #b0
-			  #b0 (extract2 #b1 x) (extract2 #b1 y) #b0
-			  Cin
-			  S LUT_VAL 
-			  S LUT_VAL)
-	))
-	(Cin Bit (
-		c_in
-		(Constant Bit)
-	))
-	(S Bit (
-		(Constant Bit)
-	))
-	(LUT_VAL (BitVec 16) (	
-		(Constant (BitVec 16))
-	))
+(synth-fun f ((x (_ BitVec 2)) (y (_ BitVec 2)) (c_in Bit)) (_ BitVec 3)
+    ((Start (_ BitVec 3)) (Cin Bit) (S Bit) (LUT_VAL (_ BitVec 16))) (
+    (Start (_ BitVec 3) (
+        (plb2 #b0 (extract2 #b0 x) (extract2 #b0 y) #b0
+              #b0 (extract2 #b1 x) (extract2 #b1 y) #b0
+              Cin
+              S LUT_VAL
+              S LUT_VAL)
+    ))
+    (Cin Bit (
+        c_in
+        (Constant Bit)
+    ))
+    (S Bit (
+        (Constant Bit)
+    ))
+    (LUT_VAL (_ BitVec 16) (
+        (Constant (_ BitVec 16))
+    ))
 ))
 
-(declare-var x (BitVec 2))
-(declare-var y (BitVec 2))
+(declare-var x (_ BitVec 2))
+(declare-var y (_ BitVec 2))
 
-(constraint (= 
-			(bvadd (concat #b0 x) (concat #b0 y))
-			(f x y #b0)
+(constraint (=
+            (bvadd (concat #b0 x) (concat #b0 y))
+            (f x y #b0)
 ))
 
-(constraint (= 
-			(bvadd (bvadd (concat #b0 x) (concat #b0 y)) #b001)
-			(f x y #b1)
+(constraint (=
+            (bvadd (bvadd (concat #b0 x) (concat #b0 y)) #b001)
+            (f x y #b1)
 ))
 
-
 (check-synth)
-	
-;(define-fun lut4_ite ((I0 Bit) (I1 Bit) (I2 Bit) (I3 Bit) (LUT_VAL (BitVec 16))) Bit
-;	(let ((s3 (BitVec 8)  (ite (bit2bool I3) ((_ extract 15 8) LUT_VAL) ((_ extract 7 0) LUT_VAL))))
-;	 (let ((s2 (BitVec 4) (ite (bit2bool I2) ((_ extract 7 4) s3) ((_ extract 3 0) s3))))
-;	  (let ((s1 (BitVec 2) (ite (bit2bool I1) ((_ extract 3 2) s2) ((_ extract 1 0) s2))))
-;	   (let ((s0 (BitVec 1) (ite (bit2bool I0) ((_ extract 1 1) s1) ((_ extract 0 0) s1))))
-;	    s0
-;	   )
-;	  )
-;	 )
-;	)
+
+;(define-fun lut4_ite ((I0 Bit) (I1 Bit) (I2 Bit) (I3 Bit) (LUT_VAL (_ BitVec 16))) Bit
+;    (let ((s3 (_ BitVec 8)  (ite (bit2bool I3) ((_ extract 15 8) LUT_VAL) ((_ extract 7 0) LUT_VAL))))
+;     (let ((s2 (ite (bit2bool I2) ((_ extract 7 4) s3) ((_ extract 3 0) s3))))
+;      (let ((s1 (ite (bit2bool I1) ((_ extract 3 2) s2) ((_ extract 1 0) s2))))
+;       (let ((s0 (ite (bit2bool I0) ((_ extract 1 1) s1) ((_ extract 0 0) s1))))
+;        s0
+;       )
+;      )
+;     )
+;    )
 ;)
diff --git a/test/regress/regress1/sygus/max2-bv.sy b/test/regress/regress1/sygus/max2-bv.sy
index 297bd9179..fa98ef26b 100644
--- a/test/regress/regress1/sygus/max2-bv.sy
+++ b/test/regress/regress1/sygus/max2-bv.sy
@@ -1,26 +1,17 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic BV)
 
-(synth-fun max2 ((x (BitVec 32))(y (BitVec 32))) (BitVec 32)
-)
+(synth-fun max2 ((x (_ BitVec 32)) (y (_ BitVec 32))) (_ BitVec 32))
 
-(declare-var x (BitVec 32))
+(declare-var x (_ BitVec 32))
 
-(declare-var y (BitVec 32))
+(declare-var y (_ BitVec 32))
 
-(constraint 
-(bvuge (max2 x y) x)
-)
+(constraint (bvuge (max2 x y) x))
 
-(constraint 
-(bvuge (max2 x y) y)
-)
+(constraint (bvuge (max2 x y) y))
 
-(constraint 
-(or (= x (max2 x y)) (= y (max2 x y)))
-)
+(constraint (or (= x (max2 x y)) (= y (max2 x y))))
 
 (check-synth)
-
-
diff --git a/test/regress/regress1/sygus/multi-fun-polynomial2.sy b/test/regress/regress1/sygus/multi-fun-polynomial2.sy
index 22a2e0a4b..a20bf853d 100644
--- a/test/regress/regress1/sygus/multi-fun-polynomial2.sy
+++ b/test/regress/regress1/sygus/multi-fun-polynomial2.sy
@@ -1,27 +1,29 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic LIA)
 
 (synth-fun addExpr1 ((x Int) (y Int)) Int
+    ((Start Int))
     ((Start Int (x
                  y
-     0
-     1
+                 0
+                 1
                  (+ Start Start)
                  (- Start Start)
                  ))
-          ))
+    ))
 
 (synth-fun addExpr2 ((x Int) (y Int)) Int
+((Start Int))
     ((Start Int (x
                  y
-     0
-     1
+                 0
+                 1
                  (+ Start Start)
                  (- Start Start)
                  ))
-          ))
+    ))
 
 
 (declare-var x Int)
diff --git a/test/regress/regress1/sygus/nflat-fwd-3.sy b/test/regress/regress1/sygus/nflat-fwd-3.sy
index a1776cf93..f9b6708d5 100644
--- a/test/regress/regress1/sygus/nflat-fwd-3.sy
+++ b/test/regress/regress1/sygus/nflat-fwd-3.sy
@@ -1,11 +1,11 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
+    ((Start Int) (Con Int))
     ((Start Int ((+ (+ Con Con) Con) x))
      (Con Int (0 1))))
 
 (declare-var x Int)
 (constraint (= (f x) 2))
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/nflat-fwd.sy b/test/regress/regress1/sygus/nflat-fwd.sy
index da26a6c93..c36232a5d 100644
--- a/test/regress/regress1/sygus/nflat-fwd.sy
+++ b/test/regress/regress1/sygus/nflat-fwd.sy
@@ -1,11 +1,11 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
+    ((Start Int) (Con Int))
     ((Start Int ((+ Con Con) (+ (+ Start Start) Con) x))
      (Con Int (0 1))))
 
 (declare-var x Int)
 (constraint (= (f x) (* 2 x)))
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/nia-max-square-ns.sy b/test/regress/regress1/sygus/nia-max-square-ns.sy
index 6e7f70ff0..5d63ab023 100644
--- a/test/regress/regress1/sygus/nia-max-square-ns.sy
+++ b/test/regress/regress1/sygus/nia-max-square-ns.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status --nl-ext-tplanes
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --nl-ext-tplanes
 (set-logic NIA)
 
 (synth-fun max ((x Int) (y Int)) Int)
diff --git a/test/regress/regress1/sygus/no-flat-simp.sy b/test/regress/regress1/sygus/no-flat-simp.sy
index c0f0e4c0f..42b73394b 100644
--- a/test/regress/regress1/sygus/no-flat-simp.sy
+++ b/test/regress/regress1/sygus/no-flat-simp.sy
@@ -1,9 +1,10 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic LIA)
 
 (synth-fun f ((x Int) (y Int)) Int
+    ((Start Int))
     ((Start Int (x
                  y
                  0
@@ -15,6 +16,4 @@
 
 (constraint (= (f x y) (+ x y)))
 
-
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/no-mention.sy b/test/regress/regress1/sygus/no-mention.sy
index f964d6039..ff10c1263 100644
--- a/test/regress/regress1/sygus/no-mention.sy
+++ b/test/regress/regress1/sygus/no-mention.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
 
 (synth-fun p ((x Int) (y Int)) Int)
@@ -12,4 +12,3 @@
 (constraint (>= (m x y) x))
 
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/pbe_multi.sy b/test/regress/regress1/sygus/pbe_multi.sy
index 70cb6b2d2..4c588ee17 100644
--- a/test/regress/regress1/sygus/pbe_multi.sy
+++ b/test/regress/regress1/sygus/pbe_multi.sy
@@ -1,27 +1,25 @@
 ; EXPECT: unsat

-; COMMAND-LINE: --sygus-out=status

+; COMMAND-LINE: --lang=sygus2 --sygus-out=status

 (set-logic BV)

 

-(define-fun shr1 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000001))

-(define-fun shr4 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000004))

-(define-fun shr16 ((x (BitVec 64))) (BitVec 64) (bvlshr x #x0000000000000010))

-(define-fun shl1 ((x (BitVec 64))) (BitVec 64) (bvshl x #x0000000000000001))

-(define-fun if0 ((x (BitVec 64)) (y (BitVec 64)) (z (BitVec 64))) (BitVec 64) (ite (= x #x0000000000000001) y z))

-

-(synth-fun f ( (x (BitVec 64))) (BitVec 64)

-(

-

-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)

-                    (shl1 Start)

- 		    (shr1 Start)

-		    (shr4 Start)

-		    (shr16 Start)

-		    (bvand Start Start)

-		    (bvor Start Start)

-		    (bvxor Start Start)

-		    (bvadd Start Start)

-		    (if0 Start Start Start)

- ))

+(define-fun shr1 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000001))

+(define-fun shr4 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000004))

+(define-fun shr16 ((x (_ BitVec 64))) (_ BitVec 64) (bvlshr x #x0000000000000010))

+(define-fun shl1 ((x (_ BitVec 64))) (_ BitVec 64) (bvshl x #x0000000000000001))

+(define-fun if0 ((x (_ BitVec 64)) (y (_ BitVec 64)) (z (_ BitVec 64))) (_ BitVec 64) (ite (= x #x0000000000000001) y z))

+

+(synth-fun f ( (x (_ BitVec 64))) (_ BitVec 64)

+((Start (_ BitVec 64)))

+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)

+            (shl1 Start)

+            (shr1 Start)

+            (shr4 Start)

+            (shr16 Start)

+            (bvand Start Start)

+            (bvor Start Start)

+            (bvxor Start Start)

+            (bvadd Start Start)

+            (if0 Start Start Start)))

 )

 )

 

@@ -37,20 +35,18 @@
 (constraint (= (f #x483db90b3dee6596) #x0000483db90b3dee))

 (constraint (= (f #x55376e703c4a1ea8) #x000055376e703c4a))

 

-(synth-fun g ( (x (BitVec 64))) (BitVec 64)

-(

-

-(Start (BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)

-                    (shl1 Start)

- 		    (shr1 Start)

-		    (shr4 Start)

-		    (shr16 Start)

-		    (bvand Start Start)

-		    (bvor Start Start)

-		    (bvxor Start Start)

-		    (bvadd Start Start)

-		    (if0 Start Start Start)

- ))

+(synth-fun g ( (x (_ BitVec 64))) (_ BitVec 64)

+((Start (_ BitVec 64)))

+((Start (_ BitVec 64) (#x0000000000000000 #x0000000000000001 x (bvnot Start)

+            (shl1 Start)

+            (shr1 Start)

+            (shr4 Start)

+            (shr16 Start)

+            (bvand Start Start)

+            (bvor Start Start)

+            (bvxor Start Start)

+            (bvadd Start Start)

+            (if0 Start Start Start)))

 )

 )

 

diff --git a/test/regress/regress1/sygus/phone-1-long.sy b/test/regress/regress1/sygus/phone-1-long.sy
index 00a031ed4..0b402acf5 100644
--- a/test/regress/regress1/sygus/phone-1-long.sy
+++ b/test/regress/regress1/sygus/phone-1-long.sy
@@ -1,25 +1,21 @@
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-fair=direct

+; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-fair=direct

 ; EXPECT: unsat

 (set-logic SLIA)

- 

+

 (synth-fun f ((name String)) String

-    ((Start String (ntString))

-     (ntString String (name " "

+    ((ntString String) (ntInt Int))

+    ((ntString String (name " "

                        (str.++ ntString ntString)

                        (str.replace ntString ntString ntString)

                        (str.at ntString ntInt)

-                       (int.to.str ntInt)

+                       (str.from_int ntInt)

                        (str.substr ntString ntInt ntInt)))

       (ntInt Int (0 1 2 3 4 5

                   (+ ntInt ntInt)

                   (- ntInt ntInt)

                   (str.len ntString)

-                  (str.to.int ntString)

-                  (str.indexof ntString ntString ntInt)))

-      (ntBool Bool (true false

-                    (str.prefixof ntString ntString)

-                    (str.suffixof ntString ntString)

-                    (str.contains ntString ntString)))))

+                  (str.to_int ntString)

+                  (str.indexof ntString ntString ntInt)))))

 

 (declare-var name String)

 (constraint (= (f "938-242-504") "242"))

diff --git a/test/regress/regress1/sygus/planning-unif.sy b/test/regress/regress1/sygus/planning-unif.sy
index 3a715501a..212c25595 100644
--- a/test/regress/regress1/sygus/planning-unif.sy
+++ b/test/regress/regress1/sygus/planning-unif.sy
@@ -1,8 +1,8 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-unif-pi=complete --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-unif-pi=complete --sygus-out=status
 (set-logic LIA)
 
-(define-fun get-y ((currPoint Int)) Int 
+(define-fun get-y ((currPoint Int)) Int
 (ite (< currPoint 10) 0 (ite (< currPoint 20) 1 (ite (< currPoint 30) 2 (ite (< currPoint 40) 3 (ite (< currPoint 50) 4 (ite (< currPoint 60) 5 (ite (< currPoint 70) 6 (ite (< currPoint 80) 7 (ite (< currPoint 90) 8 9))))))))))
 
 (define-fun get-x ((currPoint Int)) Int
@@ -11,19 +11,19 @@
 (ite (= move 0) currPoint 
 (ite (= move 1)  (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10))     currPoint (+ currPoint  10)) 
 (ite (= move 2)  (ite (or (< (+ (get-x currPoint) 1) 0) (>= (+ (get-x currPoint) 1) 10))     currPoint (+ currPoint  1)) 
-(ite (= move 3)  (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10))     currPoint (+ currPoint  -10)) 
-(ite (= move 4)  (ite (or (< (+ (get-x currPoint) -1) 0) (>= (+ (get-x currPoint) -1) 10))     currPoint (+ currPoint  -1)) 
+(ite (= move 3)  (ite (or (< (+ (get-y currPoint)(- 1)) 0) (>= (+ (get-y currPoint)(- 1)) 10))     currPoint (+ currPoint (- 10))) 
+(ite (= move 4)  (ite (or (< (+ (get-x currPoint)(- 1)) 0) (>= (+ (get-x currPoint)(- 1)) 10))     currPoint (+ currPoint (- 1))) 
 currPoint))))))
 
 (define-fun interpret-move-obstacle-0 (( currPoint Int ) ( move Int)) Int
 (ite (= move 0)  (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10))     currPoint (+ currPoint  10)) 
-(ite (= move 1)  (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10))     currPoint (+ currPoint  -10)) 
+(ite (= move 1)  (ite (or (< (+ (get-y currPoint)(- 1)) 0) (>= (+ (get-y currPoint)(- 1)) 10))     currPoint (+ currPoint (- 10))) 
 currPoint)))
 
 (define-fun interpret-move-obstacle-1 (( currPoint Int ) ( move Int)) Int
 (ite (= move 0)  (ite (or (< (+ (get-y currPoint) 1) 0) (>= (+ (get-y currPoint) 1) 10))     currPoint (+ currPoint  10)) 
 (ite (= move 1) currPoint 
-(ite (= move 2)  (ite (or (< (+ (get-y currPoint) -1) 0) (>= (+ (get-y currPoint) -1) 10))     currPoint (+ currPoint  -10)) 
+(ite (= move 2)  (ite (or (< (+ (get-y currPoint)(- 1)) 0) (>= (+ (get-y currPoint)(- 1)) 10))     currPoint (+ currPoint (- 10))) 
 currPoint))))
 
 (define-fun allowable-move-obstacle-0 (( start Int ) ( end Int)) Bool
@@ -37,12 +37,12 @@ currPoint))))
 
 (define-fun get-move-obstacle-0 (( start Int ) ( end Int)) Int
 	(ite (= (interpret-move-obstacle-0 start 0) end) 0 
-	(ite (= (interpret-move-obstacle-0 start 1) end) 1  -1)))
+	(ite (= (interpret-move-obstacle-0 start 1) end) 1 (- 1))))
 
 (define-fun get-move-obstacle-1 (( start Int ) ( end Int)) Int
 	(ite (= (interpret-move-obstacle-1 start 0) end) 0 
 	(ite (= (interpret-move-obstacle-1 start 1) end) 1 
-	(ite (= (interpret-move-obstacle-1 start 2) end) 2  -1))))
+	(ite (= (interpret-move-obstacle-1 start 2) end) 2 (- 1)))))
 
 (define-fun no-overlap-one-move-combination-2-2 ((p0 Int) (p1 Int) (p2 Int) (p3 Int)) Bool
 	(and (not (= p0 p2)) (and (not (= p0 p3)) (and (not (= p1 p2)) (and (not (= p1 p3)) true)))))
@@ -51,42 +51,42 @@ currPoint))))
 	(= 1
 	(ite (= move 0) 
 		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
-		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0)(- 10))) 1 0) 0))
 	(ite (= move 1) 
 		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
-		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0)(- 10))) 1 0) 0))
 	(ite (= move 2) 
 		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
-		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0)(- 10))) 1 0) 0))
 	(ite (= move 3) 
-		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
-		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0)(- 10)) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0)(- 10)) obstacleCurrPoint (+ (+ obstacleCurrPoint 0)(- 10))) 1 0) 0))
 	(ite (= move 4) 
-		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
-		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)) 0)))))))
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint(- 1)) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint(- 1)) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0)(- 10))) 1 0) 0)) 0)))))))
 
 (define-fun no-overlaps-1 (( currPoint Int ) ( move Int) (obstacleCurrPoint Int) (obstacleMove Int)) Bool
 	(= 1
 	(ite (= move 0) 
 		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
 		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
-		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
+		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0)(- 10))) 1 0) 0)))
 	(ite (= move 1) 
 		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
 		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
-		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
+		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) 10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0)(- 10))) 1 0) 0)))
 	(ite (= move 2) 
 		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
 		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
-		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
+		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0)(- 10))) 1 0) 0)))
 	(ite (= move 3) 
-		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
-		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
-		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0) -10) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0)))
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0)(- 10)) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0)(- 10)) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
+		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint 0)(- 10)) obstacleCurrPoint (+ (+ obstacleCurrPoint 0)(- 10))) 1 0) 0)))
 	(ite (= move 4) 
-		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
-		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
-		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint -1) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) -10)) 1 0) 0))) 0)))))))
+		(ite (= obstacleMove 0) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint(- 1)) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 10)) 1 0)
+		(ite (= obstacleMove 1) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint(- 1)) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0) 0)) 1 0)
+		(ite (= obstacleMove 2) (ite (no-overlap-one-move-combination-2-2 currPoint (+ (+ currPoint(- 1)) 0) obstacleCurrPoint (+ (+ obstacleCurrPoint 0)(- 10))) 1 0) 0))) 0)))))))
 
 (define-fun no-overlaps-one-step-helper ((currPoint Int) (move Int) (o0-t Int) (o0move Int) (o1-t Int) (o1move Int)) Bool
 	(and (no-overlaps-0 currPoint move o0-t o0move) (and (no-overlaps-1 currPoint move o1-t o1move) true)))
@@ -104,15 +104,16 @@ currPoint))))
 (declare-var o1-3 Int)
 
 (synth-fun move ((currPoint Int) (o0 Int) (o1 Int)) Int
+	((Start Int) (MoveId Int) (CondInt Int) (StartBool Bool))
 	((Start Int (
 		MoveId
 		(ite StartBool Start Start)))
-    (MoveId Int (0
+	(MoveId Int (0
 		1
 		2
 		3
 		4
-  	))
+	))
 	(CondInt Int (
 		(get-y currPoint) ;y coord
 		(get-x currPoint) ;x coord
@@ -122,7 +123,7 @@ currPoint))))
 		(get-x o1)
 		(+ CondInt CondInt)
 		(- CondInt CondInt)
-		-1
+		(- 1)
 		0
 		1
 		2
@@ -133,15 +134,15 @@ currPoint))))
 		7
 		8
 		9
-				))
+	))
 	(StartBool Bool ((and StartBool StartBool)
 		(or  StartBool StartBool)
 		(not StartBool)
 		(<=  CondInt CondInt)
 		(=   CondInt CondInt)
-		(>=  CondInt CondInt))))) 
- 
- (constraint (or 
+		(>=  CondInt CondInt)))))
+
+(constraint (or
 	(and
 		(= (interpret-move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) (move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) o0-2 o1-2)) 30)
 		(and (no-overlaps-one-step 0 (move 0 99 98) 99 o0-1 98 o1-1) (and (no-overlaps-one-step (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1) o0-1 o0-2 o1-1 o1-2) (and (no-overlaps-one-step (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) (move (interpret-move (interpret-move 0 (move 0 99 98)) (move (interpret-move 0 (move 0 99 98)) o0-1 o1-1)) o0-2 o1-2) o0-2 o0-3 o1-2 o1-3) true))))
diff --git a/test/regress/regress1/sygus/process-10-vars.sy b/test/regress/regress1/sygus/process-10-vars.sy
index 77990473f..6a9a80a49 100644
--- a/test/regress/regress1/sygus/process-10-vars.sy
+++ b/test/regress/regress1/sygus/process-10-vars.sy
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status --sygus-arg-relevant
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status --sygus-arg-relevant
 ; EXPECT: unsat
 (set-logic LIA)
 
diff --git a/test/regress/regress1/sygus/qe.sy b/test/regress/regress1/sygus/qe.sy
index 77e16efcb..c8d56229a 100644
--- a/test/regress/regress1/sygus/qe.sy
+++ b/test/regress/regress1/sygus/qe.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status --sygus-qe-preproc
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status --sygus-qe-preproc
 (set-logic LIA)
 
 (synth-fun f ((x Int)) Int)
diff --git a/test/regress/regress1/sygus/real-any-const.sy b/test/regress/regress1/sygus/real-any-const.sy
index 2b59b7301..431d0c1b0 100644
--- a/test/regress/regress1/sygus/real-any-const.sy
+++ b/test/regress/regress1/sygus/real-any-const.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term-concise
 
 (set-logic LRA)
 (synth-fun f ((x Real) (y Real)) Real)
diff --git a/test/regress/regress1/sygus/real-grammar.sy b/test/regress/regress1/sygus/real-grammar.sy
index c2f4ae0bc..128a94c1d 100644
--- a/test/regress/regress1/sygus/real-grammar.sy
+++ b/test/regress/regress1/sygus/real-grammar.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --cegqi-si=none
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --cegqi-si=none
 
 (set-logic LRA)
 
diff --git a/test/regress/regress1/sygus/sets-pred-test.sy b/test/regress/regress1/sygus/sets-pred-test.sy
index 284325712..f45329b27 100644
--- a/test/regress/regress1/sygus/sets-pred-test.sy
+++ b/test/regress/regress1/sygus/sets-pred-test.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic ALL)
 (synth-fun P ((x (Set Int))) Bool)
 
diff --git a/test/regress/regress1/sygus/stopwatch-bt.sy b/test/regress/regress1/sygus/stopwatch-bt.sy
index 291ae6099..c33e16bcd 100644
--- a/test/regress/regress1/sygus/stopwatch-bt.sy
+++ b/test/regress/regress1/sygus/stopwatch-bt.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-inv-templ=post --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-inv-templ=post --sygus-out=status
 (set-logic LIA)
 
 (define-fun
@@ -116,14 +116,6 @@
 ))
 
 
-(declare-primed-var stopwatch.usr.toggle Bool)
-(declare-primed-var stopwatch.usr.reset Bool)
-(declare-primed-var stopwatch.usr.count Int)
-(declare-primed-var stopwatch.res.init_flag Bool)
-(declare-primed-var stopwatch.res.abs_0 Bool)
-(declare-primed-var stopwatch.impl.usr.running Bool)
-(declare-primed-var stopwatch.res.abs_1 Int)
-(declare-primed-var stopwatch.res.inst_0 Bool)
 
 (define-fun
   init (
diff --git a/test/regress/regress1/sygus/strings-any-term1.sy b/test/regress/regress1/sygus/strings-any-term1.sy
index 3d8fd7530..cca2edb2c 100644
--- a/test/regress/regress1/sygus/strings-any-term1.sy
+++ b/test/regress/regress1/sygus/strings-any-term1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --no-sygus-pbe --cegqi-si=none --sygus-grammar-cons=any-term
 (set-logic ALL)
 (synth-fun f ((x String) (y String)) Int)
 (declare-var x String)
diff --git a/test/regress/regress1/sygus/strings-concat-3-args.sy b/test/regress/regress1/sygus/strings-concat-3-args.sy
index 6628ff746..681d3ccff 100644
--- a/test/regress/regress1/sygus/strings-concat-3-args.sy
+++ b/test/regress/regress1/sygus/strings-concat-3-args.sy
@@ -1,10 +1,10 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
 (synth-fun f ((x String)) String
-((Start String (ntString))
+((ntString String) (ntStringConst String))
 
-(ntString String (x "" (str.++ ntStringConst ntString ntString)))
+((ntString String (x "" (str.++ ntStringConst ntString ntString)))
 
 (ntStringConst String ("a" "b" " "))
 
@@ -15,4 +15,3 @@
 (constraint (= (f "def") "ab def"))
 
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/strings-double-rec.sy b/test/regress/regress1/sygus/strings-double-rec.sy
index ea9caadea..0c21015e7 100644
--- a/test/regress/regress1/sygus/strings-double-rec.sy
+++ b/test/regress/regress1/sygus/strings-double-rec.sy
@@ -1,8 +1,9 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
- 
+
 (synth-fun f ((name String)) String
+    ((Start String) (Start1 String) (Start2 String))
     ((Start String (name "A" "B" "" (str.++ Start1 Start2)))
      (Start1 String (name "A" "B" ""))
      (Start2 String (name "B" "A" (str.++ Start2 Start)))
@@ -10,7 +11,7 @@
 
 
 (declare-var name String)
- 
+
 (constraint (= (f "BB") "AAAAAAAAAAAA"))
- 
+
 (check-synth)
diff --git a/test/regress/regress1/sygus/strings-no-syntax.sy b/test/regress/regress1/sygus/strings-no-syntax.sy
index 4959d6fe1..8abb33f33 100644
--- a/test/regress/regress1/sygus/strings-no-syntax.sy
+++ b/test/regress/regress1/sygus/strings-no-syntax.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic ALL)
 
 (synth-fun f ((x String) (y String)) String)
diff --git a/test/regress/regress1/sygus/strings-small.sy b/test/regress/regress1/sygus/strings-small.sy
index 7d976ff39..834898b02 100644
--- a/test/regress/regress1/sygus/strings-small.sy
+++ b/test/regress/regress1/sygus/strings-small.sy
@@ -1,27 +1,27 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
 (synth-fun f ((firstname String) (lastname String)) String
-((Start String (ntString))
+((ntString String) (ntInt Int) (ntBool Bool))
 
-(ntString String (
-firstname 
-lastname 
+((ntString String (
+firstname
+lastname
 " "
 (str.++ ntString ntString)))
 
 (ntInt Int (
-0 
-1 
+0
+1
 2
 (+ ntInt ntInt)
 (- ntInt ntInt)
 (str.len ntString)
-(str.to.int ntString)
+(str.to_int ntString)
 (str.indexof ntString ntString ntInt)))
 
 (ntBool Bool (
-true 
+true
 false
 (str.prefixof ntString ntString)
 (str.suffixof ntString ntString)
@@ -32,4 +32,3 @@ false
 (constraint (= (f "Nancy" "FreeHafer") "Nancy FreeHafer"))
 
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/strings-template-infer-unused.sy b/test/regress/regress1/sygus/strings-template-infer-unused.sy
index d0bee5564..2c075388a 100644
--- a/test/regress/regress1/sygus/strings-template-infer-unused.sy
+++ b/test/regress/regress1/sygus/strings-template-infer-unused.sy
@@ -1,16 +1,17 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
- 
+
 (define-fun cA ((x String) (w String) (y String) (z String)) String (str.++ (str.++ x "A") y))
- 
+
 (synth-fun f ((name String)) String
+    ((Start String))
     ((Start String (name "A" "B" ""
-                       (cA Start Start Start Start)))))
+                        (cA Start Start Start Start)))))
 
 
 (declare-var name String)
- 
+
 (constraint (= (f "BB") "AAAAAAAAAAAA"))
- 
+
 (check-synth)
diff --git a/test/regress/regress1/sygus/strings-template-infer.sy b/test/regress/regress1/sygus/strings-template-infer.sy
index 13c4d7dac..8cbce19b6 100644
--- a/test/regress/regress1/sygus/strings-template-infer.sy
+++ b/test/regress/regress1/sygus/strings-template-infer.sy
@@ -1,16 +1,17 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
- 
+
 (define-fun cA ((x String) (y String)) String (str.++ (str.++ x "A") y))
- 
+
 (synth-fun f ((name String)) String
+    ((Start String))
     ((Start String (name "A" "B" ""
-                       (cA Start Start)))))
+                        (cA Start Start)))))
 
 
 (declare-var name String)
- 
+
 (constraint (= (f "BB") "AAAAAAAAAAAA"))
- 
+
 (check-synth)
diff --git a/test/regress/regress1/sygus/strings-trivial-simp.sy b/test/regress/regress1/sygus/strings-trivial-simp.sy
index f5e41a8f5..c0e3f0ea6 100644
--- a/test/regress/regress1/sygus/strings-trivial-simp.sy
+++ b/test/regress/regress1/sygus/strings-trivial-simp.sy
@@ -1,14 +1,15 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
- 
+
 (synth-fun f ((name String)) String
+    ((Start String))
     ((Start String (name "A" "B"
-                       (str.++ Start Start)))))
+                        (str.++ Start Start)))))
 
 
 (declare-var name String)
- 
+
 (constraint (= (f "BB") "AAAAAAAAAAAABAAAAAAAABAAA"))
- 
+
 (check-synth)
diff --git a/test/regress/regress1/sygus/strings-trivial-two-type.sy b/test/regress/regress1/sygus/strings-trivial-two-type.sy
index 86c71aa3a..ba9ac5064 100644
--- a/test/regress/regress1/sygus/strings-trivial-two-type.sy
+++ b/test/regress/regress1/sygus/strings-trivial-two-type.sy
@@ -1,18 +1,17 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
- 
+
 (synth-fun f ((name String)) String
-    ((Start String (ntString))
-     (ntString String (name "B" ""
-                       (str.++ ntStringC ntString)))
+    ((ntString String) (ntStringC String))
+    ((ntString String (name "B" ""
+                        (str.++ ntStringC ntString)))
      (ntStringC String (name "A" ""))
-                       
-                       ))
+    ))
 
 
 (declare-var name String)
- 
+
 (constraint (= (f "B") "AAAAAAAAAAAAAAAAAAAAAAAAA"))
- 
+
 (check-synth)
diff --git a/test/regress/regress1/sygus/strings-trivial.sy b/test/regress/regress1/sygus/strings-trivial.sy
index 9af0a1bb1..7fe96cf14 100644
--- a/test/regress/regress1/sygus/strings-trivial.sy
+++ b/test/regress/regress1/sygus/strings-trivial.sy
@@ -1,15 +1,15 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic SLIA)
- 
+
 (synth-fun f ((name String)) String
-    ((Start String (ntString))
-     (ntString String (name "A" "B"
-                       (str.++ ntString ntString)))))
+    ((ntString String))
+    ((ntString String (name "A" "B"
+                        (str.++ ntString ntString)))))
 
 
 (declare-var name String)
- 
+
 (constraint (= (f "B") "AAAAAAAAAAAAAAAAAAAAAAAAA"))
- 
+
 (check-synth)
diff --git a/test/regress/regress1/sygus/sygus-dt.sy b/test/regress/regress1/sygus/sygus-dt.sy
index 336c59b27..7539fdd0d 100644
--- a/test/regress/regress1/sygus/sygus-dt.sy
+++ b/test/regress/regress1/sygus/sygus-dt.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --decision=justification
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --decision=justification
 
 (set-logic LIA)
 
@@ -7,8 +7,10 @@
 (define-fun g ((x Int)) List (cons (+ x 1) nil))
 (define-fun i () List (cons 3 nil))
 
-(synth-fun f ((x Int)) List ((Start List ((g StartInt) i (cons StartInt Start) nil (tail Start)))
-                             (StartInt Int (x 0 1 (+ StartInt StartInt)))))
+(synth-fun f ((x Int)) List
+    ((Start List) (StartInt Int))
+    ((Start List ((g StartInt) i (cons StartInt Start) nil (tail Start)))
+     (StartInt Int (x 0 1 (+ StartInt StartInt)))))
 
 (declare-var x Int)
 
diff --git a/test/regress/regress1/sygus/sygus-lambda-fv.sy b/test/regress/regress1/sygus/sygus-lambda-fv.sy
index d2a3700ce..d96960c83 100644
--- a/test/regress/regress1/sygus/sygus-lambda-fv.sy
+++ b/test/regress/regress1/sygus/sygus-lambda-fv.sy
@@ -1,10 +1,11 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic ALL)
 
-(synth-fun SC ((y (BitVec 32)) (w (BitVec 32)) ) (BitVec 32)
+(synth-fun SC ((y (_ BitVec 32)) (w (_ BitVec 32)) ) (_ BitVec 32)
+  ((Start (_ BitVec 32)) (StartBool Bool))
   (
-   (Start (BitVec 32) (
+   (Start (_ BitVec 32) (
      y
      w
      #x00000000
diff --git a/test/regress/regress1/sygus/t8.sy b/test/regress/regress1/sygus/t8.sy
index 4dd726875..6ac904832 100644
--- a/test/regress/regress1/sygus/t8.sy
+++ b/test/regress/regress1/sygus/t8.sy
@@ -1,31 +1,30 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
-(set-logic  LIA)
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
+(set-logic LIA)
 (
-synth-fun f_143-17-143-55 ( (x2 Int) (x1 Int) (parentNode Int) (EMPTY_PARENT Int)) Bool
-	((Start Bool (
-(< IntExpr IntExpr)
-(and Start Start)
-(= IntExpr IntExpr)
-(not Start )
-(<= IntExpr IntExpr)
-(or Start Start)
-
-
-
-))
-(IntExpr Int (
-x2 x1 parentNode EMPTY_PARENT 
-0 1
-))
-
-	)
+synth-fun f_143-17-143-55 ((x2 Int) (x1 Int) (parentNode Int) (EMPTY_PARENT Int)) Bool
+((Start Bool) (IntExpr Int))
+(
+	(Start Bool (
+		(< IntExpr IntExpr)
+		(and Start Start)
+		(= IntExpr IntExpr)
+		(not Start)
+		(<= IntExpr IntExpr)
+		(or Start Start)
+	))
+	(IntExpr Int (
+		x2 x1 parentNode EMPTY_PARENT 
+		0 1
+	))
+)
 )
+
 (declare-var x2_143-17-143-55 Int)
 (declare-var x1_143-17-143-55 Int)
 (declare-var parentNode_143-17-143-55 Int)
 (declare-var EMPTY_PARENT_143-17-143-55 Int)
 
-(constraint  (=>  (and (= parentNode_143-17-143-55 0)  (and (= EMPTY_PARENT_143-17-143-55 -1)  (and (= x2_143-17-143-55 1) (= x1_143-17-143-55 1)) ) )  (= (f_143-17-143-55 x2_143-17-143-55 x1_143-17-143-55 parentNode_143-17-143-55 EMPTY_PARENT_143-17-143-55 ) true)))
+(constraint (=> (and (= parentNode_143-17-143-55 0) (and (= EMPTY_PARENT_143-17-143-55 (- 1)) (and (= x2_143-17-143-55 1) (= x1_143-17-143-55 1)))) (= (f_143-17-143-55 x2_143-17-143-55 x1_143-17-143-55 parentNode_143-17-143-55 EMPTY_PARENT_143-17-143-55) true)))
 
 (check-synth)
diff --git a/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy
index 4efd90314..fa8bdc2d7 100644
--- a/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy
+++ b/test/regress/regress1/sygus/temp_input_to_synth_ic-error-121418.sy
@@ -1,9 +1,10 @@
 ; REQUIRES: symfpu
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic ALL)
 (define-sort FP () (_ FloatingPoint 3 5))
 (synth-fun IC ((t FP)) Bool
+  ((Start Bool) (StartFP FP) (StartRM RoundingMode))
   ((Start Bool (
      true
      false
diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy
index 282bc122c..c5b72b009 100644
--- a/test/regress/regress1/sygus/tester.sy
+++ b/test/regress/regress1/sygus/tester.sy
@@ -1,15 +1,15 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic DTSLIA)
 (declare-datatype DT ((A (a Int)) (B (b String)) (JSBool (jsBool Bool))))
 
-(define-fun isA ((i DT)) Bool ((_ is A) i) )
-(define-fun isB ((i DT)) Bool ((_ is B) i) )
+(define-fun isA ((i DT)) Bool ((_ is A) i))
+(define-fun isB ((i DT)) Bool ((_ is B) i))
 
 (synth-fun add ((x1 DT)) DT
+	((ntDT DT) (ntBool Bool) (ntInt Int))
 	(
-		(Start DT (ntDT))
 		(ntDT DT
 			( x1
 				(JSBool ntBool)
diff --git a/test/regress/regress1/sygus/tl-type-0.sy b/test/regress/regress1/sygus/tl-type-0.sy
index ceda89d78..0beea8056 100644
--- a/test/regress/regress1/sygus/tl-type-0.sy
+++ b/test/regress/regress1/sygus/tl-type-0.sy
@@ -1,11 +1,11 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
+    ((Start Int) (Term Int))
     ((Start Int ((+ Term Term)))
      (Term Int (x 0))))
 
 (declare-var x Int)
 (constraint (= (f x) 0))
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/tl-type-4x.sy b/test/regress/regress1/sygus/tl-type-4x.sy
index bf8eee5ee..7c4403397 100644
--- a/test/regress/regress1/sygus/tl-type-4x.sy
+++ b/test/regress/regress1/sygus/tl-type-4x.sy
@@ -1,11 +1,11 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
+    ((Start Int) (Term Int))
     ((Start Int (Term (+ Start Start)))
      (Term Int (x 0))))
 
 (declare-var x Int)
 (constraint (= (f x) (* 4 x)))
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/tl-type.sy b/test/regress/regress1/sygus/tl-type.sy
index 6f25a570e..fe39ddd8e 100644
--- a/test/regress/regress1/sygus/tl-type.sy
+++ b/test/regress/regress1/sygus/tl-type.sy
@@ -1,11 +1,11 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=none --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=none --sygus-out=status
 (set-logic LIA)
 (synth-fun f ((x Int)) Int
+    ((Start Int) (Term Int))
     ((Start Int (Term (+ Start Start)))
      (Term Int (x 0))))
 
 (declare-var x Int)
 (constraint (= (f x) (* 3 x)))
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/triv-type-mismatch-si.sy b/test/regress/regress1/sygus/triv-type-mismatch-si.sy
index 37c5a7f53..6ef891560 100644
--- a/test/regress/regress1/sygus/triv-type-mismatch-si.sy
+++ b/test/regress/regress1/sygus/triv-type-mismatch-si.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
 
 (synth-fun R ((y Int)) Bool)
@@ -10,4 +10,3 @@
 (constraint (=> (= x e) (R x)))
 
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/trivial-stream.sy b/test/regress/regress1/sygus/trivial-stream.sy
index 33abb6ee8..8d3e91b06 100644
--- a/test/regress/regress1/sygus/trivial-stream.sy
+++ b/test/regress/regress1/sygus/trivial-stream.sy
@@ -3,15 +3,16 @@
 ; EXPECT: (error "Maximum term size (0) for enumerative SyGuS exceeded.")
 ; EXIT: 1
 
-; COMMAND-LINE: --sygus-stream --sygus-abort-size=0 --sygus-active-gen=var-agnostic
+; COMMAND-LINE: --lang=sygus2 --sygus-stream --sygus-abort-size=0 --sygus-active-gen=var-agnostic
 
 (set-logic LIA)
 
 (synth-fun triv ((x Int) (y Int)) Int
+    ((Start Int))
     ((Start Int (x
                  y
                  (+ Start Start)
                  ))
-          ))
+    ))
 
 (check-synth)
diff --git a/test/regress/regress1/sygus/twolets1.sy b/test/regress/regress1/sygus/twolets1.sy
index 06d2ecb71..b78bf7647 100644
--- a/test/regress/regress1/sygus/twolets1.sy
+++ b/test/regress/regress1/sygus/twolets1.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 
 ;; f1 is x plus 2 ;; f2 is 2x plus 5
@@ -7,6 +7,7 @@
 (define-fun let0 ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
 
 (synth-fun f1 ((x Int)) Int
+     ((Start Int) (Intx Int) (CInt Int))
      (
      (Start Int (
             (let0 Intx CInt CInt)
@@ -14,11 +15,11 @@
      )
      (Intx Int (x))
      (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
-
      )
 )
 
 (synth-fun f2 ((x Int)) Int
+     ((Start Int) (Intx Int) (CInt Int))
      (
      (Start Int (x
             (let0 Intx Start CInt)
@@ -26,15 +27,13 @@
      )
      (Intx Int (x))
      (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
-
      )
 )
 
 
 (declare-var x Int)
 
-(constraint (= (+ (f1 x)(f2 x)) (+ (+ x x) (+ x 8))))
-(constraint (= (- (f2 x)(f1 x)) (+ x 2)))
+(constraint (= (+ (f1 x) (f2 x)) (+ (+ x x) (+ x 8))))
+(constraint (= (- (f2 x) (f1 x)) (+ x 2)))
 
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/twolets2-orig.sy b/test/regress/regress1/sygus/twolets2-orig.sy
index a92c0b014..ca1e512a1 100644
--- a/test/regress/regress1/sygus/twolets2-orig.sy
+++ b/test/regress/regress1/sygus/twolets2-orig.sy
@@ -1,29 +1,28 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --cegqi-si=all --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --cegqi-si=all --sygus-out=status
 (set-logic LIA)
 (define-fun letf ((x Int) (y Int) (z Int)) Int (+ (+ y x) z))
 (synth-fun f1 ((x Int)) Int
+     ((Start Int) (CInt Int))
      (
      (Start Int (
             (letf x CInt CInt)
             )
      )
      (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
-
      )
 )
 (synth-fun f2 ((x Int)) Int
+     ((Start Int) (CInt Int))
      (
      (Start Int (x
             (letf x Start CInt)
             )
      )
      (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
-
      )
 )
 (declare-var x1 Int)
 (declare-var x2 Int)
-(constraint (= (+ (f1 x1)(f2 x2)) (+ (+ x2 x2) (+ x1 8))))
+(constraint (= (+ (f1 x1) (f2 x2)) (+ (+ x2 x2) (+ x1 8))))
 (check-synth)
-
diff --git a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy b/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
index 73d410d51..34abb6de8 100644
--- a/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
+++ b/test/regress/regress1/sygus/unbdd_inv_gen_ex7.sy
@@ -1,14 +1,15 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 (set-logic LIA)
 (synth-fun inv ((i Int) (y Int) (l Int)) Bool
+    ((Start Bool) (AtomicFormula Bool) (Sum Int) (Term Int) (Sign Int) (Var Int) (Const Int))
     (
         (Start Bool ((and AtomicFormula AtomicFormula)
                      (or AtomicFormula AtomicFormula)))
         (AtomicFormula Bool ((<= Sum Const) (= Sum Const)))
         (Sum Int ((+ Term Term)))
         (Term Int ((* Sign Var)))
-        (Sign Int (0 1 -1))
+        (Sign Int (0 1 (- 1)))
         (Var Int (i y l))
         (Const Int ((+ Const Const) (- Const Const) 0 1))
     )
@@ -35,6 +36,6 @@
 (constraint (implies (or3 (< x 0) (< y 0) (> y x)) true))
 (constraint (implies (and3 (not (or3 (< x 0) (< y 0) (> y x))) (= l x) (= i 0)) (inv i y l)))
 (constraint (implies (and4 (inv i y l) (< i y) (not (or (< i 0) (>= i l))) (= i1 (+ i 1))) (inv i1 y l)))
-(constraint (implies (and3 (inv i y l) (< i y) (or (< i 0) (>= i  l))) false))
+(constraint (implies (and3 (inv i y l) (< i y) (or (< i 0) (>= i l))) false))
 
 (check-synth)
diff --git a/test/regress/regress1/sygus/unbdd_inv_gen_winf1.sy b/test/regress/regress1/sygus/unbdd_inv_gen_winf1.sy
index d45cec38b..edfc2176b 100644
--- a/test/regress/regress1/sygus/unbdd_inv_gen_winf1.sy
+++ b/test/regress/regress1/sygus/unbdd_inv_gen_winf1.sy
@@ -1,15 +1,16 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status
 
 (set-logic LIA)
 (synth-fun inv ((x Int)) Bool
+    ((Start Bool) (AtomicFormula Bool) (Sum Int) (Term Int) (Sign Int) (Var Int) (Const Int))
     (
         (Start Bool ((and AtomicFormula AtomicFormula)
                      (or AtomicFormula AtomicFormula)))
         (AtomicFormula Bool ((<= Sum Const) (= Sum Const)))
         (Sum Int ((+ Term Term)))
         (Term Int ((* Sign Var)))
-        (Sign Int (0 1 -1))
+        (Sign Int (0 1 (- 1)))
         (Var Int (x))
         (Const Int ((+ Const Const) (- Const Const) 0 1))
     )
diff --git a/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy b/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy
index 38267c10d..c1d196f60 100644
--- a/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy
+++ b/test/regress/regress1/sygus/unifpi-solve-car_1.lus.sy
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-; COMMAND-LINE: --sygus-out=status --sygus-grammar-cons=any-term-concise --sygus-unif-pi=complete
+; COMMAND-LINE: --lang=sygus2 --sygus-out=status --sygus-grammar-cons=any-term-concise --sygus-unif-pi=complete
 
 (set-logic LIA)
 
@@ -189,11 +189,11 @@
   ) Bool
 
   (let
-   ((X1 Int top.res.abs_3_a_0))
+   ((X1 top.res.abs_3_a_0))
    (and
     (= top.res.abs_10_a_0 (and top.res.abs_9_a_0 (< X1 32767)))
     (let
-     ((X2 Bool top.res.abs_11_a_0))
+     ((X2 top.res.abs_11_a_0))
      (and
       (= top.usr.OK_a_0 (=> X2 (>= X1 0)))
       (__node_init_voiture_0
@@ -267,11 +267,11 @@
   ) Bool
 
   (let
-   ((X1 Int top.res.abs_3_a_1))
+   ((X1 top.res.abs_3_a_1))
    (and
     (= top.res.abs_10_a_1 (and top.res.abs_9_a_1 (< X1 32767)))
     (let
-     ((X2 Bool top.res.abs_11_a_1))
+     ((X2 top.res.abs_11_a_1))
      (and
       (= top.usr.OK_a_1 (=> X2 (>= X1 0)))
       (__node_trans_voiture_0
@@ -346,26 +346,6 @@
 ))
 
 
-(declare-primed-var top.usr.m Bool)
-(declare-primed-var top.usr.s Bool)
-(declare-primed-var top.usr.OK Bool)
-(declare-primed-var top.res.init_flag Bool)
-(declare-primed-var top.res.abs_0 Bool)
-(declare-primed-var top.res.abs_1 Bool)
-(declare-primed-var top.res.abs_2 Bool)
-(declare-primed-var top.res.abs_3 Int)
-(declare-primed-var top.res.abs_4 Int)
-(declare-primed-var top.res.abs_5 Int)
-(declare-primed-var top.res.abs_6 Bool)
-(declare-primed-var top.res.abs_7 Bool)
-(declare-primed-var top.res.abs_8 Bool)
-(declare-primed-var top.res.abs_9 Bool)
-(declare-primed-var top.res.abs_10 Bool)
-(declare-primed-var top.res.abs_11 Bool)
-(declare-primed-var top.res.inst_3 Bool)
-(declare-primed-var top.res.inst_2 Bool)
-(declare-primed-var top.res.inst_1 Bool)
-(declare-primed-var top.res.inst_0 Bool)
 
 (define-fun
   init (
@@ -392,11 +372,11 @@
   ) Bool
 
   (let
-   ((X1 Int top.res.abs_3))
+   ((X1 top.res.abs_3))
    (and
     (= top.res.abs_10 (and top.res.abs_9 (< X1 32767)))
     (let
-     ((X2 Bool top.res.abs_11))
+     ((X2 top.res.abs_11))
      (and
       (= top.usr.OK (=> X2 (>= X1 0)))
       (__node_init_voiture_0
@@ -472,11 +452,11 @@
   ) Bool
 
   (let
-   ((X1 Int top.res.abs_3!))
+   ((X1 top.res.abs_3!))
    (and
     (= top.res.abs_10! (and top.res.abs_9! (< X1 32767)))
     (let
-     ((X2 Bool top.res.abs_11!))
+     ((X2 top.res.abs_11!))
      (and
       (= top.usr.OK! (=> X2 (>= X1 0)))
       (__node_trans_voiture_0
diff --git a/test/regress/regress1/sygus/univ_2-long-repeat.sy b/test/regress/regress1/sygus/univ_2-long-repeat.sy
index ac9493b2d..a2c4c028d 100644
--- a/test/regress/regress1/sygus/univ_2-long-repeat.sy
+++ b/test/regress/regress1/sygus/univ_2-long-repeat.sy
@@ -1,89 +1,89 @@
 ; EXPECT: unsat

-; COMMAND-LINE: --sygus-fair=direct --sygus-out=status

+; COMMAND-LINE: --lang=sygus2 --sygus-fair=direct --sygus-out=status

 (set-logic SLIA)

- 

+

 (synth-fun f ((col1 String) (col2 String)) String

-    ((Start String (ntString))

-     (ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY"

+    ((ntString String) (ntInt Int) (ntBool Bool))

+    ((ntString String (col1 col2 " " "," "USA" "PA" "CT" "CA" "MD" "NY"

                        (str.++ ntString ntString)

                        (str.replace ntString ntString ntString)

                        (str.at ntString ntInt)

-                       (int.to.str ntInt)

+                       (str.from_int ntInt)

                        (ite ntBool ntString ntString)

                        (str.substr ntString ntInt ntInt)))

       (ntInt Int (0 1 2

                   (+ ntInt ntInt)

                   (- ntInt ntInt)

                   (str.len ntString)

-                  (str.to.int ntString)

+                  (str.to_int ntString)

                   (str.indexof ntString ntString ntInt)))

       (ntBool Bool (true false

                     (str.prefixof ntString ntString)

                     (str.suffixof ntString ntString)

                     (str.contains ntString ntString)))))

 

-

 (declare-var col1 String)

 (declare-var col2 String)

-(constraint (= (f "UC Berkeley" "Berkeley, CA") 

+

+(constraint (= (f "UC Berkeley" "Berkeley, CA")

                   "UC Berkeley, Berkeley, CA, USA"))

-(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") 

+(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA")

                   "University of Pennsylvania, Phialdelphia, PA, USA"))

-(constraint (= (f "UCLA" "Los Angeles, CA") 

+(constraint (= (f "UCLA" "Los Angeles, CA")

                     "UCLA, Los Angeles, CA, USA"))

-(constraint (= (f "Cornell University" "Ithaca, New York, USA") 

+(constraint (= (f "Cornell University" "Ithaca, New York, USA")

                   "Cornell University, Ithaca, New York, USA"))

-(constraint (= (f "Penn" "Philadelphia, PA, USA") 

+(constraint (= (f "Penn" "Philadelphia, PA, USA")

                   "Penn, Philadelphia, PA, USA"))

-(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA") 

+(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA")

                   "University of Michigan, Ann Arbor, MI, USA"))

-(constraint (= (f "UC Berkeley" "Berkeley, CA") 

+(constraint (= (f "UC Berkeley" "Berkeley, CA")

                   "UC Berkeley, Berkeley, CA, USA"))

-(constraint (= (f "MIT" "Cambridge, MA") 

+(constraint (= (f "MIT" "Cambridge, MA")

                   "MIT, Cambridge, MA, USA"))

-(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA") 

+(constraint (= (f "University of Pennsylvania" "Phialdelphia, PA, USA")

                   "University of Pennsylvania, Phialdelphia, PA, USA"))

-(constraint (= (f "UCLA" "Los Angeles, CA") 

-                    "UCLA, Los Angeles, CA, USA"))                  

-(constraint (= (f "University of Maryland College Park" "College Park, MD")   

+(constraint (= (f "UCLA" "Los Angeles, CA")

+                    "UCLA, Los Angeles, CA, USA"))

+(constraint (= (f "University of Maryland College Park" "College Park, MD")

                   "University of Maryland College Park, College Park, MD, USA"))

-(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA") 

+(constraint (= (f "University of Michigan" "Ann Arbor, MI, USA")

                   "University of Michigan, Ann Arbor, MI, USA"))

-(constraint (= (f "UC Berkeley" "Berkeley, CA") 

+(constraint (= (f "UC Berkeley" "Berkeley, CA")

                   "UC Berkeley, Berkeley, CA, USA"))

-(constraint (= (f "MIT" "Cambridge, MA") 

+(constraint (= (f "MIT" "Cambridge, MA")

                   "MIT, Cambridge, MA, USA"))

-(constraint (= (f "Rice University" "Houston, TX") 

+(constraint (= (f "Rice University" "Houston, TX")

                   "Rice University, Houston, TX, USA"))

-(constraint (= (f "Yale University" "New Haven, CT, USA") 

+(constraint (= (f "Yale University" "New Haven, CT, USA")

                   "Yale University, New Haven, CT, USA"))

-(constraint (= (f "Columbia University" "New York, NY, USA") 

+(constraint (= (f "Columbia University" "New York, NY, USA")

                   "Columbia University, New York, NY, USA"))

-(constraint (= (f "NYU" "New York, New York, USA") 

+(constraint (= (f "NYU" "New York, New York, USA")

                   "NYU, New York, New York, USA"))

-(constraint (= (f "Drexel University" "Philadelphia, PA") 

-                  "Drexel University, Philadelphia, PA, USA"))                  

-(constraint (= (f "UC Berkeley" "Berkeley, CA") 

+(constraint (= (f "Drexel University" "Philadelphia, PA")

+                  "Drexel University, Philadelphia, PA, USA"))

+(constraint (= (f "UC Berkeley" "Berkeley, CA")

                   "UC Berkeley, Berkeley, CA, USA"))

-(constraint (= (f "UIUC" "Urbana, IL") 

+(constraint (= (f "UIUC" "Urbana, IL")

                   "UIUC, Urbana, IL, USA"))

-(constraint (= (f "Temple University" "Philadelphia, PA") 

+(constraint (= (f "Temple University" "Philadelphia, PA")

                   "Temple University, Philadelphia, PA, USA"))

-(constraint (= (f "Harvard University" "Cambridge, MA, USA") 

+(constraint (= (f "Harvard University" "Cambridge, MA, USA")

                   "Harvard University, Cambridge, MA, USA"))

-(constraint (= (f "University of Connecticut" "Storrs, CT, USA") 

+(constraint (= (f "University of Connecticut" "Storrs, CT, USA")

                   "University of Connecticut, Storrs, CT, USA"))

-(constraint (= (f "Drexel University" "Philadelphia, PA") 

+(constraint (= (f "Drexel University" "Philadelphia, PA")

                   "Drexel University, Philadelphia, PA, USA"))

-(constraint (= (f "NYU" "New York, New York, USA") 

-                  "NYU, New York, New York, USA"))  

-(constraint (= (f "UIUC" "Urbana, IL") 

-                  "UIUC, Urbana, IL, USA"))                                  

-(constraint (= (f "New Haven University" "New Haven, CT, USA") 

+(constraint (= (f "NYU" "New York, New York, USA")

+                  "NYU, New York, New York, USA"))

+(constraint (= (f "UIUC" "Urbana, IL")

+                  "UIUC, Urbana, IL, USA"))

+(constraint (= (f "New Haven University" "New Haven, CT, USA")

                   "New Haven University, New Haven, CT, USA"))

-(constraint (= (f "University of California, Santa Barbara" "Santa Barbara, CA, USA") 

+(constraint (= (f "University of California, Santa Barbara" "Santa Barbara, CA, USA")

                   "University of California, Santa Barbara, Santa Barbara, CA, USA"))

-(constraint (= (f "University of Connecticut" "Storrs, CT, USA") 

-                  "University of Connecticut, Storrs, CT, USA"))                  

- 

+(constraint (= (f "University of Connecticut" "Storrs, CT, USA")

+                  "University of Connecticut, Storrs, CT, USA"))

+

 (check-synth)