This isn't actually a bug. Your spec isn't machine-closed (see page 112 in Specifying Systems). Let's expand out the definition of WF_vars(HackStep):
WF_vars(HackStep) == <>(ENABLED <<HackStep>>_vars) => <><<Hackstep>>_vars)
In your spec, Hackstep is always enabled: there is no state where tmp' = 1 /\ UNCHANGED pc is forbidden. But Hackstep isn't part of your spec. So we can (handwaving a bit) rewrite it as
Spec == Init /\ [(Step1 \/ Step2) /\ ~HackStep]_vars /\ <><<Hackstep>>_vars
So we have that in a valid behavior, HackStep must happen infinitely often and also HackStep may never happen. No behavior could satisfy this, and it reduces to Spec == FALSE.
Saying GetsToDone is a property is equivalent to saying Spec => GetsToDone, which is equivalent to FALSE => GetsToDone, which is trivially true.
Always make sure your spec is machine closed. You can do that by only writing fairness properties that are subactions of Next.