Checker "canonical-min" on test "bugs/loose-bvar-value"
Checker: canonical-min · Version: kernel-arena (0acb45d) · 📄 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: 🚫 declined · exit code 2 · wall time: 996 ms · instructions: 3.3 G · max rss memory: 1.1 GB · run 2026-10-27 12:18:59 UTC
stderr:
PANIC at Lean.Meta.whnfEasyCases Lean.Meta.WHNF:381:22: loose bvar in expression backtrace: .lake/build/bin/canonical-min-arena(+0x6093c6e) [0x55d6da22ec6e] .lake/build/bin/canonical-min-arena(+0x60940fc) [0x55d6da22f0fc] .lake/build/bin/canonical-min-arena(+0x11cdcdb) [0x55d6d5368cdb] .lake/build/bin/canonical-min-arena(+0x11cc7f7) [0x55d6d53677f7] .lake/build/bin/canonical-min-arena(+0x11f9fb3) [0x55d6d5394fb3] .lake/build/bin/canonical-min-arena(+0x60a668a) [0x55d6da24168a] .lake/build/bin/canonical-min-arena(+0x11fbf18) [0x55d6d5396f18] .lake/build/bin/canonical-min-arena(+0x924fd) [0x55d6d422d4fd] .lake/build/bin/canonical-min-arena(+0x8f4c6) [0x55d6d422a4c6] .lake/build/bin/canonical-min-arena(+0x60ab50c) [0x55d6da24650c] .lake/build/bin/canonical-min-arena(+0x845b4) [0x55d6d421f5b4] .lake/build/bin/canonical-min-arena(+0x60a78bf) [0x55d6da2428bf] .lake/build/bin/canonical-min-arena(+0x134f14c) [0x55d6d54ea14c] .lake/build/bin/canonical-min-arena(+0x134f55f) [0x55d6d54ea55f] .lake/build/bin/canonical-min-arena(+0x84645) [0x55d6d421f645] .lake/build/bin/canonical-min-arena(+0x92260) [0x55d6d422d260] .lake/build/bin/canonical-min-arena(+0xe2552) [0x55d6d427d552] .lake/build/bin/canonical-min-arena(+0xe650e) [0x55d6d428150e] .lake/build/bin/canonical-min-arena(+0x60a668a) [0x55d6da24168a] .lake/build/bin/canonical-min-arena(+0x207aa) [0x55d6d41bb7aa] .lake/build/bin/canonical-min-arena(+0x2168e) [0x55d6d41bc68e] .lake/build/bin/canonical-min-arena(+0x2454f) [0x55d6d41bf54f] .lake/build/bin/canonical-min-arena(+0x25025) [0x55d6d41c0025] .lake/build/bin/canonical-min-arena(+0x25933) [0x55d6d41c0933] .lake/build/bin/canonical-min-arena(+0x1e792) [0x55d6d41b9792] /nix/store/8kvxvr3pmsypxiypq4g8zy13glnfr7nx-glibc-2.42-67/lib/libc.so.6(+0x2b285) [0x7f5a58220285] /nix/store/8kvxvr3pmsypxiypq4g8zy13glnfr7nx-glibc-2.42-67/lib/libc.so.6(__libc_start_main+0x88) [0x7f5a58220338] .lake/build/bin/canonical-min-arena(+0x1f895) [0x55d6d41ba895] Declined: could not translate f: goal ?[anonymous]