There's one crucial piece of information missing here. This problem does not occur with the SMP OS/2 kernel. The reason being that the SMP kernel runs with the CR0.NE bit set. The actual number of processors in the guest does not matter.
