(assert (=> true (_ bv1 2)))