Thanks for the reference. A new version of VirtualBox with the problem fixed is now building. One warning - OBS has had difficulties with 32-bit builds for VB. The jobs hang with no errors and are terminated after a long time with no action. Thus, it may take a while for the new package to appear.