bug: verification error could not be backtranslated (no crash)

Database: prusti-fix-missing-substitution-in-apply-wands-20260515-162448-aaf0046ee.db

500 file(s) affected

File
alloc_borrow_doctest_147.rs
alloc_borrow_doctest_262.rs
alloc_borrow_doctest_295.rs
alloc_borrow_doctest_310.rs
alloc_borrow_doctest_50.rs
alloc_borrow_doctest_70.rs
alloc_boxed_convert_doctest_183.rs
alloc_boxed_convert_doctest_330.rs
alloc_boxed_doctest_332.rs
alloc_boxed_doctest_349.rs
alloc_boxed_doctest_375.rs
alloc_boxed_doctest_428.rs
alloc_boxed_doctest_485.rs
alloc_boxed_doctest_559.rs
alloc_boxed_doctest_684.rs
alloc_boxed_doctest_720.rs
alloc_boxed_doctest_827.rs
alloc_boxed_doctest_868.rs
alloc_boxed_thin_doctest_79.rs
alloc_collections_binary_heap_mod_doctest_1311.rs
alloc_collections_btree_set_doctest_917.rs
alloc_collections_linked_list_doctest_1040.rs
alloc_collections_linked_list_doctest_1921.rs
alloc_collections_linked_list_doctest_834.rs
alloc_collections_linked_list_doctest_856.rs
alloc_collections_linked_list_doctest_908.rs
alloc_collections_linked_list_doctest_928.rs
alloc_collections_vec_deque_mod_doctest_1204.rs
alloc_collections_vec_deque_mod_doctest_1327.rs
alloc_collections_vec_deque_mod_doctest_1930.rs
alloc_collections_vec_deque_mod_doctest_706.rs
alloc_ffi_c_str_doctest_169.rs
alloc_rc_doctest_1024.rs
alloc_rc_doctest_1056.rs
alloc_rc_doctest_1146.rs
alloc_rc_doctest_1195.rs
alloc_rc_doctest_1232.rs
alloc_rc_doctest_1289.rs
alloc_rc_doctest_1521.rs
alloc_rc_doctest_1733.rs
alloc_rc_doctest_1766.rs
alloc_rc_doctest_1859.rs
alloc_rc_doctest_1877.rs
alloc_rc_doctest_1957.rs
alloc_rc_doctest_2353.rs
alloc_rc_doctest_2683.rs
alloc_rc_doctest_2702.rs
alloc_rc_doctest_2721.rs
alloc_rc_doctest_2741.rs
alloc_rc_doctest_2760.rs
alloc_rc_doctest_2780.rs
alloc_rc_doctest_2799.rs
alloc_rc_doctest_2852.rs
alloc_rc_doctest_2937.rs
alloc_rc_doctest_3112.rs
alloc_rc_doctest_3284.rs
alloc_rc_doctest_3707.rs
alloc_rc_doctest_482.rs
alloc_rc_doctest_517.rs
alloc_rc_doctest_575.rs
alloc_rc_doctest_611.rs
alloc_rc_doctest_673.rs
alloc_rc_doctest_716.rs
alloc_rc_doctest_856.rs
alloc_rc_doctest_900.rs
alloc_rc_doctest_91.rs
alloc_rc_doctest_951.rs
alloc_slice_doctest_685.rs
alloc_str_doctest_227.rs
alloc_string_doctest_1037.rs
alloc_string_doctest_121.rs
alloc_string_doctest_148.rs
alloc_string_doctest_1816.rs
alloc_string_doctest_1840.rs
alloc_string_doctest_1954.rs
alloc_string_doctest_2006.rs
alloc_string_doctest_2026.rs
alloc_string_doctest_2058.rs
alloc_string_doctest_214.rs
alloc_string_doctest_2512.rs
alloc_string_doctest_268.rs
alloc_string_doctest_298.rs
alloc_string_doctest_3097.rs
alloc_string_doctest_3206.rs
alloc_string_doctest_3226.rs
alloc_string_doctest_324.rs
alloc_string_doctest_3430.rs
alloc_string_doctest_3494.rs
alloc_string_doctest_466.rs
alloc_string_doctest_973.rs
alloc_sync_doctest_1006.rs
alloc_sync_doctest_1166.rs
alloc_sync_doctest_1199.rs
alloc_sync_doctest_1290.rs
alloc_sync_doctest_1338.rs
alloc_sync_doctest_1376.rs
alloc_sync_doctest_1434.rs
alloc_sync_doctest_1672.rs
alloc_sync_doctest_2277.rs
alloc_sync_doctest_2295.rs
alloc_sync_doctest_2393.rs
alloc_sync_doctest_2435.rs
alloc_sync_doctest_2477.rs
alloc_sync_doctest_2839.rs
alloc_sync_doctest_3010.rs
alloc_sync_doctest_3551.rs
alloc_sync_doctest_3708.rs
alloc_sync_doctest_3727.rs
alloc_sync_doctest_3746.rs
alloc_sync_doctest_3766.rs
alloc_sync_doctest_3785.rs
alloc_sync_doctest_3805.rs
alloc_sync_doctest_3824.rs
alloc_sync_doctest_3877.rs
alloc_sync_doctest_3962.rs
alloc_sync_doctest_4142.rs
alloc_sync_doctest_482.rs
alloc_sync_doctest_518.rs
alloc_sync_doctest_564.rs
alloc_sync_doctest_589.rs
alloc_sync_doctest_625.rs
alloc_sync_doctest_686.rs
alloc_sync_doctest_729.rs
alloc_sync_doctest_878.rs
alloc_sync_doctest_910.rs
alloc_sync_doctest_954.rs
alloc_vec_in_place_collect_doctest_117.rs
alloc_vec_in_place_collect_doctest_128.rs
alloc_vec_in_place_collect_doctest_138.rs
alloc_vec_mod_doctest_1026.rs
alloc_vec_mod_doctest_1146.rs
alloc_vec_mod_doctest_1873.rs
alloc_vec_mod_doctest_489.rs
alloc_vec_mod_doctest_925.rs
core_any_doctest_241.rs
core_array_mod_doctest_237.rs
core_array_mod_doctest_263.rs
core_array_mod_doctest_289.rs
core_array_mod_doctest_312.rs
core_array_mod_doctest_646.rs
core_array_mod_doctest_728.rs
core_array_mod_doctest_806.rs
core_ascii_doctest_50.rs
core_borrow_doctest_118.rs
core_bstr_mod_doctest_54.rs
core_cell_once_doctest_305.rs
core_cell_once_doctest_333.rs
core_char_convert_doctest_109.rs
core_char_convert_doctest_138.rs
core_char_methods_doctest_1046.rs
core_char_methods_doctest_1113.rs
core_char_methods_doctest_436.rs
core_char_methods_doctest_501.rs
core_char_methods_doctest_557.rs
core_cmp_doctest_1197.rs
core_cmp_doctest_1209.rs
core_cmp_doctest_145.rs
core_cmp_doctest_756.rs
core_cmp_doctest_768.rs
core_convert_mod_doctest_265.rs
core_convert_mod_doctest_550.rs
core_error_doctest_123.rs
core_error_doctest_14.rs
core_error_doctest_541.rs
core_error_doctest_58.rs
core_error_doctest_610.rs
core_error_doctest_708.rs
core_error_doctest_796.rs
core_ffi_c_str_doctest_283.rs
core_fmt_builders_doctest_107.rs
core_fmt_builders_doctest_175.rs
core_fmt_builders_doctest_220.rs
core_fmt_builders_doctest_267.rs
core_fmt_builders_doctest_309.rs
core_fmt_builders_doctest_368.rs
core_fmt_builders_doctest_410.rs
core_fmt_builders_doctest_62.rs
core_fmt_mod_doctest_138.rs
core_fmt_mod_doctest_166.rs
core_fmt_mod_doctest_196.rs
core_fmt_mod_doctest_2204.rs
core_fmt_mod_doctest_2371.rs
core_fmt_mod_doctest_680.rs
core_fmt_mod_doctest_788.rs
core_fmt_mod_doctest_912.rs
core_hash_mod_doctest_621.rs
core_hash_mod_doctest_649.rs
core_hint_doctest_703.rs
core_hint_doctest_757.rs
core_intrinsics_mod_doctest_631.rs
core_iter_adapters_array_chunks_doctest_39.rs
core_iter_adapters_chain_doctest_47.rs
core_iter_adapters_fuse_doctest_206.rs
core_iter_adapters_map_doctest_21.rs
core_iter_adapters_peekable_doctest_303.rs
core_iter_adapters_rev_doctest_28.rs
core_iter_adapters_zip_doctest_43.rs
core_iter_mod_doctest_329.rs
core_iter_sources_empty_doctest_10.rs
core_iter_sources_once_doctest_16.rs
core_iter_sources_repeat_doctest_25.rs
core_iter_sources_repeat_doctest_43.rs
core_iter_sources_repeat_n_doctest_19.rs
core_iter_sources_repeat_n_doctest_36.rs
core_iter_traits_collect_doctest_170.rs
core_iter_traits_collect_doctest_181.rs
core_iter_traits_collect_doctest_299.rs
core_iter_traits_collect_doctest_337.rs
core_iter_traits_double_ended_doctest_185.rs
core_iter_traits_exact_size_doctest_135.rs
core_iter_traits_iterator_doctest_1077.rs
core_iter_traits_iterator_doctest_1103.rs
core_iter_traits_iterator_doctest_1141.rs
core_iter_traits_iterator_doctest_1165.rs
core_iter_traits_iterator_doctest_1216.rs
core_iter_traits_iterator_doctest_1231.rs
core_iter_traits_iterator_doctest_1246.rs
core_iter_traits_iterator_doctest_1305.rs
core_iter_traits_iterator_doctest_1335.rs
core_iter_traits_iterator_doctest_1347.rs
core_iter_traits_iterator_doctest_1359.rs
core_iter_traits_iterator_doctest_1412.rs
core_iter_traits_iterator_doctest_1735.rs
core_iter_traits_iterator_doctest_1977.rs
core_iter_traits_iterator_doctest_2367.rs
core_iter_traits_iterator_doctest_2378.rs
core_iter_traits_iterator_doctest_240.rs
core_iter_traits_iterator_doctest_2681.rs
core_iter_traits_iterator_doctest_2739.rs
core_iter_traits_iterator_doctest_2749.rs
core_iter_traits_iterator_doctest_2792.rs
core_iter_traits_iterator_doctest_2802.rs
core_iter_traits_iterator_doctest_281.rs
core_iter_traits_iterator_doctest_2853.rs
core_iter_traits_iterator_doctest_2862.rs
core_iter_traits_iterator_doctest_2950.rs
core_iter_traits_iterator_doctest_3022.rs
core_iter_traits_iterator_doctest_3032.rs
core_iter_traits_iterator_doctest_3090.rs
core_iter_traits_iterator_doctest_3100.rs
core_iter_traits_iterator_doctest_3153.rs
core_iter_traits_iterator_doctest_3189.rs
core_iter_traits_iterator_doctest_3214.rs
core_iter_traits_iterator_doctest_3247.rs
core_iter_traits_iterator_doctest_3274.rs
core_iter_traits_iterator_doctest_3307.rs
core_iter_traits_iterator_doctest_3336.rs
core_iter_traits_iterator_doctest_3482.rs
core_iter_traits_iterator_doctest_349.rs
core_iter_traits_iterator_doctest_356.rs
core_iter_traits_iterator_doctest_3564.rs
core_iter_traits_iterator_doctest_3642.rs
core_iter_traits_iterator_doctest_367.rs
core_iter_traits_iterator_doctest_412.rs
core_iter_traits_iterator_doctest_445.rs
core_iter_traits_iterator_doctest_465.rs
core_iter_traits_iterator_doctest_557.rs
core_iter_traits_iterator_doctest_56.rs
core_iter_traits_iterator_doctest_630.rs
core_iter_traits_iterator_doctest_841.rs
core_macros_mod_doctest_423.rs
core_macros_mod_doctest_540.rs
core_macros_mod_doctest_628.rs
core_macros_mod_doctest_682.rs
core_macros_mod_doctest_696.rs
core_mem_manually_drop_doctest_166.rs
core_mem_maybe_uninit_doctest_1048.rs
core_mem_maybe_uninit_doctest_1323.rs
core_mem_maybe_uninit_doctest_410.rs
core_mem_maybe_uninit_doctest_70.rs
core_net_ip_addr_doctest_15.rs
core_net_ip_addr_doctest_156.rs
core_net_ip_addr_doctest_60.rs
core_net_parser_doctest_488.rs
core_net_socket_addr_doctest_132.rs
core_net_socket_addr_doctest_22.rs
core_net_socket_addr_doctest_70.rs
core_num_dec2flt_mod_doctest_202.rs
core_num_int_macros_doctest_3620.rs
core_num_int_macros_doctest_3622.rs
core_num_int_macros_doctest_3624.rs
core_num_int_macros_doctest_3649.rs
core_num_int_macros_doctest_3651.rs
core_num_int_macros_doctest_3653.rs
core_num_int_macros_doctest_3689.rs
core_num_int_macros_doctest_3691.rs
core_num_int_macros_doctest_3693.rs
core_num_mod_doctest_1395.rs
core_num_mod_doctest_1401.rs
core_num_nonzero_doctest_1024.rs
core_num_nonzero_doctest_1063.rs
core_num_nonzero_doctest_1103.rs
core_num_nonzero_doctest_1141.rs
core_num_nonzero_doctest_1180.rs
core_num_nonzero_doctest_1442.rs
core_num_nonzero_doctest_1481.rs
core_num_nonzero_doctest_1520.rs
core_num_nonzero_doctest_1550.rs
core_num_nonzero_doctest_1590.rs
core_num_nonzero_doctest_1619.rs
core_num_nonzero_doctest_1647.rs
core_num_nonzero_doctest_1683.rs
core_num_nonzero_doctest_1712.rs
core_num_nonzero_doctest_1810.rs
core_num_nonzero_doctest_1840.rs
core_num_nonzero_doctest_1874.rs
core_num_nonzero_doctest_1908.rs
core_num_nonzero_doctest_1941.rs
core_num_nonzero_doctest_1973.rs
core_num_nonzero_doctest_2005.rs
core_num_nonzero_doctest_2031.rs
core_num_nonzero_doctest_2057.rs
core_num_nonzero_doctest_2089.rs
core_num_nonzero_doctest_2119.rs
core_num_nonzero_doctest_2154.rs
core_num_nonzero_doctest_571.rs
core_num_nonzero_doctest_601.rs
core_num_nonzero_doctest_628.rs
core_num_nonzero_doctest_658.rs
core_num_nonzero_doctest_688.rs
core_num_nonzero_doctest_712.rs
core_num_nonzero_doctest_736.rs
core_num_nonzero_doctest_771.rs
core_num_nonzero_doctest_802.rs
core_num_nonzero_doctest_829.rs
core_num_nonzero_doctest_857.rs
core_num_nonzero_doctest_887.rs
core_num_nonzero_doctest_920.rs
core_num_nonzero_doctest_953.rs
core_num_nonzero_doctest_986.rs
core_num_saturating_doctest_26.rs
core_num_saturating_doctest_331.rs
core_num_uint_macros_doctest_2849.rs
core_num_uint_macros_doctest_3572.rs
core_num_uint_macros_doctest_3574.rs
core_num_uint_macros_doctest_3575.rs
core_num_uint_macros_doctest_3601.rs
core_num_uint_macros_doctest_3603.rs
core_num_uint_macros_doctest_3604.rs
core_num_uint_macros_doctest_3641.rs
core_num_uint_macros_doctest_3643.rs
core_num_uint_macros_doctest_3644.rs
core_num_wrapping_doctest_1077.rs
core_num_wrapping_doctest_27.rs
core_num_wrapping_doctest_951.rs
core_ops_arith_doctest_1045.rs
core_ops_arith_doctest_158.rs
core_ops_arith_doctest_42.rs
core_ops_arith_doctest_664.rs
core_ops_arith_doctest_885.rs
core_ops_arith_doctest_948.rs
core_ops_arith_doctest_979.rs
core_ops_bit_doctest_768.rs
core_ops_bit_doctest_8.rs
core_ops_bit_doctest_844.rs
core_ops_control_flow_doctest_177.rs
core_ops_deref_doctest_242.rs
core_ops_deref_doctest_342.rs
core_ops_index_doctest_89.rs
core_ops_try_trait_doctest_101.rs
core_ops_try_trait_doctest_170.rs
core_ops_try_trait_doctest_23.rs
core_ops_try_trait_doctest_56.rs
core_ops_try_trait_doctest_79.rs
core_option_doctest_1023.rs
core_option_doctest_1107.rs
core_option_doctest_1320.rs
core_option_doctest_1373.rs
core_option_doctest_1397.rs
core_option_doctest_1439.rs
core_option_doctest_1470.rs
core_option_doctest_2012.rs
core_option_doctest_424.rs
core_option_doctest_482.rs
core_option_doctest_526.rs
core_option_doctest_748.rs
core_option_doctest_818.rs
core_option_doctest_828.rs
core_option_doctest_866.rs
core_option_doctest_926.rs
core_option_doctest_97.rs
core_option_doctest_991.rs
core_pin_doctest_1000.rs
core_pin_doctest_1170.rs
core_pin_doctest_1196.rs
core_pin_doctest_1250.rs
core_pin_doctest_1271.rs
core_pin_doctest_1808.rs
core_primitive_docs_doctest_129.rs
core_primitive_docs_doctest_416.rs
core_primitive_docs_doctest_443.rs
core_primitive_docs_doctest_679.rs
core_primitive_docs_doctest_704.rs
core_primitive_docs_doctest_860.rs
core_ptr_mod_doctest_1252.rs
core_ptr_mod_doctest_2395.rs
core_ptr_mut_ptr_doctest_603.rs
core_range_doctest_421.rs
core_range_doctest_46.rs
core_result_doctest_1026.rs
core_result_doctest_1052.rs
core_result_doctest_1103.rs
core_result_doctest_1242.rs
core_result_doctest_1414.rs
core_result_doctest_1500.rs
core_result_doctest_1817.rs
core_result_doctest_23.rs
core_result_doctest_771.rs
core_slice_iter_doctest_1317.rs
core_slice_iter_doctest_1471.rs
core_slice_iter_doctest_1844.rs
core_slice_iter_doctest_1880.rs
core_slice_iter_doctest_2314.rs
core_slice_iter_doctest_257.rs
core_slice_iter_doctest_2684.rs
core_slice_iter_doctest_2719.rs
core_slice_iter_doctest_289.rs
core_slice_iter_doctest_323.rs
core_slice_mod_doctest_1081.rs
core_slice_mod_doctest_161.rs
core_slice_mod_doctest_204.rs
core_slice_mod_doctest_246.rs
core_slice_mod_doctest_2662.rs
core_slice_mod_doctest_2702.rs
core_slice_mod_doctest_2736.rs
core_slice_mod_doctest_2779.rs
core_slice_mod_doctest_287.rs
core_slice_mod_doctest_341.rs
core_slice_mod_doctest_3626.rs
core_slice_mod_doctest_3672.rs
core_slice_mod_doctest_3695.rs
core_slice_mod_doctest_3774.rs
core_slice_mod_doctest_3837.rs
core_slice_mod_doctest_3964.rs
core_slice_mod_doctest_400.rs
core_slice_mod_doctest_4499.rs
core_slice_mod_doctest_4509.rs
core_slice_mod_doctest_4519.rs
core_slice_mod_doctest_4559.rs
core_slice_mod_doctest_4583.rs
core_slice_mod_doctest_4609.rs
core_slice_mod_doctest_461.rs
core_slice_mod_doctest_4633.rs
core_slice_mod_doctest_5048.rs
core_slice_mod_doctest_5076.rs
core_slice_mod_doctest_5207.rs
core_slice_mod_doctest_523.rs
core_slice_mod_doctest_584.rs
core_slice_mod_doctest_624.rs
core_slice_mod_doctest_667.rs
core_str_converts_doctest_75.rs
core_str_lossy_doctest_56.rs
core_str_mod_doctest_1014.rs
core_str_mod_doctest_1037.rs
core_str_mod_doctest_1118.rs
core_str_mod_doctest_1149.rs
core_str_mod_doctest_1161.rs
core_str_mod_doctest_1173.rs
core_str_mod_doctest_1200.rs
core_str_mod_doctest_1213.rs
core_str_mod_doctest_1225.rs
core_str_mod_doctest_1258.rs
core_str_mod_doctest_1273.rs
core_str_mod_doctest_1559.rs
core_str_mod_doctest_1574.rs
core_str_mod_doctest_1583.rs
core_str_mod_doctest_1610.rs
core_str_mod_doctest_2170.rs
core_str_mod_doctest_2209.rs
core_str_mod_doctest_2249.rs
core_str_mod_doctest_227.rs
core_str_mod_doctest_2289.rs
core_str_mod_doctest_2678.rs
core_str_mod_doctest_2686.rs
core_str_mod_doctest_2694.rs
core_str_mod_doctest_2790.rs
core_str_mod_doctest_2818.rs
core_str_mod_doctest_398.rs
core_str_mod_doctest_441.rs
core_str_mod_doctest_504.rs
core_str_mod_doctest_513.rs
core_str_mod_doctest_591.rs
core_str_mod_doctest_617.rs
core_str_mod_doctest_661.rs
core_str_mod_doctest_696.rs
core_str_mod_doctest_858.rs
core_str_mod_doctest_898.rs
core_str_mod_doctest_937.rs
core_str_pattern_doctest_18.rs
core_str_pattern_doctest_889.rs
core_str_traits_doctest_146.rs
core_str_traits_doctest_845.rs
core_str_traits_doctest_869.rs
core_str_traits_doctest_879.rs
core_task_poll_doctest_166.rs
core_task_poll_doctest_196.rs
core_task_ready_doctest_10.rs
core_task_ready_doctest_29.rs
core_time_doctest_56.rs
core_time_doctest_9.rs