[CatarinaGamboa]

Fixes #451

Cause. When a call argument carries no information (its refinement is just true, as for the result of a method without refinements), createVariableRepresentingArgument still wrapped it as arg == true. For an int argument Z3 rejects that with "Sorts Int and Bool are incompatible". For a boolean argument it silently assumed the value was true, so takeTrue(s.isEmpty()) against @Refinement("_ == true") was accepted. Now such an argument is left unconstrained, like any unknown value.

Study exercise A2_04, fixed with socket.connect(addr, Math.max(timeout, 0)) (no spec for Math.max):

Before:

Error: Sorts Int and Bool are incompatible
101 |             socket.connect(new InetSocketAddress(host, port), Math.max(timeout, 0));

After:

Refinement Error: expected Math.max(timeout, 0) >= 0 but could not prove it
101 |             socket.connect(new InetSocketAddress(host, port), Math.max(timeout, 0));
 --> Counterexample: Math.max(timeout, 0) == -1

The other A2_04 fixes (guard + return, guard + throw, ternary) still verify. With a Math.max spec (_ >= a && _ >= b && (_ == a || _ == b)) the Math.max fix verifies too. The issue's new Socket(addr, server.getLocalPort()) now reports expected server.getLocalPort() >= 0 && server.getLocalPort() <= 65535 but could not prove it.

Tests. Two cases added to ErrorUnknownMethodInOperation: an unknown int result and an unknown boolean result passed as arguments. Both fail on main (the first crashes, the second is accepted).

🤖 Generated with Claude Code

[CatarinaGamboa]

Codex review, round 1

• [P2] Preserve known-true boolean argument values: isBooleanTrue() also holds for an expression such as true && true, so takeTrue(true && true) against _ == true lost its value and was rejected.

Fixed in 54a6de7: the equality is now skipped only when the argument's refinement is exactly the literal true (the placeholder for "nothing known"). takeTrue(true && true) and takeTrue(true) verify again; full suite passes.

[CatarinaGamboa]

Codex review, round 2

No findings: "The change prevents an unknown argument refinement from being treated as the literal value true. The verifier test suite passes, including the new argument tests."