Verifier crashes on ++ or -- on a field of another object (c.count++) #436

Impact: verification stops with an internal error (crash) on ++/-- applied to a field of another object.

Description

c.count++ where c is an object of another class: OperationsChecker.getUnaryOpRefinements names the operand with Utils.qualifyFieldName, and getRefinementUnaryVariableWrite (OperationsChecker.java:500) looks that name up in the context, gets null, and calls substituteVariable on it. The same happens for c.count--, ++c.count, and c.count = -c.count (the NEG path at OperationsChecker.java:196). int k = -c.count, count++ / this.count++, and o.count++ with o of the current class do not crash. When the field has no tracked refinement, the operand could be treated as an unrefined value instead.

Minimal reproducer

class Counter {
    int count;
}

public class Repro {
    void inc(Counter c) {
        c.count++;
    }
}

Expected

Correct! Passed Verification.

Actual

Exception in thread "main" java.lang.RuntimeException: 
Error while checking CtMethodImpl
  on inc(Counter c) { 
  ...
Error while checking CtUnaryOperatorImpl
  on c.count++; 
  at .../Repro.java:7
  with Cannot invoke "liquidjava.rj_language.Predicate.substituteVariable(String, String)" because "metadada" is null
...
Caused by: java.lang.NullPointerException: Cannot invoke "liquidjava.rj_language.Predicate.substituteVariable(String, String)" because "metadada" is null
	at liquidjava.processor.refinement_checker.general_checkers.OperationsChecker.getRefinementUnaryVariableWrite(OperationsChecker.java:501)
	at liquidjava.processor.refinement_checker.general_checkers.OperationsChecker.getUnaryOpRefinements(OperationsChecker.java:183)
	at liquidjava.processor.refinement_checker.RefinementTypeChecker.visitCtUnaryOperator(RefinementTypeChecker.java:387)

The same crash happens when the field's class is not on the classpath (opts.sampleSize++ with Options missing).

Reproduced on main at 1a506fe (liquidjava-verifier 0.0.36).

Context

Found while reviewing #432. Related: #426 (plain assignment to a field of an unresolved class).

🤖 Generated with Claude Code