Panic when using raw identifiers

[ChaseParate]

I found that when you use raw identifiers (e.g., r#in) either in spec function parameters or in the body (at minimum), verus panics.

2026-03-02-20-28-15.zip

Examples

use vstd::prelude::*;

verus! {

spec fn f(r#in: i32) -> bool {
    true
}

fn main() {
}

} // verus!

use vstd::prelude::*;

verus! {

spec fn g() -> bool {
    let r#for = 1i32;
    r#for == 1
}

fn main() {
}

} // verus!

Backtrace

$ verus src/main.rs

thread '<unnamed>' (1214038) panicked at air/src/smt_verify.rs:393:39:
no entry found for key
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace

thread '<unnamed>' (1214038) panicked at rust_verify/src/verifier.rs:415:17:
dropped, expected call to `into_inner` instead
stack backtrace:
   0:     0x7f19dc2ab193 - <std::sys::backtrace::BacktraceLock::print::DisplayBacktrace as core::fmt::Display>::fmt::h1851ca2a850bd9a9
   1:     0x7f19dca106c8 - core::fmt::write::h22467d3ad5dd5554
   2:     0x7f19ddeb23b6 - std::io::Write::write_fmt::h5e3b6a876f7a20bf
   3:     0x7f19dc278835 - std::panicking::default_hook::{{closure}}::he43c3ac33dfa4b50
   4:     0x7f19dc278663 - std::panicking::default_hook::hd124da54acf1152f
   5:     0x7f19dc278b2b - std::panicking::panic_with_hook::h9b5f1f19954f65a8
   6:     0x7f19dc27892a - std::panicking::panic_handler::{{closure}}::hf431df8c849ee0d6
   7:     0x7f19dc2728f9 - std::sys::backtrace::__rust_end_short_backtrace::hf97362b31a346cc0
   8:     0x7f19dc253a5d - __rustc[9e6a08e89e4b9111]::rust_begin_unwind
   9:     0x7f19d9555b5c - core::panicking::panic_fmt::ha4414e4328fe24a0
  10:     0x555a15920473 - core[5424e89100fc38d5]::ptr::drop_in_place::<core[5424e89100fc38d5]::option::Option<rust_verify[ed8fb1d5398c6a28]::verifier::util::PanicOnDropVec<(alloc[9e645bc090c49844]::sync::Arc<vir[a3daf83d6fd14791]::messages::MessageX>, air[a8d654438157815]::messages::MessageLevel)>>>
  11:     0x555a1590d577 - <rust_verify[ed8fb1d5398c6a28]::verifier::Verifier>::verify_bucket::<rust_verify[ed8fb1d5398c6a28]::verifier::QueuedReporter>
  12:     0x555a1591d835 - <rust_verify[ed8fb1d5398c6a28]::verifier::Verifier>::verify_bucket_outer::<rust_verify[ed8fb1d5398c6a28]::verifier::QueuedReporter>
  13:     0x555a159af872 - std[6c2a84ad8a8dd4fe]::sys::backtrace::__rust_begin_short_backtrace::<<rust_verify[ed8fb1d5398c6a28]::verifier::Verifier>::verify_crate_inner::{closure#1}, (rust_verify[ed8fb1d5398c6a28]::verifier::Verifier, alloc[9e645bc090c49844]::vec::Vec<core[5424e89100fc38d5]::result::Result<vir[a3daf83d6fd14791]::context::GlobalCtx, ()>>)>
  14:     0x555a159c44c7 - <std[6c2a84ad8a8dd4fe]::thread::lifecycle::spawn_unchecked<<rust_verify[ed8fb1d5398c6a28]::verifier::Verifier>::verify_crate_inner::{closure#1}, (rust_verify[ed8fb1d5398c6a28]::verifier::Verifier, alloc[9e645bc090c49844]::vec::Vec<core[5424e89100fc38d5]::result::Result<vir[a3daf83d6fd14791]::context::GlobalCtx, ()>>)>::{closure#1} as core[5424e89100fc38d5]::ops::function::FnOnce<()>>::call_once::{shim:vtable#0}
  15:     0x7f19ddb51538 - std::sys::thread::unix::Thread::new::thread_start::hc71bde616ea8b6e9
  16:     0x7f19d755a97a - <unknown>
  17:     0x7f19d75de2bc - <unknown>
  18:                0x0 - <unknown>

thread '<unnamed>' (1214038) panicked at library/core/src/panicking.rs:233:5:
panic in a destructor during cleanup
thread caused non-unwinding panic. aborting.
Aborted                    (core dumped) verus src/main.rs

verus --version

Verus
  Version: 0.2026.03.01.25809cb
  Profile: release
  Platform: linux_x86_64
  Toolchain: 1.93.1-x86_64-unknown-linux-gnu

I was also able to reproduce this on master as of Mon Mar 2 14:23:38 2026 -0800.