lambda80.gold

; Automatically generated by SBV. Do not modify!
; |foo @(SBV Integer -> SBV Integer)| :: SInteger -> SInteger
(define-fun |foo @(SBV Integer -> SBV Integer)| ((l1_s0 Int)) Int
                          (let ((l1_s1 1))
                          (let ((l1_s3 2))
                          (let ((l1_s5 3))
                          (let ((l1_s7 0))
                          (let ((l1_s2 (+ l1_s0 l1_s1)))
                          (let ((l1_s4 (+ l1_s0 l1_s3)))
                          (let ((l1_s6 (+ l1_s0 l1_s5)))
                          (let ((table0 (lambda ((idx Int)) (ite (= idx 0) l1_s2 (ite (= idx 1) l1_s4 l1_s6)))))
                          (let ((l1_s8 (ite (or (< l1_s0 0) (<= 3 l1_s0)) l1_s7 (table0 l1_s0))))
                          l1_s8))))))))))