sbv-14.4: SBVTestSuite/GoldFiles/lambda71.gold

; Automatically generated by SBV. Do not modify!
; |bar @(SBV Integer -> SBV Integer)| :: SInteger -> SInteger [Recursive]
(define-fun-rec |bar @(SBV Integer -> SBV Integer)| ((l2_s0 Int)) Int
                                          (let ((l2_s1 1))
                                          (let ((l2_s2 (- l2_s0 l2_s1)))
                                          (let ((l2_s3 (|bar @(SBV Integer -> SBV Integer)| l2_s2)))
                                          l2_s3))))
; |foo @(SBV Integer -> SBV Integer)| :: SInteger -> SInteger [Refers to: |bar @(SBV Integer -> SBV Integer)|]
(define-fun |foo @(SBV Integer -> SBV Integer)| ((l1_s0 Int)) Int
                          (let ((l1_s1 1))
                          (let ((l1_s2 (- l1_s0 l1_s1)))
                          (let ((l1_s3 (|bar @(SBV Integer -> SBV Integer)| l1_s2)))
                          l1_s3))))