update golds/tests

LeventErkok · Dec 3, 2024 · f99c05c · f99c05c
1 parent 016c6f1
commit f99c05c
Show file tree

Hide file tree

Showing 32 changed files with 181 additions and 145 deletions.
diff --git a/SBVTestSuite/GoldFiles/lambda04.gold b/SBVTestSuite/GoldFiles/lambda04.gold
@@ -20,17 +20,18 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
-[GOOD] ; --- SBV Function definitions
-[GOOD] (define-fun-rec |sbv.map_@((SInteger,_SBool))_(lambda_((l1_s0_Int))_false)| ((lst (Seq Int))) (Seq Bool)
+[GOOD] ; --- Firstified function definitions
+[GOOD] ; Firstified function: map :: (SInteger -> SBool) -> [SInteger] -> [SBool]
+[GOOD] (define-fun-rec sbv.map_db28ce ((lst (Seq Int))) (Seq Bool)
                      (ite (= lst (as seq.empty (Seq Int)))
                           (as seq.empty (Seq Bool))
                           (seq.++ (seq.unit (select (lambda ((l1_s0 Int))
                                  false) (seq.nth lst 0)))
-                                  (|sbv.map_@((SInteger,_SBool))_(lambda_((l1_s0_Int))_false)| (seq.extract lst 1 (- (seq.len lst) 1))))))
+                                  (sbv.map_db28ce (seq.extract lst 1 (- (seq.len lst) 1))))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s3 () Bool (= s0 s2))
-[GOOD] (define-fun s4 () (Seq Bool) (|sbv.map_@((SInteger,_SBool))_(lambda_((l1_s0_Int))_false)| s0))
+[GOOD] (define-fun s4 () (Seq Bool) (sbv.map_db28ce s0))
 [GOOD] (define-fun s5 () Bool (= s1 s4))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---

diff --git a/SBVTestSuite/GoldFiles/lambda05.gold b/SBVTestSuite/GoldFiles/lambda05.gold
@@ -20,28 +20,30 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
-[GOOD] ; --- SBV Function definitions
-[GOOD] (define-fun-rec |sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| ((lst (Seq Int))) (Seq Int)
+[GOOD] ; --- Firstified function definitions
+[GOOD] ; Firstified function: map :: (SInteger -> SInteger) -> [SInteger] -> [SInteger]
+[GOOD] (define-fun-rec sbv.map_3ed6e9 ((lst (Seq Int))) (Seq Int)
                      (ite (= lst (as seq.empty (Seq Int)))
                           (as seq.empty (Seq Int))
                           (seq.++ (seq.unit (select (lambda ((l1_s0 Int))
                                  (let ((l1_s1 2))
                                  (let ((l1_s2 (+ l1_s0 l1_s1)))
                                  l1_s2))) (seq.nth lst 0)))
-                                  (|sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| (seq.extract lst 1 (- (seq.len lst) 1))))))
-[GOOD] (define-fun-rec |sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_1))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| ((lst (Seq Int))) (Seq Int)
+                                  (sbv.map_3ed6e9 (seq.extract lst 1 (- (seq.len lst) 1))))))
+[GOOD] ; Firstified function: map :: (SInteger -> SInteger) -> [SInteger] -> [SInteger]
+[GOOD] (define-fun-rec sbv.map_1f10ee ((lst (Seq Int))) (Seq Int)
                      (ite (= lst (as seq.empty (Seq Int)))
                           (as seq.empty (Seq Int))
                           (seq.++ (seq.unit (select (lambda ((l1_s0 Int))
                                  (let ((l1_s1 1))
                                  (let ((l1_s2 (+ l1_s0 l1_s1)))
                                  l1_s2))) (seq.nth lst 0)))
-                                  (|sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_1))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| (seq.extract lst 1 (- (seq.len lst) 1))))))
+                                  (sbv.map_1f10ee (seq.extract lst 1 (- (seq.len lst) 1))))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s3 () Bool (= s0 s2))
-[GOOD] (define-fun s4 () (Seq Int) (|sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_2))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| s0))
-[GOOD] (define-fun s5 () (Seq Int) (|sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_1))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| s4))
+[GOOD] (define-fun s4 () (Seq Int) (sbv.map_3ed6e9 s0))
+[GOOD] (define-fun s5 () (Seq Int) (sbv.map_1f10ee s4))
 [GOOD] (define-fun s6 () Bool (= s1 s5))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---

diff --git a/SBVTestSuite/GoldFiles/lambda06.gold b/SBVTestSuite/GoldFiles/lambda06.gold
@@ -20,8 +20,9 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
-[GOOD] ; --- SBV Function definitions
-[GOOD] (define-fun-rec |sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_(*_l1_s0_l1_s0)))_(let_((l1_s2_(+_l1_s0_l1_s1)))_(let_((l1_s3_(*_l1_s0_l1_s1)))_(let_((l1_s4_(+_l1_s2_l1_s3)))_(let_((l1_s5_(*_l1_s1_l1_s1)))_(let_((l1_s6_(+_l1_s4_l1_s5)))_(let_((l1_s7_(*_l1_s0_l1_s5)))_(let_((l1_s8_(+_l1_s6_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s5)))_(let_((l1_s10_(+_l1_s8_l1_s9)))_(let_((l1_s11_(*_l1_s0_l1_s9)))_(let_((l1_s12_(+_l1_s10_l1_s11)))_(let_((l1_s13_(*_l1_s5_l1_s5)))_(let_((l1_s14_(+_l1_s12_l1_s13)))_(let_((l1_s15_(*_l1_s0_l1_s13)))_(let_((l1_s16_(+_l1_s14_l1_s15)))_(let_((l1_s17_(*_l1_s1_l1_s13)))_(let_((l1_s18_(+_l1_s16_l1_s17)))_l1_s18)))))))))))))))))))| ((lst (Seq Int))) (Seq Int)
+[GOOD] ; --- Firstified function definitions
+[GOOD] ; Firstified function: map :: (SInteger -> SInteger) -> [SInteger] -> [SInteger]
+[GOOD] (define-fun-rec sbv.map_8f5bf3 ((lst (Seq Int))) (Seq Int)
                      (ite (= lst (as seq.empty (Seq Int)))
                           (as seq.empty (Seq Int))
                           (seq.++ (seq.unit (select (lambda ((l1_s0 Int))
@@ -44,11 +45,11 @@
                                  (let ((l1_s17 (* l1_s1 l1_s13)))
                                  (let ((l1_s18 (+ l1_s16 l1_s17)))
                                  l1_s18))))))))))))))))))) (seq.nth lst 0)))
-                                  (|sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_(*_l1_s0_l1_s0)))_(let_((l1_s2_(+_l1_s0_l1_s1)))_(let_((l1_s3_(*_l1_s0_l1_s1)))_(let_((l1_s4_(+_l1_s2_l1_s3)))_(let_((l1_s5_(*_l1_s1_l1_s1)))_(let_((l1_s6_(+_l1_s4_l1_s5)))_(let_((l1_s7_(*_l1_s0_l1_s5)))_(let_((l1_s8_(+_l1_s6_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s5)))_(let_((l1_s10_(+_l1_s8_l1_s9)))_(let_((l1_s11_(*_l1_s0_l1_s9)))_(let_((l1_s12_(+_l1_s10_l1_s11)))_(let_((l1_s13_(*_l1_s5_l1_s5)))_(let_((l1_s14_(+_l1_s12_l1_s13)))_(let_((l1_s15_(*_l1_s0_l1_s13)))_(let_((l1_s16_(+_l1_s14_l1_s15)))_(let_((l1_s17_(*_l1_s1_l1_s13)))_(let_((l1_s18_(+_l1_s16_l1_s17)))_l1_s18)))))))))))))))))))| (seq.extract lst 1 (- (seq.len lst) 1))))))
+                                  (sbv.map_8f5bf3 (seq.extract lst 1 (- (seq.len lst) 1))))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s3 () Bool (= s0 s2))
-[GOOD] (define-fun s4 () (Seq Int) (|sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_(*_l1_s0_l1_s0)))_(let_((l1_s2_(+_l1_s0_l1_s1)))_(let_((l1_s3_(*_l1_s0_l1_s1)))_(let_((l1_s4_(+_l1_s2_l1_s3)))_(let_((l1_s5_(*_l1_s1_l1_s1)))_(let_((l1_s6_(+_l1_s4_l1_s5)))_(let_((l1_s7_(*_l1_s0_l1_s5)))_(let_((l1_s8_(+_l1_s6_l1_s7)))_(let_((l1_s9_(*_l1_s1_l1_s5)))_(let_((l1_s10_(+_l1_s8_l1_s9)))_(let_((l1_s11_(*_l1_s0_l1_s9)))_(let_((l1_s12_(+_l1_s10_l1_s11)))_(let_((l1_s13_(*_l1_s5_l1_s5)))_(let_((l1_s14_(+_l1_s12_l1_s13)))_(let_((l1_s15_(*_l1_s0_l1_s13)))_(let_((l1_s16_(+_l1_s14_l1_s15)))_(let_((l1_s17_(*_l1_s1_l1_s13)))_(let_((l1_s18_(+_l1_s16_l1_s17)))_l1_s18)))))))))))))))))))| s0))
+[GOOD] (define-fun s4 () (Seq Int) (sbv.map_8f5bf3 s0))
 [GOOD] (define-fun s5 () Bool (= s1 s4))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---

diff --git a/SBVTestSuite/GoldFiles/lambda07.gold b/SBVTestSuite/GoldFiles/lambda07.gold
@@ -21,30 +21,33 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
-[GOOD] ; --- SBV Function definitions
-[GOOD] (define-fun-rec |sbv.foldl_@((SInteger,_SInteger))_(lambda_((l2_s0_Int)_(l2_s1_Int))_(+_l2_s0_l2_s1))| ((base Int) (lst (Seq Int))) Int
+[GOOD] ; --- Firstified function definitions
+[GOOD] ; Firstified function: foldl :: (SInteger -> SInteger -> SInteger) -> SInteger -> [SInteger] -> SInteger
+[GOOD] (define-fun-rec sbv.foldl_3d10f5 ((base Int) (lst (Seq Int))) Int
                        (ite (= lst (as seq.empty (Seq Int)))
                             base
-                            (|sbv.foldl_@((SInteger,_SInteger))_(lambda_((l2_s0_Int)_(l2_s1_Int))_(+_l2_s0_l2_s1))| (select (lambda ((l2_s0 Int) (l2_s1 Int))
+                            (sbv.foldl_3d10f5 (select (lambda ((l2_s0 Int) (l2_s1 Int))
          (+ l2_s0 l2_s1)) base (seq.nth lst 0)) (seq.extract lst 1 (- (seq.len lst) 1)))))
-[GOOD] (define-fun-rec |sbv.map_@(([SInteger],_SInteger))_(lambda_((l1_s0_(Seq_Int)))_(let_((l1_s1_0))_(let_((l1_s2_(_sbv.foldl_@((SInteger,_SInteger))_(lambda_((l2_s0_Int)_(l2_s1_Int))_(+_l2_s0_l2_s1))__l1_s1_l1_s0)))_l1_s2)))| ((lst (Seq (Seq Int)))) (Seq Int)
+[GOOD] ; Firstified function: map :: ([SInteger] -> SInteger) -> [[SInteger]] -> [SInteger]
+[GOOD] (define-fun-rec sbv.map_698291 ((lst (Seq (Seq Int)))) (Seq Int)
                      (ite (= lst (as seq.empty (Seq (Seq Int))))
                           (as seq.empty (Seq Int))
                           (seq.++ (seq.unit (select (lambda ((l1_s0 (Seq Int)))
                                  (let ((l1_s1 0))
-                                 (let ((l1_s2 (|sbv.foldl_@((SInteger,_SInteger))_(lambda_((l2_s0_Int)_(l2_s1_Int))_(+_l2_s0_l2_s1))| l1_s1 l1_s0)))
+                                 (let ((l1_s2 (sbv.foldl_3d10f5 l1_s1 l1_s0)))
                                  l1_s2))) (seq.nth lst 0)))
-                                  (|sbv.map_@(([SInteger],_SInteger))_(lambda_((l1_s0_(Seq_Int)))_(let_((l1_s1_0))_(let_((l1_s2_(_sbv.foldl_@((SInteger,_SInteger))_(lambda_((l2_s0_Int)_(l2_s1_Int))_(+_l2_s0_l2_s1))__l1_s1_l1_s0)))_l1_s2)))| (seq.extract lst 1 (- (seq.len lst) 1))))))
-[GOOD] (define-fun-rec |sbv.foldl_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| ((base Int) (lst (Seq Int))) Int
+                                  (sbv.map_698291 (seq.extract lst 1 (- (seq.len lst) 1))))))
+[GOOD] ; Firstified function: foldl :: (SInteger -> SInteger -> SInteger) -> SInteger -> [SInteger] -> SInteger
+[GOOD] (define-fun-rec sbv.foldl_929914 ((base Int) (lst (Seq Int))) Int
                        (ite (= lst (as seq.empty (Seq Int)))
                             base
-                            (|sbv.foldl_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| (select (lambda ((l1_s0 Int) (l1_s1 Int))
+                            (sbv.foldl_929914 (select (lambda ((l1_s0 Int) (l1_s1 Int))
          (+ l1_s0 l1_s1)) base (seq.nth lst 0)) (seq.extract lst 1 (- (seq.len lst) 1)))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s3 () Bool (= s0 s2))
-[GOOD] (define-fun s5 () (Seq Int) (|sbv.map_@(([SInteger],_SInteger))_(lambda_((l1_s0_(Seq_Int)))_(let_((l1_s1_0))_(let_((l1_s2_(_sbv.foldl_@((SInteger,_SInteger))_(lambda_((l2_s0_Int)_(l2_s1_Int))_(+_l2_s0_l2_s1))__l1_s1_l1_s0)))_l1_s2)))| s0))
-[GOOD] (define-fun s6 () Int (|sbv.foldl_@((SInteger,_SInteger))_(lambda_((l1_s0_Int)_(l1_s1_Int))_(+_l1_s0_l1_s1))| s4 s5))
+[GOOD] (define-fun s5 () (Seq Int) (sbv.map_698291 s0))
+[GOOD] (define-fun s6 () Int (sbv.foldl_929914 s4 s5))
 [GOOD] (define-fun s7 () Bool (= s1 s6))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---

diff --git a/SBVTestSuite/GoldFiles/lambda08.gold b/SBVTestSuite/GoldFiles/lambda08.gold
@@ -20,19 +20,20 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
-[GOOD] ; --- SBV Function definitions
-[GOOD] (define-fun-rec |sbv.map_@((SFloat,_SFloat))_(lambda_((l1_s0_(__FloatingPoint_8_24)))_(let_((l1_s1_((__to_fp_8_24)_roundNearestTiesToEven_(/_1.0_1.0))))_(let_((l1_s2_(fp.add_roundNearestTiesToEven_l1_s0_l1_s1)))_l1_s2)))| ((lst (Seq (_ FloatingPoint  8 24)))) (Seq (_ FloatingPoint  8 24))
+[GOOD] ; --- Firstified function definitions
+[GOOD] ; Firstified function: map :: (SFloat -> SFloat) -> [SFloat] -> [SFloat]
+[GOOD] (define-fun-rec sbv.map_172e96 ((lst (Seq (_ FloatingPoint  8 24)))) (Seq (_ FloatingPoint  8 24))
                      (ite (= lst (as seq.empty (Seq (_ FloatingPoint  8 24))))
                           (as seq.empty (Seq (_ FloatingPoint  8 24)))
                           (seq.++ (seq.unit (select (lambda ((l1_s0 (_ FloatingPoint  8 24)))
                                  (let ((l1_s1 ((_ to_fp 8 24) roundNearestTiesToEven (/ 1.0 1.0))))
                                  (let ((l1_s2 (fp.add roundNearestTiesToEven l1_s0 l1_s1)))
                                  l1_s2))) (seq.nth lst 0)))
-                                  (|sbv.map_@((SFloat,_SFloat))_(lambda_((l1_s0_(__FloatingPoint_8_24)))_(let_((l1_s1_((__to_fp_8_24)_roundNearestTiesToEven_(/_1.0_1.0))))_(let_((l1_s2_(fp.add_roundNearestTiesToEven_l1_s0_l1_s1)))_l1_s2)))| (seq.extract lst 1 (- (seq.len lst) 1))))))
+                                  (sbv.map_172e96 (seq.extract lst 1 (- (seq.len lst) 1))))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s3 () Bool (= s0 s2))
-[GOOD] (define-fun s4 () (Seq (_ FloatingPoint  8 24)) (|sbv.map_@((SFloat,_SFloat))_(lambda_((l1_s0_(__FloatingPoint_8_24)))_(let_((l1_s1_((__to_fp_8_24)_roundNearestTiesToEven_(/_1.0_1.0))))_(let_((l1_s2_(fp.add_roundNearestTiesToEven_l1_s0_l1_s1)))_l1_s2)))| s0))
+[GOOD] (define-fun s4 () (Seq (_ FloatingPoint  8 24)) (sbv.map_172e96 s0))
 [GOOD] (define-fun s5 () Bool (= s1 s4))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---

diff --git a/SBVTestSuite/GoldFiles/lambda09.gold b/SBVTestSuite/GoldFiles/lambda09.gold
@@ -20,19 +20,20 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
-[GOOD] ; --- SBV Function definitions
-[GOOD] (define-fun-rec |sbv.map_@((SInt8,_SInt8))_(lambda_((l1_s0_(__BitVec_8)))_(let_((l1_s1_#x01))_(let_((l1_s2_(bvadd_l1_s0_l1_s1)))_l1_s2)))| ((lst (Seq (_ BitVec 8)))) (Seq (_ BitVec 8))
+[GOOD] ; --- Firstified function definitions
+[GOOD] ; Firstified function: map :: (SInt8 -> SInt8) -> [SInt8] -> [SInt8]
+[GOOD] (define-fun-rec sbv.map_f39867 ((lst (Seq (_ BitVec 8)))) (Seq (_ BitVec 8))
                      (ite (= lst (as seq.empty (Seq (_ BitVec 8))))
                           (as seq.empty (Seq (_ BitVec 8)))
                           (seq.++ (seq.unit (select (lambda ((l1_s0 (_ BitVec 8)))
                                  (let ((l1_s1 #x01))
                                  (let ((l1_s2 (bvadd l1_s0 l1_s1)))
                                  l1_s2))) (seq.nth lst 0)))
-                                  (|sbv.map_@((SInt8,_SInt8))_(lambda_((l1_s0_(__BitVec_8)))_(let_((l1_s1_#x01))_(let_((l1_s2_(bvadd_l1_s0_l1_s1)))_l1_s2)))| (seq.extract lst 1 (- (seq.len lst) 1))))))
+                                  (sbv.map_f39867 (seq.extract lst 1 (- (seq.len lst) 1))))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s3 () Bool (= s0 s2))
-[GOOD] (define-fun s4 () (Seq (_ BitVec 8)) (|sbv.map_@((SInt8,_SInt8))_(lambda_((l1_s0_(__BitVec_8)))_(let_((l1_s1_#x01))_(let_((l1_s2_(bvadd_l1_s0_l1_s1)))_l1_s2)))| s0))
+[GOOD] (define-fun s4 () (Seq (_ BitVec 8)) (sbv.map_f39867 s0))
 [GOOD] (define-fun s5 () Bool (= s1 s4))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---

diff --git a/SBVTestSuite/GoldFiles/lambda10.gold b/SBVTestSuite/GoldFiles/lambda10.gold
@@ -20,19 +20,20 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
-[GOOD] ; --- SBV Function definitions
-[GOOD] (define-fun-rec |sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_1))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| ((lst (Seq Int))) (Seq Int)
+[GOOD] ; --- Firstified function definitions
+[GOOD] ; Firstified function: map :: (SInteger -> SInteger) -> [SInteger] -> [SInteger]
+[GOOD] (define-fun-rec sbv.map_1f10ee ((lst (Seq Int))) (Seq Int)
                      (ite (= lst (as seq.empty (Seq Int)))
                           (as seq.empty (Seq Int))
                           (seq.++ (seq.unit (select (lambda ((l1_s0 Int))
                                  (let ((l1_s1 1))
                                  (let ((l1_s2 (+ l1_s0 l1_s1)))
                                  l1_s2))) (seq.nth lst 0)))
-                                  (|sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_1))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| (seq.extract lst 1 (- (seq.len lst) 1))))))
+                                  (sbv.map_1f10ee (seq.extract lst 1 (- (seq.len lst) 1))))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s3 () Bool (= s0 s2))
-[GOOD] (define-fun s4 () (Seq Int) (|sbv.map_@((SInteger,_SInteger))_(lambda_((l1_s0_Int))_(let_((l1_s1_1))_(let_((l1_s2_(+_l1_s0_l1_s1)))_l1_s2)))| s0))
+[GOOD] (define-fun s4 () (Seq Int) (sbv.map_1f10ee s0))
 [GOOD] (define-fun s5 () Bool (= s1 s4))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---

diff --git a/SBVTestSuite/GoldFiles/lambda11.gold b/SBVTestSuite/GoldFiles/lambda11.gold
@@ -20,19 +20,20 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
-[GOOD] ; --- SBV Function definitions
-[GOOD] (define-fun-rec |sbv.map_@((SWord8,_SWord8))_(lambda_((l1_s0_(__BitVec_8)))_(let_((l1_s1_#x01))_(let_((l1_s2_(bvadd_l1_s0_l1_s1)))_l1_s2)))| ((lst (Seq (_ BitVec 8)))) (Seq (_ BitVec 8))
+[GOOD] ; --- Firstified function definitions
+[GOOD] ; Firstified function: map :: (SWord8 -> SWord8) -> [SWord8] -> [SWord8]
+[GOOD] (define-fun-rec sbv.map_ea1537 ((lst (Seq (_ BitVec 8)))) (Seq (_ BitVec 8))
                      (ite (= lst (as seq.empty (Seq (_ BitVec 8))))
                           (as seq.empty (Seq (_ BitVec 8)))
                           (seq.++ (seq.unit (select (lambda ((l1_s0 (_ BitVec 8)))
                                  (let ((l1_s1 #x01))
                                  (let ((l1_s2 (bvadd l1_s0 l1_s1)))
                                  l1_s2))) (seq.nth lst 0)))
-                                  (|sbv.map_@((SWord8,_SWord8))_(lambda_((l1_s0_(__BitVec_8)))_(let_((l1_s1_#x01))_(let_((l1_s2_(bvadd_l1_s0_l1_s1)))_l1_s2)))| (seq.extract lst 1 (- (seq.len lst) 1))))))
+                                  (sbv.map_ea1537 (seq.extract lst 1 (- (seq.len lst) 1))))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s3 () Bool (= s0 s2))
-[GOOD] (define-fun s4 () (Seq (_ BitVec 8)) (|sbv.map_@((SWord8,_SWord8))_(lambda_((l1_s0_(__BitVec_8)))_(let_((l1_s1_#x01))_(let_((l1_s2_(bvadd_l1_s0_l1_s1)))_l1_s2)))| s0))
+[GOOD] (define-fun s4 () (Seq (_ BitVec 8)) (sbv.map_ea1537 s0))
 [GOOD] (define-fun s5 () Bool (= s1 s4))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---

diff --git a/SBVTestSuite/GoldFiles/lambda12.gold b/SBVTestSuite/GoldFiles/lambda12.gold
@@ -20,17 +20,18 @@
 [GOOD] ; --- constant tables ---
 [GOOD] ; --- non-constant tables ---
 [GOOD] ; --- uninterpreted constants ---
-[GOOD] ; --- SBV Function definitions
-[GOOD] (define-fun-rec |sbv.map_@((SInteger,_[SInteger]))_(lambda_((l1_s0_Int))_(seq.unit_l1_s0))| ((lst (Seq Int))) (Seq (Seq Int))
+[GOOD] ; --- Firstified function definitions
+[GOOD] ; Firstified function: map :: (SInteger -> [SInteger]) -> [SInteger] -> [[SInteger]]
+[GOOD] (define-fun-rec sbv.map_135533 ((lst (Seq Int))) (Seq (Seq Int))
                      (ite (= lst (as seq.empty (Seq Int)))
                           (as seq.empty (Seq (Seq Int)))
                           (seq.++ (seq.unit (select (lambda ((l1_s0 Int))
          (seq.unit l1_s0)) (seq.nth lst 0)))
-                                  (|sbv.map_@((SInteger,_[SInteger]))_(lambda_((l1_s0_Int))_(seq.unit_l1_s0))| (seq.extract lst 1 (- (seq.len lst) 1))))))
+                                  (sbv.map_135533 (seq.extract lst 1 (- (seq.len lst) 1))))))
 [GOOD] ; --- user defined functions ---
 [GOOD] ; --- assignments ---
 [GOOD] (define-fun s3 () Bool (= s0 s2))
-[GOOD] (define-fun s4 () (Seq (Seq Int)) (|sbv.map_@((SInteger,_[SInteger]))_(lambda_((l1_s0_Int))_(seq.unit_l1_s0))| s0))
+[GOOD] (define-fun s4 () (Seq (Seq Int)) (sbv.map_135533 s0))
 [GOOD] (define-fun s5 () Bool (= s1 s4))
 [GOOD] ; --- delayedEqualities ---
 [GOOD] ; --- formula ---