All issues

Search results

Add a Pure(T) wrapper for types to be able to use Mutable types in pure context

Status: Open.

#1779 In epfl-lara/stainless;

· samuelchassot opened on Aug 26, 2026

Cannot establish a reference to L#rev

Status: Open.

#1776 In epfl-lara/stainless;

· mbovel opened on Aug 20, 2026

Crash when a function parameter refinement refers to another parameter that happens to be mutated

Status: Open.

#1775 In epfl-lara/stainless;

· samuelchassot opened on Aug 20, 2026

Compile BigInt as Int in genc

Status: Open.

#1773 In epfl-lara/stainless;

· samuelchassot opened on Aug 19, 2026

Refinement types can introduce multiple duplicate VCs

Status: Open.

#1772 In epfl-lara/stainless;

· samuelchassot opened on Aug 19, 2026

Lost require

Status: Open.

#1771 In epfl-lara/stainless;

· mbovel opened on Aug 18, 2026

Non-deterministic very slow verification

Status: Open.

#1766 In epfl-lara/stainless;

· mbovel opened on Jul 18, 2026

Undesirable type casts and bindings added in AntiAliasing phase

aliasingAlias and effect analysis for imperativeAlias and effect analysis for imperative

imperative

Status: Open.

#1743 In epfl-lara/stainless;

· vkuncak opened on Jun 4, 2026

Stainless crash: Variable ... is not defined in context when lifting two while loops

Status: Open.

#1742 In epfl-lara/stainless;

· sfiruch opened on Jun 3, 2026

Assertion error when using var with Map.updated

aliasingAlias and effect analysis for imperativeAlias and effect analysis for imperative

bug

imperative

Status: Open.

#1714 In epfl-lara/stainless;

· EmmeliBlomkvist opened on Mar 4, 2026

Capture of this.v is too restrictive when v is a field of a mutable class this

Status: Open.

#1706 In epfl-lara/stainless;

· samuelchassot opened on Feb 18, 2026

Missed ghost usage outside of ghost context

Status: Open.

#1697 In epfl-lara/stainless;

· samuelchassot opened on Jan 8, 2026