expected opaque (was TyData { data: TyUsePureRef { snapshot: s_Slice, args: GArgsTy { ty_args: [s_Int_i32_type()], const_args: [] }, ty_pure_ref: TyPureRef { domain: DomainIdn { idn: ViperIdent("s_Slice"), params: 0, _p: PhantomData<vir::type::Snap> }, unreachable_to_snap: FunctionIdn { idn: ViperIdent("s_Slice_unreachable"), args: ([Type], []), result_ty: s_Slice, debug_info: DebugInfo(PhantomData<&()>) } } }, specifics: Array(ArrayData { data: TyUsePureArrayData { caster: Casters(Casters { cast: GArgCasters { make_generic: FunctionIdn { idn: ViperIdent("make_generic_s_Int_i32"), args: (s_Int_i32, [], []), result_ty: s_Param, debug_info: DebugInfo(PhantomData<&()>) }, make_concrete: FunctionIdn { idn: ViperIdent("make_concrete_s_Int_i32"), args: (s_Param, [], []), result_ty: s_Int_i32, debug_info: DebugInfo(PhantomData<&()>) } }, ty_args: GArgsTy { ty_args: [], const_args: [] } }), args: GArgsTy { ty_args: [s_Int_i32_type()], const_args: [] }, pure: TyPureArrayData { index_access: FunctionIdn { idn: ViperIdent("s_Slice_index"), args: (s_Slice, Int), result_ty: s_Param, debug_info: DebugInfo(PhantomData<&()>) }, ref_to_index_ref: FunctionIdn { idn: ViperIdent("s_Slice_index_ref"), args: (Ref, Int, [Type], []), result_ty: Ref, debug_info: DebugInfo(PhantomData<&()>) }, len: FunctionIdn { idn: ViperIdent("s_Slice_len"), args: s_Slice, result_ty: Int, debug_info: DebugInfo(PhantomData<&()>) } } }, slice: true }) })

Database: prusti-20260410-212618-bd3a77aef.db

2 file(s) affected