(set-logic QF_AUFBV)
(declare-fun a1 () (Array (_ BitVec 1) (_ BitVec 1)))
(define-fun $e2 () (_ BitVec 1) (_ bv0 1))
(define-fun $e3 () (_ BitVec 1) (select a1 (bvnot $e2)))
(define-fun $e4 () (_ BitVec 1) (select a1 $e2))
(assert (not (= $e3 #b0)))
(assert (not (= (bvnot $e4) #b0)))
(check-sat)
(exit)