diff --git a/tlatools/src/tlc2/output/OutputCollector.java b/tlatools/src/tlc2/output/OutputCollector.java
index 4c237f703cdcaa7d1c9c09dc3ab96b7243a5acf6..93b5eb6e36cf0b16227d0ee80eeb2f4047bc4d86 100644
--- a/tlatools/src/tlc2/output/OutputCollector.java
+++ b/tlatools/src/tlc2/output/OutputCollector.java
@@ -4,6 +4,7 @@ import java.util.ArrayList;
 import java.util.Date;
 import java.util.Hashtable;
 
+import tla2sany.semantic.ModuleNode;
 import tla2sany.semantic.SemanticNode;
 import tla2sany.st.Location;
 import tlc2.module.TLC;
@@ -14,12 +15,11 @@ 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 Action nextPred = null;
-	public static Hashtable<Location, Long> lineCount= new Hashtable<Location, Long>();
+	public static ModuleNode moduleNode = null;
+	public static Hashtable<Location, Long> lineCount = null;
 	
 	public static ArrayList<TLCStateInfo> getTrace() {
 		return trace;
diff --git a/tlatools/src/tlc2/tool/AbstractChecker.java b/tlatools/src/tlc2/tool/AbstractChecker.java
index 7d9ac8dad0d55111b46fd65f3bfc16ee932553f4..1c8d430dc1927622099cf72f2515546544c9b815 100644
--- a/tlatools/src/tlc2/tool/AbstractChecker.java
+++ b/tlatools/src/tlc2/tool/AbstractChecker.java
@@ -154,6 +154,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;
             Hashtable<String, Location> locationTable = new Hashtable<String, Location>();
             for (int i = 0; i < workers.length; i++)
             {
@@ -169,11 +170,15 @@ 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) });
-                OutputCollector.lineCount.put(locationTable.get(skeys[i]), val);
+                Location location = locationTable.get(skeys[i]);
+                if(location != null){
+                    OutputCollector.lineCount.put(location, val);
+                }
             }
             MP.printMessage(EC.TLC_COVERAGE_END);
         }
diff --git a/tlatools/src/tlc2/tool/Spec.java b/tlatools/src/tlc2/tool/Spec.java
index 48b1f0f4e905b30df213abe055a40e0d0883a4bd..1094f2586c269d9947ab6c304b36071706ae412d 100644
--- a/tlatools/src/tlc2/tool/Spec.java
+++ b/tlatools/src/tlc2/tool/Spec.java
@@ -42,7 +42,6 @@ import tla2sany.semantic.ThmOrAssumpDefNode;
 import tlc2.TLCGlobals;
 import tlc2.output.EC;
 import tlc2.output.MP;
-import tlc2.output.OutputCollector;
 import tlc2.util.Context;
 import tlc2.util.List;
 import tlc2.util.ObjLongTable;
@@ -916,7 +915,6 @@ public class Spec implements ValueConstants, ToolGlobals, Serializable
                 Assert.fail(EC.TLC_CONFIG_ID_REQUIRES_NO_ARG, new String[] { "next state action", name });
             }
             this.nextPred = new Action(def.getBody(), Context.Empty);
-            OutputCollector.nextPred = this.nextPred;
         }
     }