diff --git a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
index 61609f6aebcfe0822a25e1faef5c16b453e219ba..c1ba55cab7eb98d59f641812bbe7b15c1ef1f525 100644
--- a/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
+++ b/src/main/java/de/tla2b/translation/UsedDefinitionsFinder.java
@@ -5,6 +5,7 @@ import de.tla2b.analysis.AbstractASTVisitor;
 import de.tla2b.analysis.SpecAnalyser;
 import de.tla2b.global.BBuiltInOPs;
 import de.tla2b.global.TranslationGlobals;
+import de.tla2b.util.DebugUtils;
 import tla2sany.semantic.ASTConstants;
 import tla2sany.semantic.ModuleNode;
 import tla2sany.semantic.OpApplNode;
@@ -60,7 +61,9 @@ public class UsedDefinitionsFinder extends AbstractASTVisitor implements ASTCons
 		for (OpDefNode opDef : specAnalyser.getModuleNode().getOpDefs()) {
 			String defName = opDef.getName().toString();
 			// GOAL, ANIMATION_FUNCTION, ANIMATION_IMGxx, SET_PREF_xxx, etc.
+			// DebugUtils.printDebugMsg("Checking definition: " + defName);
 			if (Utils.isProBSpecialDefinitionName(defName)) {
+			    DebugUtils.printMsg("ProB special definition: " + defName);
 				usedDefinitions.add(opDef);
 			}
 		}
diff --git a/src/main/java/de/tla2b/util/DebugUtils.java b/src/main/java/de/tla2b/util/DebugUtils.java
index 4818ecf5804e576597217f43915b26d4cfd4505a..7f78432aa55219c4aafffb5352d0b0dade532833 100644
--- a/src/main/java/de/tla2b/util/DebugUtils.java
+++ b/src/main/java/de/tla2b/util/DebugUtils.java
@@ -7,6 +7,11 @@ public class DebugUtils {
 		debugOn = newDebugOn;
 	}
 
+	public static void printVeryVerboseMsg(String Msg) {
+	    // TODO: turn on using -vv flag
+		// System.out.println(Msg);
+	}
+
 	public static void printDebugMsg(String Msg) {
 		if(debugOn) {
 		   System.out.println(Msg);
diff --git a/src/main/java/de/tla2bAst/BAstCreator.java b/src/main/java/de/tla2bAst/BAstCreator.java
index 9346e3a3824d5115cc27263d293f6ec5915eebd5..f1edcd5a1ade77560e3e6ffcb099db3d976406d2 100644
--- a/src/main/java/de/tla2bAst/BAstCreator.java
+++ b/src/main/java/de/tla2bAst/BAstCreator.java
@@ -14,6 +14,7 @@ import de.tla2b.global.*;
 import de.tla2b.translation.BMacroHandler;
 import de.tla2b.translation.RecursiveFunctionHandler;
 import de.tla2b.types.*;
+import de.tla2b.util.DebugUtils;
 import tla2sany.semantic.*;
 import tla2sany.st.Location;
 import tlc2.tool.BuiltInOPs;
@@ -178,13 +179,17 @@ public class BAstCreator extends BuiltInOPs
 			OpDefNode def = moduleNode.getOpDefs()[i];
 			if (specAnalyser.getBDefinitions().contains(def)) {
 				if (conEval != null && conEval.getConstantOverrideTable().containsValue(def)) {
+			        DebugUtils.printVeryVerboseMsg("Not creating B DEFINITION (in Override Table) " + def.getName() + " " + def);
 					continue;
 				}
 				if (def.getOriginallyDefinedInModuleNode().getName().toString().equals("MC")) {
 					continue;
 				}
+			    //debugUtils.printVeryVerboseMsg("Creating B DEFINITION " + def.getName() + " " + def);
 
 				bDefs.add(def);
+			} else {
+			    DebugUtils.printVeryVerboseMsg("Not creating unused B DEFINITION for " + def.getName() + " " + def);
 			}
 
 		}