(assert (distinct (_ bv0 1))