(assert (not (_ bv0 2)))