Add soundness-hole test: int multiplication overflow

Verifier proves _ > 0 for int c = 46341 * 46341, but the product overflows int to -2147479015. Root: int is modeled as an unbounded Z3 Int (TranslatorContextToZ3.java:93; TranslatorToZ3.java:103,327).

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>

Author: GUIpsp

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

@@ -0,0 +1,17 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: Java `int` is modeled as an unbounded Z3 integer, so 32-bit
+// two's-complement overflow is not modeled. 46341 * 46341 == 2147488281 mathematically,
+// but in Java `int` it wraps to -2147479015. The verifier currently ACCEPTS "_ > 0";
+// at runtime the value is negative, so the refinement is violated. Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorIntOverflowUnsound {
+    public static void main(String[] args) {
+        @Refinement("_ > 0")
+        int c = 46341 * 46341; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because c == -2147479015
+        assert c > 0 : "c=" + c;
+    }
+}