Search results

Pulse:  while -guard post-condition inference fails for a stateful conditional guard when the loop has an  ensures  clause (Error 339, "Cannot find witness")

Status: Open.

#4330 In FStarLang/FStar;

· KimayaBedarkar opened on Jun 23, 2026

Pulse reports failed postcondition at final expression instead of ensures

Status: Open.

#4321 In FStarLang/FStar;

· KimayaBedarkar opened on Jun 17, 2026

Join-point inference unhelpful for array assignments

Status: Open.

#4319 In FStarLang/FStar;

· gebner opened on Jun 17, 2026

Problems opening a module that was previously imported under a given name

Status: Open.

#4301 In FStarLang/FStar;

· jberthold-ms opened on Jun 7, 2026

Pulse existential inference fails when struct field appears in separation logic predicate

Status: Open.

#4298 In FStarLang/FStar;

· gebner opened on Jun 3, 2026

Ascriptions in local lets seemingly dropped

Status: Open.

#4291 In FStarLang/FStar;

· mtzguido opened on Jun 2, 2026

ANF + ascription does not work

Status: Open.

#4290 In FStarLang/FStar;

· mtzguido opened on Jun 2, 2026

Backward errors

Status: Open.

#4267 In FStarLang/FStar;

· mtzguido opened on May 18, 2026

Example of matching loop

Status: Open.

#4264 In FStarLang/FStar;

· mtzguido opened on May 17, 2026

Simple expression if fails

Status: Open.

#4263 In FStarLang/FStar;

· mtzguido opened on May 16, 2026

A val can break a proof

Status: Open.

#4245 In FStarLang/FStar;

· mtzguido opened on May 5, 2026

Semi-unsoundness: all magics are equal, all admits are equal

Status: Open.

#4244 In FStarLang/FStar;

· mtzguido opened on May 5, 2026