diff --git a/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java b/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java
index 1da3693b1965cd83b49aeb8aa1d3f8fe0dc13434..3cde356c1e94d0d0c6764fd248cffe5bcc8cdd7f 100644
--- a/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java
+++ b/de.prob.ui/src/de/prob/ui/eventb/ModelCheckingFinishedListener.java
@@ -134,8 +134,9 @@ public class ModelCheckingFinishedListener extends JobChangeAdapter {
 		StringBuffer sb = new StringBuffer();
 		sb.append("Invariant violation found.\n");
 		sb.append("ProB has detected a state that violates the invariant.\n");
-		sb.append("The following is the trace that led to the violation:\n");
-		appendTrace(trace, sb);
+		// no longer show trace of state ids to user; not very useful 
+		//sb.append("The following is the trace that led to the violation:\n");
+		//appendTrace(trace, sb);
 		return sb.toString();
 	}