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