Add soundness-hole test: long division truncation

Verifier proves _ > 3 for 7L / 2L, but Java truncates to 3. Root: long is modeled as a Z3 Real (TranslatorContextToZ3.java:96; makeLongLiteral :106), so division is exact and rational (makeDiv:336).

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

Author: GUIpsp

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

@@ -0,0 +1,20 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+// SOUNDNESS HOLE: Java `long` is modeled as a Z3 Real, so `/` becomes exact rational
+// division instead of truncating integer division. 7L / 2L == 3 in Java, but the verifier
+// models it as 3.5 and ACCEPTS "_ > 3". At runtime 3 > 3 is false. Should be rejected.
+@SuppressWarnings("unused")
+public class ErrorLongAsRealDivisionUnsound {
+    public static void main(String[] args) {
+        @Refinement("c == 7")
+        long c = 7L;
+        @Refinement("d == 2")
+        long d = 2L;
+        @Refinement("_ > 3")
+        long e = c / d; // Refinement Error
+        // runtime check mirrors the refinement; aborts under -ea because e == 3
+        assert e > 3 : "e=" + e;
+    }
+}