by $OPENJADE knob). The reason is still unclear, but it is likely to be caused by some OpenSP's bug. Spotted by: pav