Add soundness-hole test: int negative modulo

Verifier proves _ >= 0 for (-7) % 3, but Java yields -1. Root: makeMod uses Euclidean Z3 mkMod (TranslatorToZ3.java:344); Java % follows the sign of the dividend.

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

Author: GUIpsp

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

@@ -0,0 +1,18 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: integer `%` is translated to Z3's Euclidean modulo (result always >= 0),
+// but Java `%` takes the sign of the dividend. -7 % 3 == -1 in Java; the verifier models it as 2
+// and ACCEPTS "_ >= 0". At runtime -1 >= 0 is false. Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorNegativeModuloUnsound {
+    public static void main(String[] args) {
+        @Refinement("a == -7")
+        int a = -7;
+        @Refinement("_ >= 0")
+        int r = a % 3; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because r == -1
+        assert r >= 0 : "r=" + r;
+    }
+}