Treat null literals as carrying no information instead of failing

[CatarinaGamboa]

Null literals (x = null, x == null, x != null, f(null)) no longer raise Null literals are not supported and stop verification of the rest of the file.
In OperationsChecker, a null literal now yields new Predicate() (true), like String literals already do, and a binary operation with a null operand also yields true (otherwise e.g. name == null became name == true and failed with a Z3 sort mismatch). No null reasoning is added.

Fixes #301

Testing:

• New CorrectNullLiterals.java: null-initialised local, == null / != null in if, null passed to an unrefined method, the X s = null; try { ... } finally { if (s != null) ... } shape, plus an unrelated int refinement that still verifies.
• Manually checked that a failing refinement inside an if (name == null) branch is still reported as a Refinement Error.
• mvn test: 339 tests, 0 failures (existing ErrorEnumNull still fails as expected).

🤖 Generated with Claude Code

[CatarinaGamboa]

Review: there was a soundness bug. A null comparison was modelled as the constant true, so its negation was false:

• in if (s == null || y > 0) {...} else {...} the else branch was treated as dead, so a violation inside it was never reported;
• in if (s != null && y > 0) ... else the else path gained the false fact y <= 0;
• (o == null) ? -1 : 1 was treated as always -1, and boolean b = o == null as always true.

All of these passed verification on 5bf4604.

Fix (cedbdec): a comparison with null now becomes a fresh unconstrained boolean variable (reusing createFreshValue(..., new Predicate())), both at the top level and when nested inside &&/||. The other operands keep their facts, e.g. s == null && y > 0 still gives y > 0 in the then-branch.

Tests:

• new ErrorNullLiterals.java with 5 expected Refinement Errors: else of ==, else of ||, else of &&, ternary, boolean local. Only 1 of the 5 was reported before the fix.
• CorrectNullLiterals.java extended with a && case and a ternary case.
• mvn test: 340 tests, 0 failures.

🤖 Generated with Claude Code

[rcosta358]

LGTM