6 files changed, 20 insertions, 18 deletions
diff --git a/test/regress/regress0/sygus/let-ringer.sy b/test/regress/regress0/sygus/let-ringer.sy
index 0fe8dd05e..c02d2b31f 100644
--- a/test/regress/regress0/sygus/let-ringer.sy
+++ b/test/regress/regress0/sygus/let-ringer.sy
@@ -3,12 +3,14 @@
 ; COMMAND-LINE: --cegqi-si=all --sygus-unif --sygus-out=status
 (set-logic LIA)
 (define-fun g ((x Int)) Int (ite (= x 1) 15 19))
+(define-fun letf ((z Int) (w Int) (s Int) (x Int)) Int (+ z (+ x (+ x (+ s (+ 1 (+ (g w) z)))))))
+
 (synth-fun f ((x Int)) Int
     ((Start Int (x
                  0
                  1
                  (- Start Start)
-                 (let ((z Int Start) (w Int Start)) (+ z (+ x (+ x (+ Start (+ 1 (+ (g w) z)))))))))))
+                 (letf Start Start Start x)))))
                  
 (declare-var x Int)
 (constraint (= (f x) (+ (* 4 x) 15)))
diff --git a/test/regress/regress0/sygus/let-simp.sy b/test/regress/regress0/sygus/let-simp.sy
index 6f9d9fff9..7e191e312 100644
--- a/test/regress/regress0/sygus/let-simp.sy
+++ b/test/regress/regress0/sygus/let-simp.sy
@@ -1,12 +1,13 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --cegqi-si=all --sygus-out=status
 (set-logic LIA)
+(define-fun letf ((z Int)) Int (+ z z))
 (synth-fun f ((x Int) (y Int)) Int
     ((Start Int (x
                  y
                  0
                  (- Start Start)
-                 (let ((z Int Start)) (+ z z))))))
+                 (letf Start)))))
 
 (declare-var x Int)
 (declare-var y Int)
diff --git a/test/regress/regress1/sygus/abv.sy b/test/regress/regress1/sygus/abv.sy
index 6ce1a011a..d9a8a019c 100644
--- a/test/regress/regress1/sygus/abv.sy
+++ b/test/regress/regress1/sygus/abv.sy
@@ -30,6 +30,10 @@
 	(select arrIn x)
 )
 
+(define-fun letf ((m MemSort) (v1 AddrSort) (v2 AddrSort)) ValSort
+  (bvadd 
+    (ReadArr v1 m) 
+    (ReadArr v2 m)))
 
 (synth-fun f 
 	; Args
@@ -45,12 +49,8 @@
 		(WriteArr (Variable AddrSort) (Variable ValSort) mem)))
 
 	(Start ValSort (
-		(let 
-			((m MemSort StartArray)) 
-			(bvadd 
-				(ReadArr (Variable AddrSort) m) 
-				(ReadArr (Variable AddrSort) m))))))
-)
+		(letf StartArray (Variable AddrSort) (Variable AddrSort))))
+))
 
 (declare-var a (BitVec 8))
 (declare-var b (BitVec 8))
diff --git a/test/regress/regress1/sygus/let-bug-simp.sy b/test/regress/regress1/sygus/let-bug-simp.sy
index d570d5a21..5c2dccff0 100644
--- a/test/regress/regress1/sygus/let-bug-simp.sy
+++ b/test/regress/regress1/sygus/let-bug-simp.sy
@@ -1,17 +1,15 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --sygus-out=status
 (set-logic LIA)
-
+(define-fun letf ((z Int) (v1 Int) (v2 Int)) Bool  
+  (or 
+    (= v1 z) 
+    (= v2 z)))
 (synth-fun f ((x0 Int) (x1 Int)) Bool
 (
 	(StartInt Int (5))
 
-	(Start Bool (
-		(let 
-			((z Int StartInt)) 
-			(or 
-				(= (Variable Int) z) 
-				(= (Variable Int) z)))))
+	(Start Bool (  (letf StartInt (Variable Int) (Variable Int)) ))
 )
 )
 
diff --git a/test/regress/regress1/sygus/tester.sy b/test/regress/regress1/sygus/tester.sy
index 261666dd4..bf1cd1576 100644
--- a/test/regress/regress1/sygus/tester.sy
+++ b/test/regress/regress1/sygus/tester.sy
@@ -11,7 +11,7 @@
 	(
 		(Start DT (ntDT))
 		(ntDT DT
-			( x1 x2
+			( x1
 				(JSBool ntBool)
 				(A ntInt)
 				(ite ntBool ntDT ntDT)
diff --git a/test/regress/regress1/sygus/twolets2-orig.sy b/test/regress/regress1/sygus/twolets2-orig.sy
index 50f7ad544..a92c0b014 100644
--- a/test/regress/regress1/sygus/twolets2-orig.sy
+++ b/test/regress/regress1/sygus/twolets2-orig.sy
@@ -1,10 +1,11 @@
 ; EXPECT: unsat
 ; COMMAND-LINE: --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 (
-            (let ((y Int CInt) (z Int CInt)) (+ (+ y x) z))
+            (letf x CInt CInt)
             )
      )
      (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))
@@ -14,7 +15,7 @@
 (synth-fun f2 ((x Int)) Int
      (
      (Start Int (x
-            (let ((y Int Start) (z Int CInt)) (+ (+ y x) z))
+            (letf x Start CInt)
             )
      )
      (CInt Int (0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15))