Issues

Issues

• Program incorrectly rejected

  liquid-java/liquidjava#536 · opened on Nov 12, 2026

• Killed verifier JVMs leave ~30 MB of Z3 native libraries in /tmp

  liquid-java/liquidjava#535 · opened on Nov 11, 2026

• False error: a boolean query (_ == true --> open(this)) in a class fails at its return

  liquid-java/liquidjava#509 · opened on Nov 9, 2026

• Frame equalities: a to that uses a named set's function (phase(this) == phase(other)) still gets the frame

  liquid-java/liquidjava#506 · opened on Nov 9, 2026

• False error: state sets declared two levels up the hierarchy are not kept across a call

  liquid-java/liquidjava#505 · opened on Nov 9, 2026

• Soundness: a to that sets another object's state drops the receiver's frame (x.observe(y) forgets x's state)

  liquid-java/liquidjava#504 · opened on Nov 9, 2026

• Write a state as a value of its set: phase(this) == open

  liquid-java/liquidjava#502 · opened on Nov 9, 2026
  7

• Found: rewrite facts through ghost equalities g(x) == g(x@k) so they are stated about x

  liquid-java/liquidjava#501 · opened on Nov 6, 2026
  6

• False error: a switch case on a library enum (e.g. DayOfWeek) does not know its label (Found shows #MONDAY_value)

  liquid-java/liquidjava#500 · opened on Nov 6, 2026

• False error: a break nested inside a switch case forgets that path's state (Found shows true)

  liquid-java/liquidjava#499 · opened on Nov 6, 2026

• Alias arguments are substituted one at a time: Below(b, a) is expanded as a < a, giving a false "can never be true" warning

  liquid-java/liquidjava#491 · opened on Nov 5, 2026

• A for loop over indices forgets the list's ghost, so i < l.size() does not prove l.get(i)

  liquid-java/liquidjava#479 · opened on Nov 4, 2026

• Variable 'this' could not be found when a ghost-refined method is called on another call's result

  liquid-java/liquidjava#478 · opened on Nov 4, 2026

• Counterexample: a guard stored in a boolean (boolean bad = a || b || c; if (bad) return;) is not split, so every variable of the guard is listed

  liquid-java/liquidjava#471 · opened on Nov 3, 2026

• False error: an anonymous subclass (new Anon() {}) does not get the state of the constructor it calls

  liquid-java/liquidjava#470 · opened on Nov 3, 2026

• False error: @StateSet on a nested class gives "Argument Mismatch Error: ... expected Inner, got Inner"

  liquid-java/liquidjava#469 · opened on Nov 3, 2026

• False error: @StateSet on an enum is ignored, so its states give "Ghost 'Mode.off' could not be found"

  liquid-java/liquidjava#468 · opened on Nov 3, 2026

• Crash: @Ghost on a nested class gives "Sort mismatch ... supplied sort is Outer$Bag"

  liquid-java/liquidjava#467 · opened on Nov 3, 2026

• Spec predicates cannot mention null: "Variable 'null' could not be found"

  liquid-java/liquidjava#466 · opened on Nov 2, 2026

• False error: in main, an early return on the args array makes a later state-refined call report "Variable 'args' could not be found"

  liquid-java/liquidjava#465 · opened on Nov 2, 2026

• No state hints when an overload with the same arity hides an inherited refinement

  liquid-java/liquidjava#463 · opened on Nov 2, 2026

• Crash when an override has fewer state refinements than the method it overrides

  liquid-java/liquidjava#462 · opened on Nov 2, 2026

• An external spec cannot use its superclass spec's states unless the superclass spec is read first

  liquid-java/liquidjava#461 · opened on Nov 2, 2026

• False error in external specs: a @Ghost the constructor does not set gives "Ghost 'old' could not be found" at the next from-only call

  liquid-java/liquidjava#450 · opened on Oct 29, 2026

• False error: @StateRefinement(from = "false") gives "State Conflict Error: Found multiple disjoint states"

  liquid-java/liquidjava#449 · opened on Oct 29, 2026