(assert (ite (_ bv0 1)))