TLC not handling disjunction correctly in special case?

I've created a minimal spec to demonstrate what might be a case of TLC not properly handling disjunction. Running TLC on this spec produces a runtime exception. The case occurs when you have a variable which can either hold a record value or a null value; this formula will throw an exception when the record is null, when we expect it to just evaluate to true:

Formula ==
    \/ record = NoRecord
    \/ record.key

Of course TLC isn't expected to exactly correspond to mathematical semantics (it cares about the order of elements in a conjunction when defining/referencing primed variable values, I believe) but might this be a case where TLC can "short-circuit" the evaluation of the formula once it sees the first disjunct is satisfied? Or even wrap every disjunct in a try/catch to see whether it can find one which both fails to throw an exception and evaluates to true? Maybe this has all been considered before and rejected because it produces surprising behaviour elsewhere.

Here's the full spec:

-------------------------------- MODULE Bug --------------------------------
EXTENDS     Naturals

VARIABLE    clock,
            record

RecordType == [key : BOOLEAN]

NoRecord == CHOOSE r : r \notin RecordType

TypeInvariant ==
    /\ clock \in Nat
    /\ record \in RecordType \cup {NoRecord}

Tick ==
    /\ \/ record = NoRecord
        \/ record.key
    /\ clock' = clock + 1
    /\ UNCHANGED <<record>>

CreateRecord ==
    /\ record = NoRecord
    /\ record' = [key |-> FALSE]
    /\ UNCHANGED <<clock>>

SetRecordFlag(value) ==
    /\ record /= NoRecord
    /\ record' = [record EXCEPT !.key = value]
    /\ UNCHANGED <<clock>>

DestroyRecord ==
    /\ record /= NoRecord
    /\ record' = NoRecord
    /\ UNCHANGED <<clock>>

Init ==
    /\ clock = 0
    /\ record = NoRecord

Next ==
    \/ Tick
    \/ CreateRecord
    \/ \E t \in BOOLEAN : SetRecordFlag(t)
    \/ DestroyRecord
=============================================================================