diff --git a/tlatools/src/tlc2/tool/ConcurrentTLCTrace.java b/tlatools/src/tlc2/tool/ConcurrentTLCTrace.java
index 3aa689e81777c00b289c3823cda583ae46ca93dd..d49934ff25cbd9801b1ff82bc85dd7d920c38dae 100644
--- a/tlatools/src/tlc2/tool/ConcurrentTLCTrace.java
+++ b/tlatools/src/tlc2/tool/ConcurrentTLCTrace.java
@@ -73,7 +73,10 @@ public class ConcurrentTLCTrace extends TLCTrace {
 		return maxLevel;
 	}
 
-	private TLCStateInfo[] getTrace(final TLCState state) throws IOException {
+	/**
+	 * @see TLCTrace#getTrace(LongVec)
+	 */
+	public TLCStateInfo[] getTrace(final TLCState state) throws IOException {
 		final LongVec fps = new LongVec();
 
 		// Starting at the given start fingerprint (which is the end of the
diff --git a/tlatools/src/tlc2/tool/TLCTrace.java b/tlatools/src/tlc2/tool/TLCTrace.java
index bfce2da92bb531f3219e51b3dd4c9c99c04aacc2..448d0042b7d438049f117b2748cfe7494a7bfcc4 100644
--- a/tlatools/src/tlc2/tool/TLCTrace.java
+++ b/tlatools/src/tlc2/tool/TLCTrace.java
@@ -260,6 +260,17 @@ public class TLCTrace {
 		return getTrace(fps);
 	}
 
+	/**
+	 * This method is *not* safe to call multiple times iff the spec being checked
+	 * consumed randomness, ie. TLC!RandomElement or through the Randomization
+	 * module. In other words, such specs are incompatible with TLC's -continue
+	 * mode.
+	 * <p>
+	 * To implement this correctly, state space exploration would either have to
+	 * halt while the fingerprints are resolved to TLCStates below or ITool has
+	 * to offer additional API s.t. the seed of RandomEnumerableValues gets
+	 * passed as part of the method call.
+	 */
 	protected final TLCStateInfo[] getTrace(LongVec fps) {
 		// Re-Initialize the rng with the seed value recorded and used during the model
 		// checking phase. Otherwise, we won't be able to reconstruct the error trace
diff --git a/tlatools/src/tlc2/value/impl/EnumerableValue.java b/tlatools/src/tlc2/value/impl/EnumerableValue.java
index cac7483d462edff39c4008bbf3896ebd68f5cb11..86586301a1e8549df487709e53bd3c1d62ed2e42 100644
--- a/tlatools/src/tlc2/value/impl/EnumerableValue.java
+++ b/tlatools/src/tlc2/value/impl/EnumerableValue.java
@@ -121,7 +121,7 @@ public abstract class EnumerableValue extends Value implements Enumerable {
 			//
 			// x has to be co-prime to n. Since n might or might not be a prime number
 			// - it depends on the actual size of the set - we simply set x to
-			// be a prime number. The prime x has to be larger than n tough, since n is
+			// be a prime number. The prime x has to be larger than n though, since n is
 			// bound by Integer.MAX_VALUE, we simply choose the Mersenne prime
 			// Integer.MAX_VALUE
 			// for x and accept that we fail if n = Integer.MAX_VALUE. To minimize