6 files changed, 21 insertions, 15 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)))
 ))