Issues

• Namespace and argument with the same names cause shadowing issues when extracting precondition

  cryspen/aeneas#61 · Filter by author abentkamp opened on Aug 31, 2026
  1

• Call to a super-trait function is extracted with the wrong number of arguments

  bugspecs
  cryspen/aeneas#60 · Filter by author abentkamp opened on Aug 31, 2026
  1

  

• Multiple closures in requires/ensures cause mathlib linter warning

  cryspen/aeneas#59 · Filter by author abentkamp opened on Aug 31, 2026
  4

• Ord::min/max return the wrong argument on ties

  cryspen/aeneas#53 · Filter by author karthikbhargavan opened on Aug 22, 2026
  1

  

• Signed Step::backward_checked rejects crossing zero

  cryspen/aeneas#52 · Filter by author karthikbhargavan opened on Aug 22, 2026
  1

  

• Vec::insert overwrites the element at i instead of shifting

  cryspen/aeneas#51 · Filter by author karthikbhargavan opened on Aug 22, 2026
  2

  

• Crash: a closure that reads through a captured &mut aborts translation (SymbolicToPureValues.ml:366)

  cryspen/aeneas#40 · Filter by author karthikbhargavan opened on Aug 9, 2026

• Crash: two assert! of the same boolean aborts translation ("no bottoms in the value")

  cryspen/aeneas#28 · Filter by author karthikbhargavan opened on Jul 26, 2026
  2

  

• Inverted can_end guard in eliminate_shared_loans mutates frozen abstractions; valid programs rejected

  cryspen/aeneas#24 · Filter by author karthikbhargavan opened on Jul 25, 2026

• Latent scope escape in simplify_let_branching: hoisted outputs not filtered against branch-local binders

  cryspen/aeneas#23 · Filter by author karthikbhargavan opened on Jul 25, 2026

• Crash: returning a borrowed value from inside a loop aborts whole-crate translation (reorder_loop_outputs)

  cryspen/aeneas#22 · Filter by author karthikbhargavan opened on Jul 25, 2026

• Cleanup the hax-step backend

  cryspen/aeneas#14 · Filter by author clementblaudeau opened on Jul 1, 2026

• Upstream Result.holds

  cryspen/aeneas#11 · Filter by author clementblaudeau opened on Jun 30, 2026