diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 95a92df1317a3ace5d32b53f0d3bfcff977c67c8..50ac77db4de99b5ee6b5acfee5eebb33950dc800 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -186,7 +186,11 @@ public class BAstCreator extends BuiltInOPs
 					DebugUtils.printVeryVerboseMsg("Not creating B DEFINITION (in Override Table) " + def.getName() + " " + def);
 					continue;
 				}
-				if (def.getOriginallyDefinedInModuleNode().getName().toString().equals("MC")) {
+				if (def.getOriginallyDefinedInModuleNode().getName().toString().equals("MC")
+						&& !specAnalyser.getUsedDefinitions().contains(def)) {
+					// don't skip MC definitions if they are used
+					// TODO: check if this is correct (see invariant check for MC below)
+					DebugUtils.printDebugMsg("Skipping MC definition: " + def.getName());
 					continue;
 				}
 				//debugUtils.printVeryVerboseMsg("Creating B DEFINITION " + def.getName() + " " + def);