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