Search results

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

Option-less extractors result in "Lookup failure" exceptions

Status: Open.

#1696 In epfl-lara/stainless;

· Ant-28 opened on Jan 5, 2026

Make Multiplication Overflow Check More Efficient

Status: Open.

#1693 In epfl-lara/stainless;

· vkuncak opened on Dec 21, 2025

@extern functions are mistakenly verified in some cases

bug

Status: Open.

#1689 In epfl-lara/stainless;

· vkuncak opened on Dec 17, 2025

WIP ghost elimination bug

Status: Open.

#1687 In epfl-lara/stainless;

· samuelchassot opened on Dec 16, 2025

Handle all default getters that have ignored types in Extraction

Status: Open.

#1685 In epfl-lara/stainless;

· samuelchassot opened on Dec 12, 2025

Error when running a particular example with extended trait

Status: Open.

#1684 In epfl-lara/stainless;

· samuelchassot opened on Dec 12, 2025