diff --git a/tlatools/src/tlc2/output/OutputCollector.java b/tlatools/src/tlc2/output/OutputCollector.java
index 93b5eb6e36cf0b16227d0ee80eeb2f4047bc4d86..00636aaca758b44508cc02c1a2dde7f83a5bd2bb 100644
--- a/tlatools/src/tlc2/output/OutputCollector.java
+++ b/tlatools/src/tlc2/output/OutputCollector.java
@@ -4,23 +4,21 @@ import java.util.ArrayList;
 import java.util.Date;
 import java.util.Hashtable;
 
+import tla2sany.semantic.ExprNode;
 import tla2sany.semantic.ModuleNode;
-import tla2sany.semantic.SemanticNode;
 import tla2sany.st.Location;
-import tlc2.module.TLC;
-import tlc2.tool.Action;
 import tlc2.tool.TLCState;
 import tlc2.tool.TLCStateInfo;
-import tlc2.util.ObjLongTable;
 
 public class OutputCollector {
 
 	private static TLCState initialState = null;
 	private static ArrayList<TLCStateInfo> trace = null;
 	private static ArrayList<Message> allMessages = new ArrayList<Message>();
-	public static ModuleNode moduleNode = null;
-	public static Hashtable<Location, Long> lineCount = null;
-	
+	private static Hashtable<Location, Long> lineCount = new Hashtable<Location, Long>();
+	private static ModuleNode moduleNode = null;
+	private static ExprNode violatedAssumption = null;
+
 	public static ArrayList<TLCStateInfo> getTrace() {
 		return trace;
 	}
@@ -28,26 +26,34 @@ public class OutputCollector {
 	public static void setTrace(ArrayList<TLCStateInfo> trace) {
 		OutputCollector.trace = trace;
 	}
-	
-	public static void addStateToTrace(TLCStateInfo tlcStateInfo){
-		if(trace == null){
+
+	public static void addStateToTrace(TLCStateInfo tlcStateInfo) {
+		if (trace == null) {
 			trace = new ArrayList<TLCStateInfo>();
 		}
 		trace.add(tlcStateInfo);
 	}
 
-	public static void setInitialState(TLCState initialState){
+	public static void setInitialState(TLCState initialState) {
 		OutputCollector.initialState = initialState;
 	}
-	
-	public static TLCState getInitialState(){
+
+	public static TLCState getInitialState() {
 		return OutputCollector.initialState;
 	}
-	
+
 	public static ArrayList<Message> getAllMessages() {
 		return allMessages;
 	}
 
+	public static void setViolatedAssumption(ExprNode assumption) {
+		violatedAssumption = assumption;
+	}
+
+	public static ExprNode getViolatedAssumption() {
+		return violatedAssumption;
+	}
+
 	public synchronized static void saveMessage(int messageClass,
 			int messageCode, String[] parameters) {
 
@@ -55,4 +61,20 @@ public class OutputCollector {
 				new Date());
 		allMessages.add(m);
 	}
+
+	public static ModuleNode getModuleNode() {
+		return moduleNode;
+	}
+
+	public static void setModuleNode(ModuleNode moduleNode) {
+		OutputCollector.moduleNode = moduleNode;
+	}
+
+	public static Hashtable<Location, Long> getLineCountTable() {
+		return new Hashtable<Location, Long>(lineCount);
+	}
+
+	public static void putLineCount(Location location, long val) {
+		lineCount.put(location, val);
+	}
 }
diff --git a/tlatools/src/tlc2/tool/AbstractChecker.java b/tlatools/src/tlc2/tool/AbstractChecker.java
index f1efc827caf3d3aa512360177dbb3cf970df4b70..7ba4caea0207d961d797c682c1ec44380db506f1 100644
--- a/tlatools/src/tlc2/tool/AbstractChecker.java
+++ b/tlatools/src/tlc2/tool/AbstractChecker.java
@@ -77,10 +77,12 @@ public abstract class AbstractChecker implements Cancelable
         specFile = specFile.substring(lastSep + 1);
 
         this.tool = new Tool(specDir, specFile, configFile, resolver);
-
+        
         this.specObj = this.tool.init(preprocess, spec);
         this.checkLiveness = !this.tool.livenessIsTrue();
 
+        OutputCollector.setModuleNode(this.tool.rootModule);
+        
         // moved to file utilities
         this.metadir = FileUtil.makeMetaDir(specDir, fromChkpt);
         
@@ -154,7 +156,7 @@ public abstract class AbstractChecker implements Cancelable
             MP.printMessage(EC.TLC_COVERAGE_START);
             // First collecting all counts from all workers:
             ObjLongTable counts = this.tool.getPrimedLocs();
-            OutputCollector.moduleNode = this.tool.rootModule;
+            OutputCollector.setModuleNode(this.tool.rootModule);
             Hashtable<String, Location> locationTable = new Hashtable<String, Location>();
             for (int i = 0; i < workers.length; i++)
             {
@@ -170,14 +172,13 @@ public abstract class AbstractChecker implements Cancelable
             }
             // Reporting:
             Object[] skeys = counts.sortStringKeys();
-            OutputCollector.lineCount = new Hashtable<Location, Long>();
             for (int i = 0; i < skeys.length; i++)
             {
                 long val = counts.get(skeys[i]);
                 //MP.printMessage(EC.TLC_COVERAGE_VALUE, new String[] { skeys[i].toString(), String.valueOf(val) });
                 Location location = locationTable.get(skeys[i]);
                 if(location != null){
-                    OutputCollector.lineCount.put(location, val);
+                    OutputCollector.putLineCount(location, val);
                 }
             }
             MP.printMessage(EC.TLC_COVERAGE_END);
diff --git a/tlatools/src/tlc2/tool/ModelChecker.java b/tlatools/src/tlc2/tool/ModelChecker.java
index 39948af7d4f4118b367a8c00be4c71c3295361ec..84b950e13eea76035faaf68b52607951da35f969 100644
--- a/tlatools/src/tlc2/tool/ModelChecker.java
+++ b/tlatools/src/tlc2/tool/ModelChecker.java
@@ -273,6 +273,7 @@ public class ModelChecker extends AbstractChecker
             {
                 if ((!isAxiom[i]) && !this.tool.isValid(assumps[i]))
                 {
+                	OutputCollector.setViolatedAssumption(assumps[i]);
                     MP.printError(EC.TLC_ASSUMPTION_FALSE, assumps[i].toString());
                     return false;
                 }