diff --git a/tlatools/src/tlc2/output/MP.java b/tlatools/src/tlc2/output/MP.java index fba524bba8d9aa50a83f32c9fb62664c7a196302..593529e5ecb2981b7f27b3574abc67be9449dd1d 100644 --- a/tlatools/src/tlc2/output/MP.java +++ b/tlatools/src/tlc2/output/MP.java @@ -358,7 +358,7 @@ public class MP break; case EC.TLC_INVARIANT_EVALUATION_FAILED: - b.append("Evaluating invariant %1% failed."); + b.append("Evaluating invariant %1% failed:\n%2%"); break; case EC.TLC_ACTION_PROPERTY_VIOLATED_BEHAVIOR: