diff --git a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java
index ab761a43730c1bb760e6c065540308ede029ce38..88bef1fc7a49a93a590b36f4a0cea3c3e5f12070 100644
--- a/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java
+++ b/org.lamport.tla.toolbox.tool.tlc.ui/src/org/lamport/tla/toolbox/tool/tlc/output/data/TLCModelLaunchDataProvider.java
@@ -52,6 +52,7 @@ import org.eclipse.ui.editors.text.FileDocumentProvider;
 import org.eclipse.ui.part.FileEditorInput;
 import org.lamport.tla.toolbox.Activator;
 import org.lamport.tla.toolbox.tool.tlc.launch.IModelConfigurationConstants;
+import org.lamport.tla.toolbox.tool.tlc.model.Assignment;
 import org.lamport.tla.toolbox.tool.tlc.model.Formula;
 import org.lamport.tla.toolbox.tool.tlc.model.Model;
 import org.lamport.tla.toolbox.tool.tlc.model.ModelWriter;
@@ -701,12 +702,16 @@ public class TLCModelLaunchDataProvider implements ITLCOutputListener
 											.getAttribute(attributeName, new ArrayList<String>(0));
                                     int attributeNumber = (attributeIndex != null) ? attributeIndex.intValue() : 0;
 
-                                    if (IModelConfigurationConstants.MODEL_PARAMETER_CONSTANTS.equals(attributeName)
-                                            || IModelConfigurationConstants.MODEL_PARAMETER_CONSTANTS
-                                                    .equals(attributeName))
+                                    if (IModelConfigurationConstants.MODEL_PARAMETER_CONSTANTS.equals(attributeName))
                                     {
-                                        // List valueList = ModelHelper.deserializeAssignmentList(attributeValue);
-                                        idReplacement = "'LL claims this should not happen. See Bug in TLCModelLaunchDataProvider.'";
+                                    	// MK 07/25/2017: Correctly show error when constant is assigned a non-constant.
+                                        final List<Assignment> valueList = ModelHelper.deserializeAssignmentList(attributeValue);
+                                        if (valueList.size() >= (attributeNumber + 1)) {
+	                                        final Assignment assignment = valueList.get(attributeNumber);
+	                                        idReplacement = assignment.getRight();
+                                        } else {
+                                        	idReplacement = "'LL claims this should not happen. See Bug in TLCModelLaunchDataProvider.'";
+                                        }
                                     } else
                                     {
                                         // invariants and properties
diff --git a/tlatools/src/tlc2/output/EC.java b/tlatools/src/tlc2/output/EC.java
index 65d820468b658e03d0c5cbfba83e5f379e410815..02d5eb207f1501c4707f8b388b43266773c6cf52 100644
--- a/tlatools/src/tlc2/output/EC.java
+++ b/tlatools/src/tlc2/output/EC.java
@@ -233,8 +233,8 @@ public interface EC
     public static final int TLC_CONFIG_RHS_ID_APPEARED_AFTER_LHS_ID = 2223;
     public static final int TLC_CONFIG_WRONG_SUBSTITUTION = 2224;
     public static final int TLC_CONFIG_WRONG_SUBSTITUTION_NUMBER_OF_ARGS = 2225;
-    public static final int TLC_CONFIG_UNDEFINED_OR_NO_OPERATOR = 22251;
-    public static final int TLC_CONFIG_SUBSTITUTION_NON_CONSTANT = 22252;
+    public static final int TLC_CONFIG_UNDEFINED_OR_NO_OPERATOR = 2280;
+    public static final int TLC_CONFIG_SUBSTITUTION_NON_CONSTANT = 2281;
     public static final int TLC_CONFIG_ID_DOES_NOT_APPEAR_IN_SPEC = 2226;
     public static final int TLC_CONFIG_NOT_BOTH_SPEC_AND_INIT = 2227;
     public static final int TLC_CONFIG_ID_REQUIRES_NO_ARG = 2228;