[tlaplus] Does TLC handle <> and ~[]~ differently?

The three properties defined should be logically equivalent, but the last one gets an error in TLC. The only difference between Prop2 and Prop3 is the usage of ~[]~ vs <>, which I believe should not matter.

Is this expected TLC behavior? Should I change something in my configuration file? I would prefer not to modify the module itself, as the real one is machine-generated, and I would hate to have to implement LTL formula rewriting just to work around this specific issue.

----------------------------- MODULE TestBug -----------------------------

VARIABLE s

Init == s = "a"

Next == \/ /\ s = "a"
           /\ s' = "b"
        \/ /\ s = "b"
           /\ s' = "c1"
        \/ /\ s = "b"
           /\ s' = "c2"
        \/ /\ s = "c2"
           /\ s' = "c1"
        \/ /\ s = "c1"
           /\ s' = "c2"
        \/ /\ s = "c1"
           /\ s' = "a"

Spec == Init /\ [][Next]_s /\ WF_s(Next)

\* Succeeds
Prop1 == (s = "b") ~> ((s = "a") \/ [](s \in {"c1", "c2"} /\ <>(s = "c2")))
\* Should be equivalent to Prop1. Succeeds.
Prop2 == []((s # "b") \/ <>((s = "a") \/ [](s \in {"c1", "c2"} /\ <>(s = "c2"))))
\* Should be equivalent to Prop1 and Prop2. Fails.
Prop3 == []((s # "b") \/ ~[]~((s = "a") \/ [](s \in {"c1", "c2"} /\ <>(s = "c2"))))

(*
Error trace for Prop3:

1: Initial predicate, s = "a"
2: Next in TestBug, s = "b"
3: Next in TestBug, s = "c2"
4: Next in TestBug, s = "c1"
4: Back to state (links to s = "c2")

*)

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