diff --git a/tlatools/org.lamport.tlatools/src/util/Assert.java b/tlatools/org.lamport.tlatools/src/util/Assert.java index 3cb19484effaab388ec095bbd92ed3663fe750da..99a054407afad41c6373b9b33f364e7352fb51f4 100644 --- a/tlatools/org.lamport.tlatools/src/util/Assert.java +++ b/tlatools/org.lamport.tlatools/src/util/Assert.java @@ -4,6 +4,7 @@ package util; +import tlc2.output.EC; import tlc2.output.MP; /** @@ -101,7 +102,7 @@ public class Assert { if (!condition) { - throw new TLCRuntimeException(MP.getMessage(errorCode)); + throw new TLCRuntimeException(errorCode, MP.getMessage(errorCode)); } } @@ -135,7 +136,7 @@ public class Assert public TLCRuntimeException(String errorMsg) { super(errorMsg); - this.errorCode = -1; // Unknown error code. + this.errorCode = EC.GENERAL; // Unknown error code. } public TLCRuntimeException(int errorCode, String message) {