; Automatically generated by SBV. Do not modify!
; foo :: SInteger -> SWord32
(define-fun foo ((l1_s0 Int)) (_ BitVec 32)
  (let ((l1_s1 #x00000001))
  (let ((l1_s2 #x00000002))
  (let ((l1_s3 #x00000003))
  (let ((l1_s4 #x00000000))
  (let ((table0 (lambda ((idx Int)) (ite (= idx 0) l1_s1 (ite (= idx 1) l1_s2 l1_s3)))))
  (let ((l1_s5 (ite (or (< l1_s0 0) (<= 3 l1_s0)) l1_s4 (table0 l1_s0))))
  l1_s5)))))))