(assert (= (_ bv0 32))