Reachable `unwrap` panic in `eval_seq`

[Marsman1996]

PoC

use vstd::prelude::*;
use vstd::seq::*;

verus! {

proof fn test() {
    assert(Seq::<int>::new(18446744073709551616nat, |i: int| 0int).len() == 0) by (compute_only);
}

fn main() {}

} // verus!

Panic Log

verus/source/vir/src/interpreter.rs

Line 920 in ac50b8f

Const(Constant::Int(index)) => Some(BigInt::to_usize(index).unwrap()),

thread 'interpreter' (48) panicked at vir/src/interpreter.rs:920:77:
called `Option::unwrap()` on a `None` value
note: [run with `RUST_BACKTRACE=1` environment variable to display a backtrace](https://play.verus-lang.org/?version=stable&mode=basic&edition=2021#)

thread '<unnamed>' (47) panicked at /playground/verus/source/vir/src/interpreter.rs:2108:24:
called `Result::unwrap()` on an `Err` value: Any { .. }

thread '<unnamed>' (47) panicked at rust_verify/src/verifier.rs:2154:29:
worker thread panicked

Env

Verus Version: 2026.02.12 ac50b8f

Playground Link

https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=18174e13ab968cfb2611fbe20b9d7205