Reachable unwrap panic in Debugger::eval_expr #2176
Description
Reproduce
$ verus ./poc_debugger_line_unset.rs -V debug --num-threads 1use vstd::prelude::*;
verus!{
proof fn p(){
assert(false);
}
fn main(){}
}Panic Log
verus/source/rust_verify/src/debugger.rs
Line 152 in ac50b8f
Z3 model: [ModelDefX { name: "fuel%vstd!multiset.group_multiset_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!20" }, ModelDefX { name: "fuel%vstd!std_specs.hash.group_hash_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!32" }, ModelDefX { name: "fuel%vstd!laws_cmp.group_laws_cmp.", params: [], ret: Named("FuelId"), body: "FuelId!val!2" }, ModelDefX { name: "fuel%vstd!std_specs.vecdeque.group_vec_dequeue_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!36" }, ModelDefX { name: "fuel%vstd!laws_eq.isize_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!15" }, ModelDefX { name: "fuel%vstd!laws_eq.u64_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!10" }, ModelDefX { name: "fuel%vstd!map.group_map_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!19" }, ModelDefX { name: "fuel%vstd!std_specs.bits.group_bits_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!29" }, ModelDefX { name: "$", params: [], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "fuel%vstd!laws_eq.i32_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!9" }, ModelDefX { name: "fuel%vstd!laws_eq.bool_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!3" }, ModelDefX { name: "fuel%vstd!laws_eq.i16_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!7" }, ModelDefX { name: "fuel%vstd!laws_eq.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!16" }, ModelDefX { name: "fuel%vstd!laws_eq.usize_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!14" }, ModelDefX { name: "fuel%vstd!layout.group_align_properties.", params: [], ret: Named("FuelId"), body: "FuelId!val!17" }, ModelDefX { name: "fuel%vstd!set.group_set_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!25" }, ModelDefX { name: "%%location_label%%0", params: [], ret: Bool, body: "true" }, ModelDefX { name: "fuel%vstd!string.group_string_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!28" }, ModelDefX { name: "fuel%vstd!set_lib.group_set_lib_default.", params: [], ret: Named("FuelId"), body: "FuelId!val!26" }, ModelDefX { name: "fuel%vstd!slice.group_slice_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!27" }, ModelDefX { name: "fuel%vstd!array.group_array_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!0" }, ModelDefX { name: "fuel%vstd!std_specs.vec.group_vec_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!35" }, ModelDefX { name: "fuel%vstd!raw_ptr.group_raw_ptr_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!21" }, ModelDefX { name: "fuel%vstd!std_specs.manually_drop.group_manually_drop_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!31" }, ModelDefX { name: "fuel%vstd!std_specs.range.group_range_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!33" }, ModelDefX { name: "fuel%vstd!std_specs.slice.group_slice_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!34" }, ModelDefX { name: "fuel%vstd!seq.group_seq_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!22" }, ModelDefX { name: "fuel%vstd!laws_eq.u128_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!12" }, ModelDefX { name: "fuel%vstd!seq_lib.group_filter_ensures.", params: [], ret: Named("FuelId"), body: "FuelId!val!23" }, ModelDefX { name: "fuel%vstd!laws_eq.u16_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!6" }, ModelDefX { name: "fuel%vstd!laws_eq.i8_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!5" }, ModelDefX { name: "fuel%vstd!laws_eq.i64_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!11" }, ModelDefX { name: "fuel%vstd!std_specs.control_flow.group_control_flow_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!30" }, ModelDefX { name: "fuel%vstd!laws_eq.i128_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!13" }, ModelDefX { name: "fuel%vstd!layout.group_layout_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!18" }, ModelDefX { name: "fuel%vstd!group_vstd_default.", params: [], ret: Named("FuelId"), body: "FuelId!val!37" }, ModelDefX { name: "fuel%vstd!seq_lib.group_seq_lib_default.", params: [], ret: Named("FuelId"), body: "FuelId!val!24" }, ModelDefX { name: "SZ", params: [], ret: Int, body: "32" }, ModelDefX { name: "fuel_defaults", params: [], ret: Bool, body: "true" }, ModelDefX { name: "fuel%vstd!laws_eq.u32_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!8" }, ModelDefX { name: "fuel%vstd!function.group_function_axioms.", params: [], ret: Named("FuelId"), body: "FuelId!val!1" }, ModelDefX { name: "fuel%vstd!laws_eq.u8_laws.group_laws_eq.", params: [], ret: Named("FuelId"), body: "FuelId!val!4" }, ModelDefX { name: "$dyn", params: [], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "REAL", params: [], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "$slice", params: [], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "ALLOCATOR_GLOBAL", params: [], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "TYPE%tuple%0.", params: [], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "zero", params: [], ret: Named("Fuel"), body: "Fuel!val!0" }, ModelDefX { name: "CHAR", params: [], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "ISIZE", params: [], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "BOOL", params: [], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "no%param", params: [], ret: Int, body: "0" }, ModelDefX { name: "STRSLICE", params: [], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "INT", params: [], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "USIZE", params: [], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "NAT", params: [], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "sized", params: ["x!0" -> Named("Dcr")], ret: Bool, body: "true" }, ModelDefX { name: "iLo", params: ["x!0" -> Int], ret: Int, body: "(ite\n (= x!0 16)\n (- 32768)\n (ite\n (= x!0 32)\n (- 2147483648)\n (ite\n (= x!0 64)\n (- 9223372036854775808)\n (ite\n (= x!0 128)\n (- 170141183460469231731687303715884105728)\n (- 128)\n))))" }, ModelDefX { name: "fuel_bool_default", params: ["x!0" -> Named("FuelId")], ret: Bool, body: "true" }, ModelDefX { name: "uHi", params: ["x!0" -> Int], ret: Int, body: "(ite\n (= x!0 16)\n 65536\n (ite\n (= x!0 32)\n 4294967296\n (ite\n (= x!0 64)\n 18446744073709551616\n (ite\n (= x!0 128)\n 340282366920938463463374607431768211456\n 256\n))))" }, ModelDefX { name: "iHi", params: ["x!0" -> Int], ret: Int, body: "(ite\n (= x!0 16)\n 32768\n (ite\n (= x!0 32)\n 2147483648\n (ite\n (= x!0 64)\n 9223372036854775808\n (ite\n (= x!0 128)\n 170141183460469231731687303715884105728\n 128\n))))" }, ModelDefX { name: "%I", params: ["x!0" -> Named("Poly")], ret: Int, body: "0" }, ModelDefX { name: "NEVER", params: ["x!0" -> Named("Dcr")], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "iInv", params: ["x!0" -> Int, "x!1" -> Int], ret: Bool, body: "false" }, ModelDefX { name: "charClip", params: ["x!0" -> Int], ret: Int, body: "0" }, ModelDefX { name: "MUT_REF", params: ["x!0" -> Named("Dcr")], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "RC", params: ["x!0" -> Named("Dcr"), "x!1" -> Named("Type"), "x!2" -> Named("Dcr")], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "bitand", params: ["x!0" -> Named("Poly"), "x!1" -> Named("Poly")], ret: Int, body: "0" }, ModelDefX { name: "bitshl", params: ["x!0" -> Named("Poly"), "x!1" -> Named("Poly")], ret: Int, body: "0" }, ModelDefX { name: "charInv", params: ["x!0" -> Int], ret: Bool, body: "false" }, ModelDefX { name: "%B", params: ["x!0" -> Named("Poly")], ret: Bool, body: "false" }, ModelDefX { name: "check_decrease_int", params: ["x!0" -> Int, "x!1" -> Int, "x!2" -> Bool], ret: Bool, body: "false" }, ModelDefX { name: "DST", params: ["x!0" -> Named("Dcr")], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "RDiv", params: ["x!0" -> Real, "x!1" -> Real], ret: Real, body: "0.0" }, ModelDefX { name: "GHOST", params: ["x!0" -> Named("Dcr")], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "closure_req", params: ["x!0" -> Named("Type"), "x!1" -> Named("Dcr"), "x!2" -> Named("Type"), "x!3" -> Named("Poly"), "x!4" -> Named("Poly")], ret: Bool, body: "false" }, ModelDefX { name: "F", params: ["x!0" -> Named("fndef")], ret: Named("Poly"), body: "Poly!val!0" }, ModelDefX { name: "check_decrease_height", params: ["x!0" -> Named("Poly"), "x!1" -> Named("Poly"), "x!2" -> Bool], ret: Bool, body: "false" }, ModelDefX { name: "iClip", params: ["x!0" -> Int, "x!1" -> Int], ret: Int, body: "0" }, ModelDefX { name: "%Poly%tuple%0.", params: ["x!0" -> Named("Poly")], ret: Named("tuple%0."), body: "tuple%0./tuple%0" }, ModelDefX { name: "fuel_bool", params: ["x!0" -> Named("FuelId")], ret: Bool, body: "false" }, ModelDefX { name: "bitor", params: ["x!0" -> Named("Poly"), "x!1" -> Named("Poly")], ret: Int, body: "0" }, ModelDefX { name: "R", params: ["x!0" -> Real], ret: Named("Poly"), body: "Poly!val!0" }, ModelDefX { name: "%F", params: ["x!0" -> Named("Poly")], ret: Named("fndef"), body: "fndef_singleton" }, ModelDefX { name: "RAdd", params: ["x!0" -> Real, "x!1" -> Real], ret: Real, body: "0.0" }, ModelDefX { name: "BOX", params: ["x!0" -> Named("Dcr"), "x!1" -> Named("Type"), "x!2" -> Named("Dcr")], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "SLICE", params: ["x!0" -> Named("Dcr"), "x!1" -> Named("Type")], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "EucDiv", params: ["x!0" -> Int, "x!1" -> Int], ret: Int, body: "0" }, ModelDefX { name: "height", params: ["x!0" -> Named("Poly")], ret: Named("Height"), body: "Height!val!0" }, ModelDefX { name: "Add", params: ["x!0" -> Int, "x!1" -> Int], ret: Int, body: "0" }, ModelDefX { name: "const_int", params: ["x!0" -> Named("Type")], ret: Int, body: "0" }, ModelDefX { name: "uClip", params: ["x!0" -> Int, "x!1" -> Int], ret: Int, body: "0" }, ModelDefX { name: "CONST_BOOL", params: ["x!0" -> Bool], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "nClip", params: ["x!0" -> Int], ret: Int, body: "0" }, ModelDefX { name: "fun_from_recursive_field", params: ["x!0" -> Named("Poly")], ret: Named("Poly"), body: "Poly!val!0" }, ModelDefX { name: "singular_mod", params: ["x!0" -> Int, "x!1" -> Int], ret: Int, body: "0" }, ModelDefX { name: "REF", params: ["x!0" -> Named("Dcr")], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "ARRAY", params: ["x!0" -> Named("Dcr"), "x!1" -> Named("Type"), "x!2" -> Named("Dcr"), "x!3" -> Named("Type")], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "const_bool", params: ["x!0" -> Named("Type")], ret: Bool, body: "false" }, ModelDefX { name: "RMul", params: ["x!0" -> Real, "x!1" -> Real], ret: Real, body: "0.0" }, ModelDefX { name: "ARC", params: ["x!0" -> Named("Dcr"), "x!1" -> Named("Type"), "x!2" -> Named("Dcr")], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "SINT", params: ["x!0" -> Int], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "mut_ref_update_current%", params: ["x!0" -> Named("Poly"), "x!1" -> Named("Poly")], ret: Named("Poly"), body: "Poly!val!0" }, ModelDefX { name: "succ", params: ["x!0" -> Named("Fuel")], ret: Named("Fuel"), body: "Fuel!val!0" }, ModelDefX { name: "Poly%tuple%0.", params: ["x!0" -> Named("tuple%0.")], ret: Named("Poly"), body: "Poly!val!0" }, ModelDefX { name: "CONST_PTR", params: ["x!0" -> Named("Dcr")], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "ext_eq", params: ["x!0" -> Bool, "x!1" -> Named("Type"), "x!2" -> Named("Poly"), "x!3" -> Named("Poly")], ret: Bool, body: "false" }, ModelDefX { name: "%R", params: ["x!0" -> Named("Poly")], ret: Real, body: "0.0" }, ModelDefX { name: "B", params: ["x!0" -> Bool], ret: Named("Poly"), body: "Poly!val!0" }, ModelDefX { name: "mut_ref_future%", params: ["x!0" -> Named("Poly")], ret: Named("Poly"), body: "Poly!val!0" }, ModelDefX { name: "has_type", params: ["x!0" -> Named("Poly"), "x!1" -> Named("Type")], ret: Bool, body: "false" }, ModelDefX { name: "Mul", params: ["x!0" -> Int, "x!1" -> Int], ret: Int, body: "0" }, ModelDefX { name: "bitnot", params: ["x!0" -> Named("Poly")], ret: Int, body: "0" }, ModelDefX { name: "RSub", params: ["x!0" -> Real, "x!1" -> Real], ret: Real, body: "0.0" }, ModelDefX { name: "I", params: ["x!0" -> Int], ret: Named("Poly"), body: "Poly!val!0" }, ModelDefX { name: "default_ens", params: ["x!0" -> Named("Type"), "x!1" -> Named("Dcr"), "x!2" -> Named("Type"), "x!3" -> Named("Poly"), "x!4" -> Named("Poly"), "x!5" -> Named("Poly")], ret: Bool, body: "false" }, ModelDefX { name: "height_lt", params: ["x!0" -> Named("Height"), "x!1" -> Named("Height")], ret: Bool, body: "false" }, ModelDefX { name: "mk_fun", params: ["x!0" -> Named("%%Function%%")], ret: Named("%%Function%%"), body: "%%Function%%!val!0" }, ModelDefX { name: "CONST_INT", params: ["x!0" -> Int], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "as_type", params: ["x!0" -> Named("Poly"), "x!1" -> Named("Type")], ret: Named("Poly"), body: "Poly!val!0" }, ModelDefX { name: "mut_ref_current%", params: ["x!0" -> Named("Poly")], ret: Named("Poly"), body: "Poly!val!0" }, ModelDefX { name: "bitshr", params: ["x!0" -> Named("Poly"), "x!1" -> Named("Poly")], ret: Int, body: "0" }, ModelDefX { name: "TRACKED", params: ["x!0" -> Named("Dcr")], ret: Named("Dcr"), body: "Dcr!val!0" }, ModelDefX { name: "closure_ens", params: ["x!0" -> Named("Type"), "x!1" -> Named("Dcr"), "x!2" -> Named("Type"), "x!3" -> Named("Poly"), "x!4" -> Named("Poly"), "x!5" -> Named("Poly")], ret: Bool, body: "false" }, ModelDefX { name: "MUTREF", params: ["x!0" -> Named("Dcr"), "x!1" -> Named("Type")], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "EucMod", params: ["x!0" -> Int, "x!1" -> Int], ret: Int, body: "0" }, ModelDefX { name: "Sub", params: ["x!0" -> Int, "x!1" -> Int], ret: Int, body: "0" }, ModelDefX { name: "has_resolved", params: ["x!0" -> Named("Dcr"), "x!1" -> Named("Type"), "x!2" -> Named("Poly")], ret: Bool, body: "false" }, ModelDefX { name: "FLOAT", params: ["x!0" -> Int], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "PTR", params: ["x!0" -> Named("Dcr"), "x!1" -> Named("Type")], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "UINT", params: ["x!0" -> Int], ret: Named("Type"), body: "Type!val!0" }, ModelDefX { name: "bitxor", params: ["x!0" -> Named("Poly"), "x!1" -> Named("Poly")], ret: Int, body: "0" }, ModelDefX { name: "uInv", params: ["x!0" -> Int, "x!1" -> Int], ret: Bool, body: "false" }]
3 assigned to "0_entry"
4 assigned to "0_entry"
Span from 3 to 5 => SnapPos { snapshot_id: "0_entry", kind: Start }
Span from 3 to 5 => SnapPos { snapshot_id: "0_entry", kind: Start }
Span from 4 to 4 => SnapPos { snapshot_id: "0_entry", kind: Full }
Span from 4 to 4 => SnapPos { snapshot_id: "0_entry", kind: Full }
welcome to verus debugger shell
invalid line number 26, no snapshot found
thread 'rustc' (1827985) panicked at rust_verify/src/debugger.rs:152:50:
called `Option::unwrap()` on a `None` value
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread 'rustc' (1827985) panicked at rust_verify/src/verifier.rs:386:17:
dropped, expected call to `into_inner` instead
stack backtrace:
0: 0x77e1c68aae73 - <std::sys::backtrace::BacktraceLock::print::DisplayBacktrace as core::fmt::Display>::fmt::hac1d885928ba8582
1: 0x77e1c7010508 - core::fmt::write::h83ebb4d32483be9e
2: 0x77e1c84b4cf6 - std::io::Write::write_fmt::ha6a1d6c1ea64b2d0
3: 0x77e1c6878515 - std::panicking::default_hook::{{closure}}::h8e9c4d1276f0925f
4: 0x77e1c6878343 - std::panicking::default_hook::h2b2078d38b534dfb
5: 0x77e1c687880b - std::panicking::panic_with_hook::h39b739724e701bfd
6: 0x77e1c687860a - std::panicking::panic_handler::{{closure}}::he540c4833054e458
7: 0x77e1c68725d9 - std::sys::backtrace::__rust_end_short_backtrace::hfa179d89deec8aed
8: 0x77e1c685364d - __rustc[d131491b17107b07]::rust_begin_unwind
9: 0x77e1c3b2384c - core::panicking::panic_fmt::ha564519d657d9c46
10: 0x5feffc3b9623 - core[fcada436b717a91e]::ptr::drop_in_place::<core[fcada436b717a91e]::option::Option<rust_verify[3e5c60f9687fa8eb]::verifier::util::PanicOnDropVec<(alloc[cfeb9a527306e1a7]::sync::Arc<vir[7c5bf28d1d867c4d]::messages::MessageX>, air[3553b07fb5efe012]::messages::MessageLevel)>>>
11: 0x5feffc3af0cc - <rust_verify[3e5c60f9687fa8eb]::verifier::Verifier>::verify_bucket::<rust_verify[3e5c60f9687fa8eb]::verifier::Reporter>
12: 0x5feffc3c8f17 - <rust_verify[3e5c60f9687fa8eb]::verifier::Verifier>::verify_crate_inner
13: 0x5feffc3d2c80 - <rust_verify[3e5c60f9687fa8eb]::verifier::VerifierCallbacksEraseMacro>::finish_verus
14: 0x5feffc3d592a - <rust_verify[3e5c60f9687fa8eb]::verifier::VerifierCallbacksEraseMacro as rustc_driver_impl[faaaf75c5cd7107d]::Callbacks>::after_expansion
15: 0x77e1c835f154 - <rustc_interface[fc4a506f334ac7d7]::passes::create_and_enter_global_ctxt<core[fcada436b717a91e]::option::Option<rustc_interface[fc4a506f334ac7d7]::queries::Linker>, rustc_driver_impl[faaaf75c5cd7107d]::run_compiler::{closure#0}::{closure#2}>::{closure#2} as core[fcada436b717a91e]::ops::function::FnOnce<(&rustc_session[c2edea43106fece4]::session::Session, rustc_middle[9ef750b7bb32b8b9]::ty::context::CurrentGcx, alloc[cfeb9a527306e1a7]::sync::Arc<rustc_data_structures[f905cb25ec31ff7c]::jobserver::Proxy>, &std[5414f88c956f4157]::sync::once_lock::OnceLock<rustc_middle[9ef750b7bb32b8b9]::ty::context::GlobalCtxt>, &rustc_data_structures[f905cb25ec31ff7c]::sync::worker_local::WorkerLocal<rustc_middle[9ef750b7bb32b8b9]::arena::Arena>, &rustc_data_structures[f905cb25ec31ff7c]::sync::worker_local::WorkerLocal<rustc_hir[51e6b31522dd2ac2]::Arena>, rustc_driver_impl[faaaf75c5cd7107d]::run_compiler::{closure#0}::{closure#2})>>::call_once::{shim:vtable#0}
16: 0x77e1c81f1e05 - rustc_interface[fc4a506f334ac7d7]::interface::run_compiler::<(), rustc_driver_impl[faaaf75c5cd7107d]::run_compiler::{closure#0}>::{closure#1}
17: 0x77e1c815890a - std[5414f88c956f4157]::sys::backtrace::__rust_begin_short_backtrace::<rustc_interface[fc4a506f334ac7d7]::util::run_in_thread_with_globals<rustc_interface[fc4a506f334ac7d7]::util::run_in_thread_pool_with_globals<rustc_interface[fc4a506f334ac7d7]::interface::run_compiler<(), rustc_driver_impl[faaaf75c5cd7107d]::run_compiler::{closure#0}>::{closure#1}, ()>::{closure#0}, ()>::{closure#0}::{closure#0}, ()>
18: 0x77e1c81586dd - <std[5414f88c956f4157]::thread::lifecycle::spawn_unchecked<rustc_interface[fc4a506f334ac7d7]::util::run_in_thread_with_globals<rustc_interface[fc4a506f334ac7d7]::util::run_in_thread_pool_with_globals<rustc_interface[fc4a506f334ac7d7]::interface::run_compiler<(), rustc_driver_impl[faaaf75c5cd7107d]::run_compiler::{closure#0}>::{closure#1}, ()>::{closure#0}, ()>::{closure#0}::{closure#0}, ()>::{closure#1} as core[fcada436b717a91e]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
19: 0x77e1c815bcf8 - std::sys::thread::unix::Thread::new::thread_start::h45cc87bb053add0f
20: 0x77e1c1a9caa4 - start_thread
at ./nptl/pthread_create.c:447:8
21: 0x77e1c1b29c6c - clone3
at ./misc/../sysdeps/unix/sysv/linux/x86_64/clone3.S:78:0
22: 0x0 - <unknown>
thread 'rustc' (1827985) panicked at library/core/src/panicking.rs:233:5:
panic in a destructor during cleanup
thread caused non-unwinding panic. aborting.
[1] 1827774 IOT instruction (core dumped) ./poc_debugger_line_unset.rs -V debug --num-threads 1
Env
Verus Version: ac50b8f
OS: Ubuntu 24.04.1 LTS