[CatarinaGamboa]

Closes #373.

What changed

Every value the verifier introduces used to be called #freshN, so path conditions, call results and new receivers all looked the same in Expected/Found and in counterexamples. The result of a call to a method with a contract was named #<method>_N, which was shown as getUndoManager⁵⁵⁵, like a program variable. Each one is now named after where it comes from:

Origin	Name shown
if condition	#if_condition¹¹
while/for condition (body and exit)	#loop_condition¹⁴
c ? a : b condition	#ternary_condition¹⁶
try/catch path (try ran / this catch ran)	#try_branch¹⁸, #catch_branch²¹
result of a call (with or without a contract, inside an expression, as an argument or as a receiver)	#read_result²⁸ (method name + _result)
value read from a field not tracked here (e.g. a.length, another object's field)	#length_value⁷ (field name + _value)
receiver of new T(..).m()	#new_Door³⁵
value of an operation that is not encoded (x == null, instanceof, bitwise ops)	#operation_result³⁰
size of new int[n]	#array_length⁴

The subclass-contract checks in AuxHierarchyRefinementsPassage also used #fresh for the return value and the receiver. They now use the existing #ret_N and #this_N names.

How it works: the new liquidjava.utils.GeneratedNames builds every such name as ##<description>_<counter>. The context counter keeps names unique. The second # keeps them apart from instances of program variables (#<variable>_<counter>), since a Java name can't start with #. Characters that the refinement language's ID token doesn't accept (e.g. $ in Map$Entry, non-ASCII letters in method names) are replaced by _, so the names still parse and work with the SMT encoding. GeneratedNames.isGenerated replaces the old #fresh_ prefix checks in three places: the counterexample ordering (RefinementError), unused path-binder removal (VCBinderSimplification) and keeping condition values in context (RefinementTypeChecker). Nothing else matched the old call-result name #<method>_N: the return-value checks in AuxStateHandler compare against the RETURN_VAR_NAME metadata, and the extension's translation table is keyed by whatever raw name the verifier sends. VariableFormatter removes one # as it does for instances, so generated names are shown with a single # (#if_condition¹¹), as #fresh was, and stay distinct from program variables.

Before / after

From the new fixture testSuite/classes/generated_names_error:

before: #fresh¹¹ == ready¹⁰ && #fresh¹¹ is not a subtype of a > 0
after:  #if_condition¹¹ == #ready_result¹⁰ && #if_condition¹¹ is not a subtype of a > 0

before: #fresh¹⁴ == ready¹² && #fresh¹⁴ == true is not a subtype of a > 0
after:  #loop_condition¹⁴ == #ready_result¹² && #loop_condition¹⁴ == true is not a subtype of a > 0

before: #fresh¹⁶ == ready¹⁵ && #fresh¹⁶ == true is not a subtype of a < 0
after:  #ternary_condition¹⁶ == #ready_result¹⁵ && #ternary_condition¹⁶ == true is not a subtype of a < 0

before: !#fresh¹⁸ && !#fresh²¹ is not a subtype of a²⁵ > 0
after:  !#try_branch¹⁸ && !#catch_branch²¹ is not a subtype of a²⁵ > 0

before: x²⁹ == #fresh²⁸ - 1 is not a subtype of x²⁹ > 0
after:  x²⁹ == #read_result²⁸ - 1 is not a subtype of x²⁹ > 0
        Counterexample: x²⁹ == 0 && #read_result²⁸ == 1

before: #fresh³² == #fresh³⁰ && #fresh³² && x³³ == 0 is not a subtype of x³³ > 0
after:  #if_condition³² == #operation_result³⁰ && #if_condition³² && x³³ == 0 is not a subtype of x³³ > 0

before: found closed(#fresh³⁵) but expected opened(#fresh³⁵)
after:  found closed(#new_Door³⁵) but expected opened(#new_Door³⁵)

Study exercises (exercises-oss, proposal C), run on main and on this branch:

E_OSS_A1_56_EditCommand.java:69 (JabRef)
before: found !#fresh⁵³⁷ && !(#fresh⁵⁵⁰ || #fresh⁵⁵¹) && undoManager⁵⁵⁷ == getUndoManager⁵⁵⁵ but expected redoable(undoManager⁵⁵⁷)
after:  found !#operation_result⁵³⁷ && !(#operation_result⁵⁵⁰ || #operation_result⁵⁵¹) && undoManager⁵⁵⁷ == #getUndoManager_result⁵⁵⁵ but expected redoable(undoManager⁵⁵⁷)

E_OSS_A1_19_AccessKeyGenerator.java:17
before: found dceSecurityNameRandom(randomUUID³⁸¹) but expected maybeTime(randomUUID³⁸¹) || timeBased(randomUUID³⁸¹)
after:  found dceSecurityNameRandom(#randomUUID_result³⁸¹) but expected maybeTime(#randomUUID_result³⁸¹) || timeBased(#randomUUID_result³⁸¹)

E_OSS_A2_04_VmwareCimProbe.java (OpenNMS)
before: !(#fresh¹²³⁷ || port¹²³¹ < 0 || port¹²³¹ > 65535) is not a subtype of timeout >= 0
after:  !(#operation_result¹²³⁷ || port¹²³¹ < 0 || port¹²³¹ > 65535) is not a subtype of timeout >= 0

Across the four study workspaces, only these generated names change in the messages; no error appears, disappears or moves.

The Found row in the issue's screenshot, ∀#fresh²²⁰ baseline²¹⁶ || extended²¹⁷, becomes ∀#if_condition²²⁰ baseline²¹⁶ || extended²¹⁷.

Tests

• New fixture liquidjava-example/src/main/java/testSuite/classes/generated_names_error/ (GeneratedNames.java, Door.java), one error for each origin that shows up in a message.
• New TestGeneratedNames: one test checking the exact message for each of those errors (counters stripped); it fails on any missing or extra error.
• Updated the expected names in VariableFormatterTest, VCBinderSimplificationTest, VCConstraintSimplificationTest, RefinementErrorCounterexampleTest and TestCounterexamples.
• Full suite run locally: 687 tests, 0 failures.

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

I found two issues and one test gap in the supplied diff. I did not run commands or tests.

• Generated names can be mistaken for program variables — GeneratedNames.java:31. The pattern also matches an instance of a user variable named read_result, if_condition, or new_Door. The formatter then displays that variable with a generated-name #, and counterexample sorting treats it as generated. Track generated names when creating them, or use a namespace that Formats.INSTANCE cannot produce. Add a test with a user variable named read_result.

• Array reads are missed — RefinementTypeChecker.java:287. An array read still creates #arrayAccess_N. GeneratedNames.isGenerated does not recognize it, so the formatter displays arrayAccessⁿ without the marker used for verifier-created values. Create the name through GeneratedNames and cover it in a diagnostic test.

• The integration test can hide extra errors — TestGeneratedNames.java:20. Putting errors in a map keyed only by line overwrites a second error on the same line, while the assertions never check the total error set. Assert the expected error count and retain all errors per position so unexpected diagnostics fail the test.

[CatarinaGamboa]

Round 1 responses:

1. Generated names can be mistaken for program variables: fixed in 36ef288. I confirmed it: #read_result_3 (an instance of a program variable called read_result) matched the pattern, so it was shown as #read_result³ and sorted as generated. Generated names now start with ##, e.g. ##if_condition_11. No instance name can start that way, because #<variable>_<counter> comes from a Java name and a Java name can't start with #. isGenerated is now a prefix check, and the kind-word pattern is gone. VariableFormatter keeps only the # that comes from the name, so the displayed names don't change (#if_condition¹¹), and #read_result_3 now shows as read_result³. Tests added: VariableFormatterTest (#size_result_4 shows as size_result⁴) and GeneratedNamesTest (#if_condition_3 and #read_result_3 are not generated).
2. Array reads are missed: declined. #arrayAccess_N was never a #fresh name, and it already shows as arrayAccessⁿ, which says what the value is. Changing it is outside Rename fresh to more useful name #373.
3. The integration test can hide extra errors: fixed in 36ef288. TestGeneratedNames now fails if two errors land on one line, and a new test (reportsOneErrorPerOrigin) checks the exact set of error lines. (TestExamples already checks the // Expect: count for the fixture.)

Full suite locally: 694 tests, 0 failures.

[CatarinaGamboa]

Codex review, round 2

I’ll review the supplied diff and source for behavior changes and gaps in the new naming tests. I’ll keep findings to issues I can tie to specific lines; I won’t run commands.
codex
I found no confirmed correctness bug in the supplied code. One test gap is worth addressing:

• RefinementTypeChecker.java: keepFreshValues now uses the ## prefix to retain generated values across nested branch scopes. The new tests check error text, but do not exercise a generated call result used by a joined variable after a nested if. Add a regression case that checks the refinement after that join, so a lost generated value cannot silently change verification results.

[CatarinaGamboa]

Round 2 response:

1. No regression test for keepFreshValues after a nested join: declined, because the case is already covered. ErrorNestedIfCallComparison.java and CorrectNestedIfCallComparison.java (added with keepFreshValues in Join an if on the instances its condition read #408) put a call result in a nested if condition that a joined variable uses after the join. To check that they really test this, I turned the GeneratedNames.isGenerated check in keepFreshValues off on this branch and ran them. ErrorNestedIfCallComparison then fails with Not Found Error: Variable '##current_result_14' could not be found, so TestExamples would catch it. I put the check back afterwards.

Codex found no correctness bugs this round, so I'm ending the review loop here. No code changes in this round.

[CatarinaGamboa]

Codex review, round 3

(Round 3 reviews 55fef6b, which renames the results of calls to methods with a contract.)

I found no actionable correctness bug or remaining dependency on the old #<method>_N form in the supplied diff and source files. Call results are named through GeneratedNames.valueOf, and the shown consumers use stored metadata or the generated-name prefix rather than reconstructing the old name.

I could not verify compilation or test results because commands were unavailable.

---

Codex had no findings this round, so nothing to fix or decline and the review loop ends here. It couldn't compile or run tests; locally the full suite passes at 55fef6b (687 tests, 0 failures).