Function spec_slice_update Copy item path

pub uninterp fn spec_slice_update<T>(slice: &[T], i: int, t: T) -> &[T]