[CatarinaGamboa]

Problem

When Found says nothing about the variable that Expected constrains, the counterexample leaves that variable out. It shows values for unrelated path conditions instead:

Refinement Error: !(port < 0 || port > 65535) is not a subtype of timeout >= 0
 --> Counterexample: port == 0

The value that breaks the call (timeout == -1) is in the SMT model, but it gets filtered out. In the OpenNMS study exercise the panel shows #fresh³¹⁶ == false && port³¹³ == 0, which points the reader at the port guard.

Cause

RefinementError.filterCounterexample kept only assignments to the binders of the simplified Found. That rule is wrong in three ways:

1. It drops what Expected constrains. A variable Found only knows as true loses its binder during simplification, so its value goes too (timeout, and also size(bag) for ghosts).
2. It drops variables Found does mention. A variable whose binder was simplified away can still appear in a path condition.
3. It keeps noise. It keeps any surviving binder, even one nothing displayed mentions (a generated path binder). It keeps path conditions unrelated to Expected. It keeps raw Z3 array values (l == ((as const (Array Int Int)) 4)).

Fix

The counterexample exists to show values that make Expected false under Found.

What is kept

• The terms of Expected. These are its variables and its ghost applications over variables (size(bag), length(a)), named as the SMT model names them.
• The terms of every Found fact linked to them, directly or through other facts. A fact is a conjunct of Found. Negated disjunctions are split (!(a || b) gives !a and !b), and double negations are dropped. So one combined guard !(port < 0 || … || timeout > 60000) links only timeout > 60000 to timeout, not every variable in the guard. A fact that shares no term with Expected only constrains values that cannot affect it, so it is left out.
• Not values Found already states. An x == v fact is compared structurally. Enum constants match the model's value (Format.JPG in Found, JPG in the model), and so do ghost applications with several arguments.
• Nothing when Found fixes every value Expected depends on. There is no fallback to other terms: int value = 0; if (port > 0) take(value); against _ > 1 shows no counterexample rather than port == 1. This is the same rule that already gives literal arguments no counterexample (ErrorLiteralZero). A path condition is shown only when it is linked to Expected, e.g. return port + 1; under port < 0 shows #ret == 0 && port == -1.
• Never array values. Only Z3 can read them. TranslatorToZ3 now skips array-sorted model values, as it already skipped uninterpreted sorts. Their ghosts (length(a)) remain.

Order, most relevant first:

1. Terms of Expected that Found says nothing about.
2. The other terms of Expected.
3. The linked terms, in the order the variables were introduced (the binder order of the VC chain before simplification).
4. Generated #fresh names last.

Display. VariableFormatter.format formats ghost application arguments (size(#s_3) becomes size(s³)). It uses a scanner that only splits top-level commas, so f(g(#a_1, #b_2), #c_3) becomes f(g(a¹, b²), c³). The CLI uses this, and so does the VS Code server's CounterexampleDTO. The fresh-name prefix now lives in Formats.FRESH_PREFIX, shared with VCBinderSimplification.

Behaviour changes in existing outputs

Sweep of main against this PR over 149 Error* testSuite entries, 25 ErrorCounterexample* fixtures and 97 study exercises (257 entries, main at 19991d36): 70 outputs change.

• 21 change order only. The same values come back, with Expected's values (often #ret) now first and #fresh last:
  • fixtures: ErrorAfterIf, ErrorAssignmentBeforeReturn, ErrorBitwiseUnknownOperand, ErrorBoolean, ErrorCharLiteralComparisons, ErrorDeferredCallbackState, ErrorDependentUpperBound, ErrorEmptyLoopBody, ErrorFieldOfOtherObject, ErrorIdentity, ErrorIntegerDivision, ErrorOperatorAssignments, ErrorRecursion, ErrorRecursiveDecrement, ErrorRecursiveSiblingParameter, ErrorUnknownMethodInOperation
  • exercises: E_A2_03, E_A2_07, E_A2_08, E_A2_10, E_OSS_A2_05
  • For example, x == 1 && #ret² == 0 becomes #ret² == 0 && x == 1. The 7 affected TestCounterexamples assertions are updated.
  • Of these, five fixtures reorder because #fresh now goes last: ErrorBitwiseUnknownOperand, ErrorFieldOfOtherObject, ErrorNullLiterals, ErrorUnknownMethodInOperation and ErrorCounterexampleCallArgument. The first version of this PR body did not say so.
• 49 change content. These are the new fixtures, plus:
  • values Expected needs that were missing: ErrorUnconstrainedRefinement, ErrorUnknownArgument, ErrorUnresolvedOperationValue, ErrorEnumConstantInCondition, E_OSS_A1_05, E_OSS_A2_04
  • unlinked path values dropped: ErrorLoopCondition, ErrorInstanceof, ErrorUnknownMethodInComparison, E_A2_02, E_OSS_A2_01, plus counterexamples made only of an opaque #fresh value that Expected does not depend on: ErrorNullLiterals (two of its errors; the others only reorder), ErrorUnresolvedBinaryOperator, ErrorUnresolvedFieldDeclaringType, ErrorUnresolvedUnaryOperator
  • known enum values no longer repeated: ErrorEnumFunctionRefinement, ErrorEnumNegation, ErrorLocalShadowsConstant, and the first error of ErrorEnumConstantInCondition
  • array values replaced by length(…), or dropped when the length is known: ErrorSearchIntArray, ErrorImplementationSearchValueIntArray, ErrorSearchValueIntArray, ErrorStringArrayLength, ErrorLenZeroIntArray
  • ErrorEnumNull, which is a known limitation (see below)

Relation to #299 and #459

• Show counterexample values in the final expected refinement #299 substitutes the filtered counterexample into the final Expected. With this change it has the value it needs: the reproducer would show With witness: -1 >= 0 ✗ (checked earlier with a trial merge). It conflicts textually with this PR:
  • In RefinementError, both add imports, and Show counterexample values in the final expected refinement #299 inserts substituteWitness right above the comment this PR rewrites. Keep both sides.
  • In TestCounterexamples, Show counterexample values in the final expected refinement #299 extends dependentUpperBound…, which this PR renames and reorders. Keep Show counterexample values in the final expected refinement #299's extra assertions on the renamed test.
• Drop true binders the error does not need and write fields as in code #459 merges cleanly in VariableFormatter, VariableFormatterTest and VCBinderSimplification. The application formatting is one early branch plus private methods at the end of the class, with no new imports. Its TestFoundBinders has 3 assertions that pin the old order (a == 0 && this.amount == 0, count == 0 && Basket.served == -1, y == 0 && x == -1). Whichever PR lands second flips those three to Expected-first; nothing else changes (checked with a trial merge).

Tests

25 testSuite fixtures (ErrorCounterexample*.java, each with // Expect: Refinement Error) plus matching TestCounterexamples cases that assert the exact assignments:

Fixture	main	this PR
UnconstrainedArgument (issue reproducer)	port == 0	timeout == -1
CombinedGuard (if (port<0 || … || window<1 || timeout>60000) return;)	port == 0 && retries == 0 && backoff == 0 && window == 1	timeout == -1
MixedGuard (port<0 || (retries>3 && backoff>10) || timeout>60000)	port == 0 && retries == 0	timeout == -1
GuardRelatesArguments (retries > timeout + 5)	port == 0 && retries == 0	timeout == -1 && retries == 0
NothingKnown (Found is true)	(none)	millis == -1
GuardedArgument	port == 0	timeout == -1
AliasedArgument	configured, port, timeout¹¹	timeout¹¹ == -1 && configured == -1
FieldArgument	this#…timeout, port, timeout⁶	timeout⁶ == -1 && this#…timeout == -1
CallArgument (connect(read(key) - 1))	#fresh⁶, port, timeout⁷	timeout⁷ == -1 && #fresh⁶ == 0
BranchArgument (nested if/else)	secure == false && #fresh⁰ == false && port == 1025	timeout == -1
SeveralArguments	port == 0 && lo == 1	hi == 0 && lo == 1
KnownArgument	port == 0	capacity == 0
LinkedPathCondition (connect(port - 1))	port, retries, timeout¹⁰	timeout¹⁰ == -1 && port == 0
ReturnPath	configured, port, #ret⁵	#ret⁵ == -1 && configured == -1
ReturnConstant (return 0 under port < 0)	port == -1	(none): Found fixes #ret == 0
ReturnFromPath (return port + 1 under port < 0)	port == -1 && #ret² == 0	#ret² == 0 && port == -1
KnownGuardedArgument (int value = 0; if (port > 0) take(value);)	port == 1	(none)
KnownTwiceGuardedArgument (same, under two guards)	port == 1 && retries == 0	(none)
KnownAliasedArgument (int base = 0; int value = base;)	port == 1	(none)
RefinementAlias	port == 0	timeout == -1
GhostArgument	port == 0	size(bag) == 0
KnownGhost (Found states size(s⁹) == 1)	port == 0	(none)
KnownEnum (format == Format.JPG)	(none)	(none); format == JPG stays hidden
ArrayArgument (get(a, 3))	port == 0	length(a) == 0
ArrayIndex (int[] a = new int[4]; get(a, k))	port == 0 && a⁵ == ((as const (Array Int Int)) 4)	k == -1

15 unit tests in RefinementErrorCounterexampleTest. Each builds a RefinementError from a VC chain and a hand-written model. They cover:

• an Expected variable that simplification dropped
• unlinked facts
• equality chains
• unmentioned path binders
• generated names ordered last
• known values, known enum values, and known ghosts with several arguments (and the unknown case)
• splitting negated disjunctions, nested conjunctions and double negations
• a guard that relates Expected to another variable
• no counterexample when Found fixes every linked value, even with a path condition, and a path condition Expected's value is computed from

VariableFormatterTest also covers nested applications.

The review fixtures fail on the commit before them: CombinedGuard, MixedGuard, GuardRelatesArguments, KnownEnum, ArrayArgument and ArrayIndex on 491d297e; KnownGuardedArgument, KnownTwiceGuardedArgument and KnownAliasedArgument on 9e037b6b, which showed port == 1. So do their unit tests. Four tests guard behaviour that should not change and pass on both: ReturnFromPath, keepsAPathConditionTheExpectedValueIsComputedFrom, hasNoCounterexampleWhenFoundStatesEveryValue and keepsGhostValuesWithSeveralArgumentsFoundSaysNothingAbout.

mvn test (verifier): 599 tests, 0 failures, 0 errors (534 on main).

CLI before / after

Issue reproducer:

Refinement Error: !(port < 0 || port > 65535) is not a subtype of timeout >= 0
- --> Counterexample: port == 0
+ --> Counterexample: timeout == -1

OpenNMS study exercise (E_OSS_A2_04_VmwareCimProbe):

- --> Counterexample: #fresh³¹⁶ == false && port³¹³ == 0
+ --> Counterexample: timeout == -1

Combined guard:

Refinement Error: !(port < 0 || port > 65535 || retries < 0 || backoff < 0 || window < 1 || timeout > 60000) is not a subtype of timeout >= 0
- --> Counterexample: port == 0 && retries == 0 && backoff == 0 && window == 1
+ --> Counterexample: timeout == -1

Array index:

Refinement Error: !(port < 0) && length(a⁵) == 4 is not a subtype of k >= 0 && k < length(a⁵)
- --> Counterexample: port == 0 && a⁵ == ((as const (Array Int Int)) 4)
+ --> Counterexample: k == -1

Ghost state:

Refinement Error: !(port < 0) is not a subtype of size(bag) > 0
- --> Counterexample: port == 0
+ --> Counterexample: size(bag) == 0

Known enum value (ErrorEnumFunctionRefinement):

Refinement Error: newColor¹¹ == Blue is not a subtype of newColor¹¹ == Color.Red || newColor¹¹ == Color.Green
- --> Counterexample: newColor¹¹ == Blue
+ (no counterexample: Found already states it)

Left out, and why

• ErrorEnumNull (Color c = null) now shows c³ == Blue. Found is true because the verifier does not model null for enums; the assignment is lost before the error is built. Blue is a real counterexample to what Found states, but not the value the program has. Hiding values whenever Found is true would also hide millis == -1 in the issue's own case. The fix belongs in how null enum assignments are translated, which is a separate issue.
• Typestate parameters (@Refinement("open(f)")): RefinementError receives Expected before states are expanded, while the model names the state ghost state1(#f_6). Here Found already states that ghost (closed(f⁶) is state1 == 0), so nothing new would be shown even after expansion, and state1(f⁶) == 0 would be harder to read than the state name. With nothing new to show, there is no counterexample (main showed the unrelated port == 0). Showing values in state names needs the state mapping in the error, which this PR does not add.
• No counterexample, rather than the known value, when Found fixes Expected. Repeating value == 0 would only restate Found, and it is the rule ErrorLiteralZero and ErrorStaticFinalConstant already pin. The cost is ten(port) with return 0; under port < 0 (ReturnConstant): main showed port == -1, which says which return failed. The VC cannot tell that case apart from take(value) under port > 0, where port == 1 misleads. In both, a guard is unlinked to an Expected term that Found fixes. When the return value is computed from the path (return port + 1;), the path value is linked and shown.
• Ghost applications whose arguments are not plain variables (size(old(this))) are not matched. The model names them by Z3's rendering of the argument.
• !(x != v) is not rewritten to x == v. Hiding that value would hide the breaking value itself (t == -3 against t >= 0).
• Declaring a ghost class as a nested static class makes Z3 fail with Sort mismatch … supplied sort is …$Bag. This is an unrelated, existing bug, so the ghost fixtures use top-level classes.

Fixes #453

🤖 Generated with Claude Code

[CatarinaGamboa]

[Codex review] The fallback still produces a counterexample that points at the wrong value when Found already states the value that violates Expected. Reproducer: take(@Refinement("_ > 1") int value), then int value = 0; if (port > 0) take(value);. On this head the error says port > 0 && value == 0 is not a subtype of value > 1, but the counterexample is only port == 1. In filterCounterexample, isKnown removes value == 0; the linked assignment list becomes empty, and the fallback selects an unrelated Found term. This recreates the distracting-path-value problem the PR aims to fix. When Found already explains the failing Expected term, please omit the counterexample or display that known value explicitly; reserve a path-context fallback for a case where the path value actually explains the violation. The focused counterexample tests passed, but none covers this shape.

[CatarinaGamboa]

[Claude] Fixed in 712759f: the fallback is gone. The counterexample now keeps only the values linked to Expected that Found does not already state. So when Found fixes every value Expected depends on, there is no counterexample. Your reproducer now shows none instead of port == 1. That is the same rule ErrorLiteralZero already pins: we don't repeat a known value. A path condition is still shown when Expected's value is computed from it: return port + 1; under port < 0 gives #ret == 0 && port == -1.

Covered by:

• TestCounterexamples, negative: argumentFoundAlreadyStatesHasNoCounterexampleUnderAGuard (your reproducer), …UnderTwoGuards, argumentKnownThroughAnAliasHasNoCounterexampleUnderAGuard, returnedConstantFoundAlreadyStatesHasNoCounterexample, ghostValueFoundAlreadyStatesIsOmittedWithTheUnrelatedPathCondition
• TestCounterexamples, positive: returnComputedFromThePathConditionShowsBoth
• RefinementErrorCounterexampleTest: omitsThePathConditionWhenFoundStatesEveryLinkedValue and keepsAPathConditionTheExpectedValueIsComputedFrom

The trade-off for return 0; under a guard is noted in the PR body.

[CatarinaGamboa]

[Codex re-review] Resolved. The fallback is removed, and the new tests cover the guarded argument case, aliases, multiple guards, and return values computed from path conditions. The PR’s CI is green. My port == 1 reproducer now correctly yields no counterexample when Found already fixes the expected value.