; Automatically generated by SBV. Do not modify! ; baz :: SInteger -> SInteger (define-fun baz ((l1_s0 Int)) Int (let ((l1_s1 1)) (let ((l1_s2 (+ l1_s0 l1_s1))) l1_s2)))