Checker "nanobruijn" on test "bugs/loose-bvar-value"
Checker: nanobruijn · Version: 7a04996 · 📄 Declaration · 🔗 Source
Test: bugs/loose-bvar-value · Expected: ✋ reject · Size: 2.7 KB · Lines: 48 · lean4export: 3.1.0 · Lean: 4.34.1 · 📄 Declaration
Result: ✋ rejected · exit code 1 · wall time: 29.1 ms · instructions: 3.6 M · max rss memory: 5.4 MB · run 2026-10-27 12:14:06 UTC
stderr:
ExprPtr parse: 31 parser entries → 27 DAG entries, 4 OSNF-shifted, 26 live after compaction, 0 cores with bvar indices >= 64 (0 tail words)
thread 'thread_3' (4811) panicked at src/util.rs:2151:9:
local_type: dbj_idx=0 >= depth=0
note: run with `RUST_BACKTRACE=1` environment variable to display a backtrace
thread 'thread_2' (4810) panicked at src/tc.rs:579:17:
infer_sort_of: expected Sort, got "App(V0+0,Sort(ExportFile@2)+65535)" from e="V0", infer="App(C(f)+65535,Sort(ExportFile@2)+65535)", depth=1
thread 'thread_1' (4809) panicked at src/tc.rs:579:17:
infer_sort_of: expected Sort, got "App(V0+0,Sort(ExportFile@2)+65535)" from e="V0", infer="App(C(f)+65535,Sort(ExportFile@2)+65535)", depth=2
thread 'thread_0' (4808) panicked at src/tc.rs:556:18:
ensure_sort could not produce a sort
thread 'main-worker' (4807) panicked at src/tc.rs:324:26:
A thread in `check_all_declars` panicked while being joined: Any { .. }
thread 'main' (4806) panicked at src/main.rs:11:20:
called `Result::unwrap()` on an `Err` value: Any { .. }