diff --git a/src/main/java/de/tlc4b/Translator.java b/src/main/java/de/tlc4b/Translator.java
index a8c3a6c041d4f608936f79d21cb0f33b1625ff08..9bc72461060ca297938970d54e2907db6db38395 100644
--- a/src/main/java/de/tlc4b/Translator.java
+++ b/src/main/java/de/tlc4b/Translator.java
@@ -44,7 +44,6 @@ public class Translator {
 	private PPredicate constantsSetup;
 	private Set<String> standardModulesToBeCreated;
 	private TLCOutputInfo tlcOutputInfo;
-	private String translatedLTLFormula;
 
 	public Translator(String machineString) throws BCompoundException {
 		this.machineString = machineString;
@@ -157,7 +156,6 @@ public class Translator {
 		printer.start();
 		moduleString = printer.getStringbuilder().toString();
 		configString = printer.getConfigString().toString();
-		translatedLTLFormula = printer.geTranslatedLTLFormula();
 
 		tlcOutputInfo = new TLCOutputInfo(machineContext, renamer, typechecker, generator.getTlaModule(),
 				generator.getConfigFile());
@@ -190,9 +188,4 @@ public class Translator {
 	public Set<String> getStandardModuleToBeCreated() {
 		return standardModulesToBeCreated;
 	}
-
-	public String getTranslatedLTLFormula() {
-		return translatedLTLFormula;
-	}
-
 }
diff --git a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
index 4d6505118bea0c9d6a44346ec9d50d3898bd343e..f0e8325489c6f2fcd83442d2b5aff96fe1aaafa3 100644
--- a/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
+++ b/src/main/java/de/tlc4b/prettyprint/TLAPrinter.java
@@ -58,8 +58,6 @@ public class TLAPrinter extends DepthFirstAdapter {
 	private final ConfigFile configFile;
 	private final PrimedNodesMarker primedNodesMarker;
 	private final Renamer renamer;
-	private boolean recordLTLFormula = false;
-	private final StringBuilder translatedLTLFormula = new StringBuilder();
 	private final InvariantPreservationAnalysis invariantPreservationAnalysis;
 
 	public TLAPrinter(MachineContext machineContext, Typechecker typechecker,
@@ -207,13 +205,7 @@ public class TLAPrinter extends DepthFirstAdapter {
 		if (TLC4BGlobals.isCheckLTL()) {
 			for (LTLFormulaVisitor visitor : visitors) {
 				moduleStringAppend(visitor.getName() + " == ");
-				if (TLC4BGlobals.getTestingMode()) {
-					recordLTLFormula = true;
-					visitor.printLTLFormula(this, typeRestrictor);
-					recordLTLFormula = false;
-				} else {
-					visitor.printLTLFormula(this, typeRestrictor);
-				}
+				visitor.printLTLFormula(this, typeRestrictor);
 				moduleStringAppend("\n");
 			}
 		}
@@ -287,9 +279,6 @@ public class TLAPrinter extends DepthFirstAdapter {
 
 	public void moduleStringAppend(String str) {
 		tlaModuleString.append(str);
-		if (recordLTLFormula) {
-			translatedLTLFormula.append(str);
-		}
 	}
 
 	private void printHeader() {
@@ -2970,10 +2959,6 @@ public class TLAPrinter extends DepthFirstAdapter {
 		moduleStringAppend("]");
 	}
 
-	public String geTranslatedLTLFormula() {
-		return this.translatedLTLFormula.toString();
-	}
-
 	public TLAModule getTLAModule() {
 		return this.tlaModule;
 	}
diff --git a/src/test/java/de/tlc4b/util/TestUtil.java b/src/test/java/de/tlc4b/util/TestUtil.java
index 4028da3ec65b08bca613174796415c16438ebe0b..a9b91d986266cc798ef7f437faac93f53380387e 100644
--- a/src/test/java/de/tlc4b/util/TestUtil.java
+++ b/src/test/java/de/tlc4b/util/TestUtil.java
@@ -10,6 +10,8 @@ import java.nio.file.FileSystems;
 import java.util.ArrayList;
 import java.util.Arrays;
 import java.util.List;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
 
 import de.be4.classicalb.core.parser.exceptions.BCompoundException;
 import de.tla2b.exceptions.TLA2BException;
@@ -21,9 +23,11 @@ import util.ToolIO;
 
 import static de.tlc4b.TLC4BOption.NOTRACE;
 import static org.junit.Assert.assertEquals;
+import static org.junit.Assert.assertTrue;
 
 public class TestUtil {
 	private static final String MCH_SUFFIX = ".mch";
+	private static final Pattern TRANSLATED_LTL_FORMULA_PATTERN = Pattern.compile("^ltl == (.*)$", Pattern.MULTILINE);
 
 	public static File[] getMachines(String path) {
 		return new File(path).listFiles((dir, name) -> name.endsWith(MCH_SUFFIX));
@@ -87,7 +91,21 @@ public class TestUtil {
 	public static void compareLTLFormula(String expected, String machine, String ltlFormula) throws BCompoundException {
 		Translator b2tlaTranslator = new Translator(machine, ltlFormula);
 		b2tlaTranslator.translate();
-		assertEquals(expected, b2tlaTranslator.getTranslatedLTLFormula());
+
+		// Extract the translated LTL formula from the complete TLA module.
+		Matcher matcher = TRANSLATED_LTL_FORMULA_PATTERN.matcher(b2tlaTranslator.getModuleString());
+		boolean matches = matcher.find();
+		String message = "Could not find LTL formula in translated TLA module";
+		if (!matches) {
+			// Debugging help: if the LTL formula couldn't be found,
+			// do an assertEquals with the module string (which will always fail)
+			// so that the entire module string appears in the JUnit output and in IDEs, test reports, etc.
+			assertEquals(message, expected, b2tlaTranslator.getModuleString());
+		}
+		assertTrue(message, matches);
+
+		String translatedLTLFormula = matcher.group(1);
+		assertEquals(expected, translatedLTLFormula);
 	}
 
 	public static void checkMachine(String machine) throws Exception {