(declare-fun c () (Array (_ BitVec 32) Float32)) (declare-fun ~ () (Array (_ BitVec 32) Float32)) (assert true) (push 1) (assert (= ~ c)) (set-info :status sat) (check-sat) (pop 1) (assert (= ~ (store c (_ bv0 32) (fp (_ bv0 1) (_ bv0 8) (_ bv0 23))))) (set-info :status sat) (check-sat)