offending pos id is missing for error VerificationError { full_id: "call.precondition:insufficient.permission", pos_id: None, offending_pos_id: None, reason_pos_id: None, message: "The precondition of method make_concrete_String might not hold. There might be insufficient permission to access p_Param(get_s_Ref_mutable_s_Ref_mutable_0(p_Ref_mutable_snap(_7p, s_String_type())), s_String_type()) (<no position>)\n", counterexample: None }

Database: prusti-20260426-174735-3d9ad6e85.db

1 file(s) affected