(assert (ite (_ bv0 2) (_ bv0 2) (_ bv0 2)))