Verifier crashes when a method call is an operand of a comparison or boolean operator

[CatarinaGamboa]

Description

Any if (or expression) that compares the result of a call to a method without refinements crashes the whole verification with a RuntimeException, even in a program with no refinements at all. if (s.equals(x)) on its own works; if (s.length() < 3), a.equals(x) || a.equals(y) and for (...; b < buf.getNumBanks(); ...) all crash.

Minimal reproducer (no refinements needed)

public class Repro {
    public static void main(String[] args) {
        String s = "abc";
        if (s.length() < 3) {
            System.out.println("short");
        }
    }
}

Expected

Correct! Passed Verification. A method we know nothing about should just give an unconstrained value (true), not stop verification.

Actual

Error while checking CtIfImpl
  on if (s.length() < 3) {
  with Cannot invoke "liquidjava.processor.context.RefinedFunction.getRenamedRefinements(liquidjava.processor.context.Context, spoon.reflect.declaration.CtElement)" because "fi" is null

Reproduced on main at 8816186 (liquidjava-verifier 0.0.35), and on 0.0.33.

Context

Found while turning real open-source Java code into study examples for the error-message study: real code hits this constantly, so the examples have to be rewritten around it or cannot be verified. This is the most common crash we met: it blocks or forces a rewrite in 6 of 12 examples.