(assert ((_ extract 1 1) (_ bv0 1))