Bug in TLC when checking if integer record field is element of integer range

[Andrew Helwer <andrew...@xxxxxxxxx>]

I'm using toolbox 1.5.1, with TLC version 2.07. This TLA+ code repros the issue:

------------------------------ MODULE Bugcheck ------------------------------
EXTENDS Integers

VARIABLES record

Set == {1,2,3}

Range == {1 .. 3}

SetRecord == [number : Set]

RangeRecord == [number : Range]

TypeInvariant ==
    /\ record.number \in Set
    /\ record \in SetRecord
    /\ record.number \in Range
    /\ record \in RangeRecord

Init == record = [number |-> 2]

Next == UNCHANGED record

Spec == Init /\ [][Next]_<<record>>

=============================================================================

When checking TypeInvariant in the initial state, the first three conjuncts pass but the final conjunct (record \in RangeRecord) causes this TLC error:

Attempted to compare integer 2 with non-integer:
1..3
While working on the initial state:
record = [number |-> 2]

Andrew