GeezerVison

Pull requests

• Read old(this) in a precondition as the state before the call

  #422·CatarinaGamboa opened Oct 24, 2026Collaborator·

  ·
  1

• Support .length on array expressions and spread varargs calls

  #400·CatarinaGamboa opened Oct 13, 2026Collaborator·

  ·
  3

  2

• See state changes through aliases and forget mutable field initializers across methods

  #393·CatarinaGamboa opened Oct 13, 2026Collaborator·

  ·
  2

• Reject stale refinements after short-circuit RHS writes

  #324·CatarinaGamboa opened Oct 2, 2026Collaborator·3 of 7 tasks·

  ·
  1

• Show counterexample values in the final expected refinement

  #299·CatarinaGamboa opened Sep 24, 2026Collaborator·

  ·
  1

  7

• Change instance variable numbers for line numbers instead of counter. Refs #132

  #271·maartinss opened Jul 9, 2026·

  ·
  1

  2

• Add -a/--all flag to show all SMT verification conditions

  #243·CatarinaGamboa opened Jun 2, 2026Collaborator·2 of 7 tasks·

  ·
  1

  3

• Derive Developer Facing States

  #220·rcosta358 opened May 13, 2026Collaborator·2 of 7 tasks·

  ·
  1

  7

• Add #result for Return Refinements

  #145·rajshivu opened Feb 9, 2026·

  ·
  1

  26

• Add Null Support

  #143·rcosta358 opened Feb 7, 2026Collaborator·

  ·
  13

• Increase test coverage

  #118·CatarinaGamboa opened Nov 13, 2025Collaborator·

  ·
  7