Improvements to 'bmc3' (start frame; stop when all POs are SAT; stop when 2^nRegs frames are completed).