[CatarinaGamboa]

Summary

Carry the expanded expected predicate used by the SMT check into refinement errors. Substitute every displayed counterexample value that can safely be parsed as a literal, using expression variable identities. Preserve the original expected predicate and counterexample assignments.

For an alias mismatch, the verifier can now show:

Refinement Error: ... is not a subtype of Positive(buffered)
Final expected: buffered > 0
Counterexample: buffered == 0
With witness: 0 > 0 ✗

The CLI error displays the final expected predicate and witness. RefinementError also exposes both as predicates for a future server DTO and VS Code presentation change. Verification results are unchanged.

Closes #296.

Verification

• Full verifier test suite passed: 340 tests, zero failures.
• Focused tests cover alias expansion, multiple assignments, repeated variables, negative values, unsafe values left unchanged, and a real verifier counterexample.
• git diff --check passed.

Integration note

The current VS Code server DTO does not serialize these new fields, so they will not appear in the extension until a separate server/client update consumes them.

[rcosta358]

A while back I thought about adding a simplification pass specifically for expected types that could also be applied to counterexamples, and I think that would address this issue in a better way.

This simplification would expand aliases and static final constants, for example:

• ∀x. true => x == Byte.MAX_VALUE → ∀x. true => x == 127
• ∀x. x == -1 => Positive(x) → ∀x. x == -1 => x > 0 → -1 > 0

Then we could have navigate the simplification history just like we are doing for the found types.
What do you think?

[CatarinaGamboa]

Yeah we could extend the simplification here, but also do the substitution of values with the counter-examples in the expected type

[rcosta358]

Yes, I also had thought about that possibility. We can plug them in the expected type and then perform the same simplification to see how they make the expected type false.

[rcosta358]

gitar fix

[gitar-bot]

💡 Edge Case: Witness parsing only catches SyntaxError; other parse failures escape

substituteWitness now runs raw Z3 model values through RefinementsParser.createAST, but it only catches SyntaxError. The parser can throw other unchecked exceptions. For example, literalCreate calls Long.parseLong on any INT token, and a Z3 Int model value outside the long range (Z3 integers are unbounded) throws NumberFormatException. NotImplementedException and other LJError subclasses can also escape. Any of these would escape the RefinementError constructor, so the verifier would crash with a runtime exception instead of reporting the refinement error. The witness is best-effort decoration, so a failure to parse one value should skip it the same way a syntax error does.

Treat any parse failure of an SMT value as non-representable:

try {
    Expression value = RefinementsParser.createAST(assignment.second(), "");
    if (!isLiteralValue(value))
        continue;
    expression = expression.substitute(new Var(assignment.first()), value);
    substituted = true;
} catch (RuntimeException ignored) {
    // Some SMT values cannot be represented in the refinement language.
}

• Apply fix

_{Check the box to apply the fix or reply for a change | Was this helpful? React with 👍 / 👎}

[gitar-bot]

gitar fix

On it — I'm adding constant-folding for the substituted witness values (e.g. 0 > 0 → false) so fully-substituted counterexamples display a resolved true/false instead of the raw unevaluated comparison. This is scoped to the witness display added in this PR; the broader alias/constant-expansion simplification pass you two discussed is a bigger change I'll leave for a follow-up.

[gitar-bot]

Code Review 👍 Approved with suggestions 0 closed / 1 findings

🟡 Medium risk · Adds expanded predicates and literal witness substitution to verifier errors.

Adds counterexample witness values to refinement errors by expanding the expected predicate and substituting Z3 model values into the witness expression. The feature improves error diagnostics and exposes both predicates for future server/client updates.

Consider broadening the exception handling in substituteWitness to catch NumberFormatException, NotImplementedException, and other unchecked exceptions beyond SyntaxError, so parsing failures gracefully skip individual witness values rather than crashing the verifier.

💡 Edge Case: Witness parsing only catches SyntaxError; other parse failures escape

📄 liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java:114-122

substituteWitness now runs raw Z3 model values through RefinementsParser.createAST, but it only catches SyntaxError. The parser can throw other unchecked exceptions. For example, literalCreate calls Long.parseLong on any INT token, and a Z3 Int model value outside the long range (Z3 integers are unbounded) throws NumberFormatException. NotImplementedException and other LJError subclasses can also escape. Any of these would escape the RefinementError constructor, so the verifier would crash with a runtime exception instead of reporting the refinement error. The witness is best-effort decoration, so a failure to parse one value should skip it the same way a syntax error does.

Treat any parse failure of an SMT value as non-representable

try {
    Expression value = RefinementsParser.createAST(assignment.second(), "");
    if (!isLiteralValue(value))
        continue;
    expression = expression.substitute(new Var(assignment.first()), value);
    substituted = true;
} catch (RuntimeException ignored) {
    // Some SMT values cannot be represented in the refinement language.
}

🤖 Prompt for agents

Code Review: Adds counterexample witness values to refinement errors by expanding the expected predicate and substituting Z3 model values into the witness expression. The feature improves error diagnostics and exposes both predicates for future server/client updates.
  
  Consider broadening the exception handling in `substituteWitness` to catch `NumberFormatException`, `NotImplementedException`, and other unchecked exceptions beyond `SyntaxError`, so parsing failures gracefully skip individual witness values rather than crashing the verifier.

1. 💡 Edge Case: Witness parsing only catches SyntaxError; other parse failures escape
   Files: liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java:114-122

   `substituteWitness` now runs raw Z3 model values through `RefinementsParser.createAST`, but it only catches `SyntaxError`. The parser can throw other unchecked exceptions. For example, `literalCreate` calls `Long.parseLong` on any `INT` token, and a Z3 `Int` model value outside the long range (Z3 integers are unbounded) throws `NumberFormatException`. `NotImplementedException` and other `LJError` subclasses can also escape. Any of these would escape the `RefinementError` constructor, so the verifier would crash with a runtime exception instead of reporting the refinement error. The witness is best-effort decoration, so a failure to parse one value should skip it the same way a syntax error does.

   Fix (Treat any parse failure of an SMT value as non-representable):
   try {
       Expression value = RefinementsParser.createAST(assignment.second(), "");
       if (!isLiteralValue(value))
           continue;
       expression = expression.substitute(new Var(assignment.first()), value);
       substituted = true;
   } catch (RuntimeException ignored) {
       // Some SMT values cannot be represented in the refinement language.
   }

Review coverage

📋 Rules No rules evaluated

🧪 Functional validation Not enabled · Set up

Options

Auto-apply is off → Gitar will not commit updates to this branch.
Display: compact → Counting what did not apply, without listing it.

Comment with these commands to change the behavior for this request:

Auto-apply	Compact
gitar auto-apply:on	gitar display:verbose

_{Was this helpful? React with 👍 / 👎 | Gitar}