Add Tests

rcosta358 · rcosta358 · commit 015524c7f7a7 · 2026-02-14T16:52:20.000Z
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinement.java
@@ -0,0 +1,12 @@
+// Unsatisfiable Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+@SuppressWarnings("unused")
+public class ErrorUnsatisfiableRefinement {
+    void test() {
+        @Refinement("_ > 0 && _ < 0")
+        int x = 5;
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinementParameter.java b/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinementParameter.java
@@ -0,0 +1,9 @@
+// Unsatisfiable Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorUnsatisfiableRefinementParameter {
+
+    void test(@Refinement("x == 0 && x == 1") int x) {}
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinementReturn.java b/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinementReturn.java
@@ -0,0 +1,11 @@
+// Unsatisfiable Refinement Error
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorUnsatisfiableRefinementReturn {
+    @Refinement("_ % 2 == 3")
+    int test() {
+        return 1;
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/UnsatisfiableRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/UnsatisfiableRefinementError.java
@@ -12,7 +12,7 @@ public class UnsatisfiableRefinementError extends LJError {
     private final String refinement;
 
     public UnsatisfiableRefinementError(SourcePosition position, String refinement) {
-        super("Unsatisfiable Refinement", "This predicate can never be true", position, null);
+        super("Unsatisfiable Refinement Error", "This predicate can never be true", position, null);
         this.refinement = refinement;
     }
 
diff --git a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
@@ -118,6 +118,8 @@ private void checkRefinementSatisfiability(Predicate predicate, CtElement elemen
                 SourcePosition pos = Utils.getAnnotationPosition(element, refinementString);
                 throw new UnsatisfiableRefinementError(pos, refinementString);
             }
+        } catch (UnsatisfiableRefinementError e) {
+            throw e;
         } catch (LJError e) {
             // ignore errors
         } finally {

Original file line number	Diff line number	Diff line change
`@@ -12,7 +12,7 @@ public class UnsatisfiableRefinementError extends LJError {`
`12`	`12`	`private final String refinement;`
`13`	`13`
`14`	`14`	`public UnsatisfiableRefinementError(SourcePosition position, String refinement) {`
`15`		`- super("Unsatisfiable Refinement", "This predicate can never be true", position, null);`
	`15`	`+ super("Unsatisfiable Refinement Error", "This predicate can never be true", position, null);`
`16`	`16`	`this.refinement = refinement;`
`17`	`17`	`}`
`18`	`18`
Original file line number	Diff line number	Diff line change
`@@ -118,6 +118,8 @@ private void checkRefinementSatisfiability(Predicate predicate, CtElement elemen`
`118`	`118`	`SourcePosition pos = Utils.getAnnotationPosition(element, refinementString);`
`119`	`119`	`throw new UnsatisfiableRefinementError(pos, refinementString);`
`120`	`120`	`}`
	`121`	`+ } catch (UnsatisfiableRefinementError e) {`
	`122`	`+ throw e;`
`121`	`123`	`} catch (LJError e) {`
`122`	`124`	`// ignore errors`
`123`	`125`	`} finally {`