Issues

• SMT encoding crash: "Bound term variable not found" for an aliased local let rec called under a constant-pattern match

  FStarLang/FStar#4846 · Filter by author gebner opened on Nov 4, 2026

• Double free of zero-length array

  FStarLang/FStar#4799 · Filter by author mtzguido opened on Oct 26, 2026
  1

• Custard: generated *_init_globals silently breaks library code when not called

  FStarLang/FStar#4796 · Filter by author gebner opened on Oct 26, 2026

• requires let n = foo

  FStarLang/FStar#4740 · Filter by author gebner opened on Oct 20, 2026

• "Patterns are incomplete" at fuel 0 when the scrutinee's argument is (assert_norm p; e)

  FStarLang/FStar#4705 · Filter by author karthikbhargavan opened on Oct 18, 2026

• Exponential time and memory for nested matches under a postcondition that destructures with let

  FStarLang/FStar#4695 · Filter by author karthikbhargavan opened on Oct 17, 2026

• Feature request: 64-bit compare-and-swap in Pulse.Lib.Primitives

  FStarLang/FStar#4671 · Filter by author sheeraSearch82 opened on Oct 13, 2026

• MD5 collision in SMT term identity proves False

  kind/unsoundness
  FStarLang/FStar#4600 · Filter by author hei411 opened on Sep 24, 2026
  2

• Unboxed SMT encoding

  FStarLang/FStar#4598 · Filter by author gebner opened on Sep 24, 2026
  1

• --include "" walks the whole filesystem from / (dependency analysis hangs)

  FStarLang/FStar#4593 · Filter by author gebner opened on Sep 24, 2026

• nightly-2026-09-23: nonlinear nat arithmetic times out where 2026.09.20 used 12% of its rlimit (not fixed by FSTAR_NO_DEDUP_VC, not by 8x rlimit)

  FStarLang/FStar#4592 · Filter by author gebner opened on Sep 24, 2026
  1

• Large SMT regression in nightly-2026-09-23: an unused Lemma in scope makes a later proof 20x more expensive

  FStarLang/FStar#4591 · Filter by author gebner opened on Sep 24, 2026
  3

• Custard: [@@normalize_for_extraction] is much more expensive than the legacy backend

  FStarLang/FStar#4582 · Filter by author gebner opened on Sep 23, 2026
  1

• Local let-rec syntax-hash collisions allow proving False

  kind/unsoundness
  FStarLang/FStar#4562 · Filter by author hei411 opened on Sep 22, 2026
  4

• Custard: extraction output depends on which .fst.checked files happen to exist

  FStarLang/FStar#4559 · Filter by author gebner opened on Sep 22, 2026

• Pulse: !r in a ghost argument position compiles to a real read

  FStarLang/FStar#4539 · Filter by author gebner opened on Sep 11, 2026

• Pulse early return skips leftover resources check

  FStarLang/FStar#4536 · Filter by author amosr-msft opened on Sep 10, 2026

• Flacky extraction tests, or something?

  FStarLang/FStar#4525 · Filter by author kant2002 opened on Sep 5, 2026

• --ext context_pruning=false / prune_decls=false produce duplicate SMT declarations, breaking all queries

  FStarLang/FStar#4495 · Filter by author gebner opened on Aug 27, 2026

• Pulse loop invariant: same SMT goal costs 0.65 rlimit on 2026.06.14 and exhausts rlimit 5 on 2026.08.16

  FStarLang/FStar#4488 · Filter by author gebner opened on Aug 26, 2026
  1

• inspect_ln, a Tot function, hard-crashes F* on three constants reachable from ordinary source syntax

  kind/crash
  FStarLang/FStar#4483 · Filter by author hei411 opened on Aug 25, 2026

• inspect_pack_sigelt is false for *every* Sg_Inductive: the reflection API proves False

  kind/unsoundness
  FStarLang/FStar#4480 · Filter by author hei411 opened on Aug 25, 2026

• pack_fv [] crashes F* (Failure("impossible")) — #2632 was fixed at the wrong layer

  kind/crash
  FStarLang/FStar#4479 · Filter by author hei411 opened on Aug 25, 2026

• inspect_pack_inv is false at Tv_UInst fv [] and Tv_Unsupp: the reflection API proves False

  kind/unsoundness
  FStarLang/FStar#4478 · Filter by author hei411 opened on Aug 25, 2026

• Internal error: indexed effects declared with the effect { ... } shorthand crash F* (tc_maybe_toplevel_term: not LN)

  kind/crash
  FStarLang/FStar#4477 · Filter by author hei411 opened on Aug 25, 2026