diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorUnsatisfiableRefinement.java
new file mode 100644
index 00000000..9d8bda0b
--- /dev/null
+++ 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
new file mode 100644
index 00000000..b4ffed8a
--- /dev/null
+++ 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
new file mode 100644
index 00000000..022f1cf9
--- /dev/null
+++ 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
new file mode 100644
index 00000000..431a82ec
--- /dev/null
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/UnsatisfiableRefinementError.java
@@ -0,0 +1,22 @@
+package liquidjava.diagnostics.errors;
+
+import spoon.reflect.cu.SourcePosition;
+
+/**
+ * Error indicating that a refinement is intrinsically unsatisfiable (e.g., x > 0 && x < 0)
+ * 
+ * @see LJError
+ */
+public class UnsatisfiableRefinementError extends LJError {
+
+    private final String refinement;
+
+    public UnsatisfiableRefinementError(SourcePosition position, String refinement) {
+        super("Unsatisfiable Refinement Error", "This predicate can never be true", position, null);
+        this.refinement = refinement;
+    }
+
+    public String getRefinement() {
+        return 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
index 31c019bc..c9329f16 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/processor/refinement_checker/TypeChecker.java
@@ -28,6 +28,8 @@
 import spoon.reflect.declaration.CtClass;
 import spoon.reflect.declaration.CtElement;
 import spoon.reflect.declaration.CtInterface;
+import spoon.reflect.declaration.CtNamedElement;
+import spoon.reflect.declaration.CtTypedElement;
 import spoon.reflect.factory.Factory;
 import spoon.reflect.reference.CtTypeReference;
 import spoon.reflect.visitor.CtScanner;
@@ -85,11 +87,46 @@ public Optional<Predicate> getRefinementFromAnnotation(CtElement element) throws
                 throw new InvalidRefinementError(element.getPosition(),
                         "Refinement predicate must be a boolean expression", ref.get());
             }
+            checkRefinementSatisfiability(p, element, ref.get());
             constr = Optional.of(p);
         }
         return constr;
     }
 
+    private void checkRefinementSatisfiability(Predicate predicate, CtElement element, String refinementString)
+            throws LJError {
+
+        // skip if trivially true
+        if (predicate.isBooleanTrue())
+            return;
+
+        context.enterContext();
+        try {
+            // replace _ with variable name
+            String name = element instanceof CtNamedElement named ? named.getSimpleName() : Keys.WILDCARD;
+            Predicate refinement = predicate.clone().substituteVariable(Keys.WILDCARD, name);
+
+            // check if false is a subtype of the refinement (the refinement is unsatisfiable)
+            CtTypeReference<?> elementType = element instanceof CtTypedElement typedElement ? typedElement.getType()
+                    : null;
+            if (elementType != null)
+                context.addVarToContext(name, elementType, new Predicate(), element);
+
+            Predicate falsePred = Predicate.createLit("false", Types.BOOLEAN);
+            boolean isUnsatisfiable = vcChecker.smtChecks(falsePred, refinement, element.getPosition());
+            if (isUnsatisfiable) {
+                SourcePosition pos = Utils.getAnnotationPosition(element, refinementString);
+                throw new UnsatisfiableRefinementError(pos, refinementString);
+            }
+        } catch (UnsatisfiableRefinementError e) {
+            throw e;
+        } catch (LJError e) {
+            // ignore errors
+        } finally {
+            context.exitContext();
+        }
+    }
+
     @SuppressWarnings({ "rawtypes" })
     public Optional<String> getMessageFromAnnotation(CtElement element) {
         for (CtAnnotation<? extends Annotation> ann : element.getAnnotations()) {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java
index 1cf45bc7..1e99e3f0 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/utils/Utils.java
@@ -50,7 +50,6 @@ private static boolean isLiquidJavaAnnotation(CtAnnotation<?> annotation) {
 
     private static boolean hasRefinementValue(CtAnnotation<?> annotation, String refinement) {
         Map<String, ?> values = annotation.getValues();
-        return Stream.of("value", "to", "from")
-                .anyMatch(key -> refinement.equals(String.valueOf(values.get(key))));
+        return Stream.of("value", "to", "from").anyMatch(key -> refinement.equals(String.valueOf(values.get(key))));
     }
 }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java
index f3ae77f0..cca9c146 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/utils/constants/Formats.java
@@ -5,4 +5,5 @@ public final class Formats {
     public static final String INSTANCE = "#%s_%d";
     public static final String THIS = "this#%s";
     public static final String RET = "#ret_%d";
+    public static final String REF = "#ref_%d";
 }
\ No newline at end of file