(assert (ite (_ bv0 1)(_ bv0 1)(_ bv0 1)(_ bv0 1)(_ bv0 1)(_ bv0 1)(_ bv0 1))