(assert (=> (_ bv0 1) (_ bv1 2)))