Issues

Writing a field of a class declared later in the file crashes verification
liquid-java/liquidjava#308 · opened on Sep 30, 2026
static final field plus a refinement gives a spurious "Invalid ghost declaration"
liquid-java/liquidjava#307 · opened on Sep 30, 2026
while loop condition is not assumed inside the loop body
liquid-java/liquidjava#306 · opened on Sep 30, 2026
1
Constant accessed through a subclass gives "Sorts Int and Bool are incompatible"
liquid-java/liquidjava#305 · opened on Sep 30, 2026
Soundness: if/else-if assignment followed by a guard hides a state violation
liquid-java/liquidjava#304 · opened on Sep 30, 2026
Soundness: an int passed to a float refined parameter is not checked
liquid-java/liquidjava#303 · opened on Sep 30, 2026
Verifier crashes when an enum (or class) constant is compared in an if
liquid-java/liquidjava#302 · opened on Sep 30, 2026
null literals are rejected, so any null check stops verification
liquid-java/liquidjava#301 · opened on Sep 30, 2026
Verifier crashes when a method call is an operand of a comparison or boolean operator
liquid-java/liquidjava#300 · opened on Sep 30, 2026
Link state errors to the operation that established the relevant state
liquid-java/liquidjava#298 · opened on Sep 24, 2026
Add an expected-guided simplification step to state error derivations
liquid-java/liquidjava#297 · opened on Sep 24, 2026
Show counterexample values in the final expected refinement
liquid-java/liquidjava#296 · opened on Sep 24, 2026
Restore alias expansion in refinement diagnostic history
liquid-java/liquidjava#295 · opened on Sep 24, 2026
Add a flag -a to show all verification conditions sent to the smt solver
liquid-java/liquidjava#240 · opened on Jun 2, 2026
State Names Displayed with Internal Identifiers
liquid-java/liquidjava#206 · opened on May 1, 2026
Change return to $result for method return values in refinements
liquid-java/liquidjava#133 · opened on Dec 10, 2025
3
Change instance variable numbers for line numbers instead of counter
liquid-java/liquidjava#132 · opened on Dec 10, 2025
2
State checking for extending abstract classes
liquid-java/liquidjava#131 · opened on Dec 10, 2025
Add Support for Additional Types in Refinements
liquid-java/liquidjava#91 · opened on Nov 6, 2025
Refinement Aliases don't work with Interfaces
liquid-java/liquidjava#50 · opened on Jul 29, 2025
2
Ghost variables are not correctly initialized in interfaces
liquid-java/liquidjava#44 · opened on Jul 4, 2025
1
Support LinkedList<@Refined(“x>0”) Integer>
liquid-java/liquidjava#41 · opened on Apr 22, 2025
1
State Names should be able to start with UpperCase
liquid-java/liquidjava#25 · opened on May 2, 2023
Separating logging information from other function arguments
liquid-java/liquidjava#13 · opened on Oct 13, 2022
2
This should not typecheck, but it typechecks
liquid-java/liquidjava#11 · opened on Oct 13, 2022