Show counterexample values in the final expected refinement - #299

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.
   }