How come TLA never hits the assert?

[recepient recepient]

Consider this process definition in which everything seems to run except, that once the if-then is evaluated, the assert is never hit. Without the assert, the process never seems to run the goto command either.

process MainProc \in NumClients+1..NumClients+1

variable rpc, msg;

begin

master_dequeue:

    print "await master_dequeue";

    await MasterInQueue /= <<>>;

    (* print << "master pre-dequeue:", MasterInQueue>>; *)

    rpc:=Head(MasterInQueue);

    MasterInQueue:=Tail(MasterInQueue);

    (* print << "master post-dequeue:", MasterInQueue>>; *)

master_combine:

    rpc := rpc \o << MasterSequence >>;

    Message := Message \o rpc;

    MasterSequence:=MasterSequence+1;

master_handler:

    if (rpc[RpcOpIdx]=OP_GET)

    then

        skip;

    else

        call masterWrite(rpc);

    end if;

master_cont:

    assert FALSE;

    print "goto master_dequeue";

    goto master_dequeue;

end process;

[recepient recepient]

I'll try to answer my own question: this is a (weird) side effect of the call to masterWrite: it did not have a return it. Adding a return fixed this problem.
Apparently failing to run return does not revert procedure's local variables to their initial, default value. For imperative C/C++ programmers like me,
it's an unexpected side effect.