(assert (or (_ bv0 2) (_ bv1 1)))