1 files changed, 48 insertions, 43 deletions
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)