(set-logic QF_AUFBV)
(declare-fun a0 () (Array (_ BitVec 32) (_ BitVec 32)))
(define-fun f0 ((p0 (_ BitVec 32)) (x0 (_ BitVec 32))) (_ BitVec 32) (select a0 (bvadd p0 x0)))
(define-fun g0 ((p0 (_ BitVec 32))) (_ BitVec 32) (_ bv0 32))
(define-fun l1 ((p1 (_ BitVec 32))) (_ BitVec 32) (_ bv0 32))
(define-fun l0 ((p0 (_ BitVec 32))) (_ BitVec 32) (f0 (_ bv0 32) (l1 (g0 p0))))
(assert (= ((_ extract 0 0) (l0 (_ bv0 32))) (_ bv1 1)))
(check-sat)
(exit)