About single process system, fairness, and depth-first search option

["rvpr...@xxxxxxx" <venkateshpra...@xxxxxxxxx>]

I have the following module in PlusCal. 
 
(*

--algorithm Untitled
{
    variables u = 24 ; v \in 1 .. N;
    {
        print <<u, v>>;
        while (u # 0) {
            if (u < v) {
                u := v || v := u
            };
            u := u - v ;
        };
        print <<"have gcd", v>>;
    }
}

\*PlusCal options (-wf)

*)

Here are the observations when running TLC with one worker thread.

1) Model checking this module for termination with N as 30, depth as 50, and Depth-first checked, results in no errors.

2) Model checking this module for termination with N as 30, depth as 50, and Depth-first unchecked, results in an error trace suggesting temporal properties were violated.

3) Uncommenting PlusCal options line and then model checking this module statement for termination with N as 30, depth as 50, and Depth-first unchecked, results in no errors.

4) Uncommenting PlusCal options line and then model checking this module statement for termination with N as 30, depth as 50, and Depth-first checked, results in no errors.

Why does (2) result in an error?

Isn't the above algorithm treated as a single process system?  If so, why is the explored behavior affected by fairness constraints (3)?