Treat instanceof as an unknown boolean (#359)

Fixes #335.

## Problem
`instanceof` has no counterpart in the refinement language, so
`getOperatorFromKind` returned null for it and any `if (o instanceof
String)` crashed with `Cannot invoke "String.hashCode()" because
"<local1>" is null`, even in a file without refinements.

## Change
`OperationsChecker` treats `instanceof` the way it already treats
comparisons with `null`: the result is a fresh, unconstrained boolean
(`isUntranslatable` covers both, in the binary-operator and the
assignment paths). Both branches stay reachable, so nothing is assumed
from the test.

## Tests
- `CorrectInstanceof`: `instanceof` in an `if`, bound to a boolean local
and combined with `&&`, and negated inside `||`. Crashed on main, now
passes.
- `ErrorInstanceof`: a refinement violation inside an `instanceof`
branch is reported (crashed on main).
- Pattern matching (`o instanceof String s && !s.isEmpty()`) also
verifies.
- `mvn test` passes.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-authored-by: Claude Opus 5.5 <noreply@anthropic.com>

Author: CatarinaGamboa

liquidjava-example/src/main/java/testSuite/CorrectInstanceof.java

@@ -0,0 +1,28 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class CorrectInstanceof {
+
+    static int positive(@Refinement("_ > 0") int x) {
+        return x;
+    }
+
+    static String describe(Object o) {
+        if (o instanceof String) {
+            return "text";
+        }
+        return "other";
+    }
+
+    static int size(Object o, @Refinement("_ > 0") int n) {
+        boolean isText = o instanceof String;
+        if (isText && n > 1) {
+            return positive(n - 1);
+        }
+        if (!(o instanceof Integer) || n > 3) {
+            return positive(n);
+        }
+        return positive(n + 1);
+    }
+}

liquidjava-example/src/main/java/testSuite/ErrorInstanceof.java

@@ -0,0 +1,17 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorInstanceof {
+
+    static int positive(@Refinement("_ > 0") int x) {
+        return x;
+    }
+
+    static int size(Object o, @Refinement("_ >= 0") int n) {
+        if (o instanceof String) {
+            return positive(n); // Expect: Refinement Error
+        }
+        return 1;
+    }
+}

liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/general_checkers/OperationsChecker.java

@@ -82,8 +82,8 @@ public <T> void getBinaryOpRefinements(CtBinaryOperator<T> operator) throws LJEr
                 && ((CtAssignment<?, ?>) parent).getAssigned()instanceof CtVariableWrite<?> parentVar) {
             oper = getOperationRefinements(operator, parentVar, operator);
 
-        } else if (hasNullOperand(operator)) {
-            oper = createFreshValue(operator, new Predicate()); // null comparisons are not supported yet: unknown value
+        } else if (isUntranslatable(operator)) {
+            oper = createFreshValue(operator, new Predicate()); // null comparisons and instanceof: unknown value
         } else if (operatorFor(operator) == null) {
             oper = untranslatableOperation(operator);
         } else {
@@ -245,7 +245,7 @@ private Predicate getOperationRefinements(CtBinaryOperator<?> operator, CtVariab
             rtc.getContext().addVarToContext(elemName, elemVar.getType(), e, elemVar);
             return Predicate.createVar(returnName);
         } else if (element instanceof CtBinaryOperator<?> binop) {
-            if (hasNullOperand(binop)) // null comparisons are not supported yet: unknown boolean value
+            if (isUntranslatable(binop)) // null comparisons and instanceof: unknown boolean value
                 return createFreshValue(binop, new Predicate());
             if (operatorFor(binop) == null)
                 return untranslatableOperation(binop);
@@ -336,6 +336,11 @@ private Predicate getOperationRefinementFromExternalLib(CtInvocation<?> inv) thr
         return getUnconstrainedInvocationVariable(inv);
     }
 
+    /** Null comparisons are not supported yet, and the logic has no types to test {@code instanceof} against. */
+    private static boolean isUntranslatable(CtBinaryOperator<?> binop) {
+        return binop.getKind() == BinaryOperatorKind.INSTANCEOF || hasNullOperand(binop);
+    }
+
     private static boolean hasNullOperand(CtBinaryOperator<?> binop) {
         return isNullLiteral(binop.getLeftHandOperand()) || isNullLiteral(binop.getRightHandOperand());
     }