diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedRefinement.java
new file mode 100644
index 00000000..251c22bc
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedRefinement.java
@@ -0,0 +1,12 @@
+package testSuite;
+
+import liquidjava.specification.Refinement;
+
+public class ErrorUnconstrainedRefinement {
+
+    private static void requirePositive(@Refinement("_ > 0") int value) {}
+
+    public static void check(int value) {
+        requirePositive(value); // Refinement Error
+    }
+}
diff --git a/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedStateRefinement.java b/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedStateRefinement.java
new file mode 100644
index 00000000..3fb4e0dc
--- /dev/null
+++ b/liquidjava-example/src/main/java/testSuite/ErrorUnconstrainedStateRefinement.java
@@ -0,0 +1,15 @@
+package testSuite;
+
+import liquidjava.specification.Ghost;
+import liquidjava.specification.StateRefinement;
+
+@Ghost("boolean ready")
+public class ErrorUnconstrainedStateRefinement {
+
+    @StateRefinement(from = "ready(this)")
+    public void run() {}
+
+    public static void check(ErrorUnconstrainedStateRefinement value) {
+        value.run(); // State Refinement Error
+    }
+}
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java
index 01a3d2ce..ae6b3b37 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/LJDiagnostic.java
@@ -16,6 +16,7 @@ public class LJDiagnostic extends RuntimeException {
     private String file;
     private SourcePosition position;
     private String hint;
+    private String counterexample;
     private static final String PIPE = " | ";
 
     public LJDiagnostic(String title, String message, SourcePosition pos, String accentColor, String customMessage) {
@@ -43,6 +44,10 @@ public String getHint() {
         return hint;
     }
 
+    public String getCounterexampleStr() {
+        return counterexample;
+    }
+
     public SourcePosition getPosition() {
         return position;
     }
@@ -70,6 +75,10 @@ public void setHint(String hint) {
         this.hint = hint;
     }
 
+    public void setCounterexampleStr(String counterexample) {
+        this.counterexample = counterexample;
+    }
+
     @Override
     public String toString() {
         StringBuilder sb = new StringBuilder();
@@ -84,6 +93,12 @@ public String toString() {
             sb.append(snippet);
         }
 
+        // counterexample
+        String counterexample = getCounterexampleStr();
+        if (counterexample != null && !counterexample.isBlank()) {
+            sb.append(" --> ").append(String.join("\n     ", counterexample.split("\n"))).append("\n");
+        }
+
         // hint
         String hint = getHint();
         if (hint != null && !hint.isBlank()) {
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
index e048b08c..61bf4a98 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/RefinementError.java
@@ -13,6 +13,8 @@
 import liquidjava.utils.Pair;
 import spoon.reflect.cu.SourcePosition;
 
+import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
+
 /**
  * Error indicating that a refinement constraint either was violated or cannot be proven
  * 
@@ -37,6 +39,14 @@ public RefinementError(SourcePosition position, SourcePosition declarationPositi
         this.found = found;
         this.counterexample = filterCounterexample(counterexample);
         this.declarationPosition = declarationPosition;
+        if (!this.counterexample.isEmpty()) {
+            String counterexampleString = this.counterexample.assignments().stream()
+                    .map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
+                    .collect(Collectors.joining(" && "));
+            setCounterexampleStr("Counterexample: " + counterexampleString);
+        }
+        if (isTrue(found.getImplication().toPredicate().getExpression()))
+            setHint("Not enough information to prove the expected refinement. Add a refinement or condition to constrain it.");
     }
 
     @Override
@@ -44,17 +54,6 @@ public SourcePosition getDeclarationPosition() {
         return declarationPosition;
     }
 
-    @Override
-    public String getHint() {
-        if (counterexample.isEmpty())
-            return null;
-
-        String counterexampleString = counterexample.assignments().stream()
-                .map(a -> VariableFormatter.format(a.first()) + " == " + a.second())
-                .collect(Collectors.joining(" && "));
-        return "Counterexample: " + counterexampleString;
-    }
-
     public Counterexample getCounterexample() {
         return counterexample;
     }
diff --git a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
index e4bb8a41..fbb661c5 100644
--- a/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
+++ b/liquidjava-verifier/src/main/java/liquidjava/diagnostics/errors/StateRefinementError.java
@@ -1,5 +1,7 @@
 package liquidjava.diagnostics.errors;
 
+import static liquidjava.rj_language.opt.VCSimplificationUtils.isTrue;
+
 import liquidjava.diagnostics.TranslationTable;
 import liquidjava.processor.VCImplication;
 import liquidjava.rj_language.Predicate;
@@ -27,6 +29,8 @@ public StateRefinementError(SourcePosition position, SourcePosition declarationP
         this.declarationPosition = declarationPosition;
         this.expected = expected;
         this.found = found;
+        if (isTrue(found.getImplication().toPredicate().getExpression()))
+            setHint("No state information is known for this object. Make sure its state is initialized and available at this point.");
     }
 
     @Override