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..0383d34e10e6b46f64490993d6d10fc00bb0bc8a 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();
 	}
 
@@ -143,24 +144,25 @@ public class ModelCheckingFinishedListener extends JobChangeAdapter {
 		StringBuffer sb = new StringBuffer();
 		sb.append("Theorem violation found.\n");
 		sb.append("ProB has detected a state that violates the theorems.\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();
 	}
 
 	private String createStateErrorResult(final List<String> trace) {
 		StringBuffer sb = new StringBuffer();
 		sb.append("ProB has detected an erroneous state (e.g., witness error, guard strengthening error).\n");
-		sb.append("The following is the trace that led to the error:\n");
-		appendTrace(trace, sb);
+		//sb.append("The following is the trace that led to the error:\n");
+		//appendTrace(trace, sb);
 		return sb.toString();
 	}
 
 	private String createWDErrorResult(final List<String> trace) {
 		StringBuffer sb = new StringBuffer();
 		sb.append("ProB has detected a state which caused a well-definedness error(e.g., division by zero).\n");
-		sb.append("The following is the trace that led to the error:\n");
-		appendTrace(trace, sb);
+		//sb.append("The following is the trace that led to the error:\n");
+		//appendTrace(trace, sb);
 		return sb.toString();
 	}
 
@@ -168,8 +170,8 @@ public class ModelCheckingFinishedListener extends JobChangeAdapter {
 		StringBuffer sb = new StringBuffer();
 		sb.append("ProB has detected a state which caused an internal error.\n");
 		sb.append("This is probably a bug (please report).\n");
-		sb.append("The following is the trace that led to the error:\n");
-		appendTrace(trace, sb);
+		//sb.append("The following is the trace that led to the error:\n");
+		//appendTrace(trace, sb);
 		return sb.toString();
 	}
 
@@ -177,8 +179,8 @@ public class ModelCheckingFinishedListener extends JobChangeAdapter {
 		StringBuffer sb = new StringBuffer();
 		sb.append("Deadlock found.\n");
 		sb.append("ProB has detected a state where all guards are false.\n");
-		sb.append("The following is the trace that led to the deadlock:\n");
-		appendTrace(trace, sb);
+		//sb.append("The following is the trace that led to the deadlock:\n");
+		//appendTrace(trace, sb);
 		return sb.toString();
 	}