Model evaluator forgetting about state variable

[rws...@xxxxxxxxx]

I've been editing a fairly complicated (for me, at least) specification across multiple modules. This is happening on a Linux box with Oracle Java 1.8 and toolkit 1.5.1. One of the modules starts as follows:

=== start fragment
------------------------ MODULE ObjectWithEventsCrud ------------------------
EXTENDS EnumeratedField

LOCAL INSTANCE Integers
LOCAL INSTANCE Sequences
LOCAL INSTANCE TLC
LOCAL INSTANCE GlobalConstants

VARIABLE objectStore
=== end fragment

Further down in the spec there's the following operator (Print statements are there because I'm trying to figure out what's going on):
=== start fragment
\* ============= STEPS ===================
\* Add an object to the objectStore
createObjectInEmpty(objectId, noHistoryFunction) ==
  /\ Print("CRUD create object empty legal",LegalNoHistory(noHistoryFunction))
  /\ Print("CRUD create object empty id",objectId \in ObjectIdSet)
  /\ Print("CRUD create object empty isEmpty", objectStore = EMPTY_STORE)
     \* covered by TestObjectWithEvents
  /\ objectStore' = Print("CRUD create object empty new", [x \in {objectId} |->
        [class |-> ObjectClass,
         id |-> objectId,
         noHistory |-> noHistoryFunction,
         mostRecent |-> NULL_FUNCTION,
         events |-> NO_EVENTS] ])
  /\ UNCHANGED enumeratedStore
=== end fragment

There are no parse errors. When I run a model that includes this module, I get the following error:

TLC threw an unexpected exception.
This was probably caused by an error in the spec or model.
See the User Output or TLC Console for clues to what happened.
The exception was a java.lang.RuntimeException: In evaluation, the identifier objectStore is either undefined or not an operator.
line 29, col 1 to line 36, col 37 of module Test2ObjectWithEvents
The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 38, column 33 to line 38, column 59 in Test2ObjectWithEvents
1. Line 191, column 32 to line 191, column 62 in ObjectWithEventsCrud
2. Line 188, column 6 to line 188, column 53 in ObjectWithEventsCrud
3. Line 188, column 6 to line 188, column 53 in ObjectWithEventsCrud
4. Line 163, column 6 to line 168, column 33 in ObjectWithEventsCrud
5. Line 163, column 6 to line 163, column 16 in ObjectWithEventsCrud
6. Line 29, column 1 to line 36, column 37 in Test2ObjectWithEvents

Stack Entry #3 points to the objectStore' expression above and #4 points to the "objectStore" string that's followed by the prime. This is consistent with the user output reported by the model:

"CRUD create object empty legal"  TRUE
"CRUD create object empty id"  TRUE
"CRUD create object empty isEmpty"  TRUE
"CRUD create object empty legal"  TRUE
"CRUD create object empty id"  TRUE
"CRUD create object empty isEmpty"  TRUE

I've tried the following:

a. Change the variable name to something other than objectStore, throughout the specification. RESULT: no change - model evaluation stops at the same place.

b. Change the initialization of objectStore to avoid entering the createObjectInEmpty operation. RESULT: similar error involving objectStore', but at a different place in the module.

c. Change objectStore' to xxx' in the offending operation. RESULT: parse error.

d. Change objectStore' to objectStore in the offending line. RESULT: model runs to completion, but of course doesn't cover all the expected states; the line becomes a FALSE qualification that stops the state from changing, rather than a state change.

Note that the model reports detecting two errors (consistent with two sets of user output in the model), though the error stack reports only one.

An earlier version of this spec worked fine, so the editing has clearly triggered something bad. Anybody have any idea what's going on and (more importantly) how to fix it?