Improve proof obligation generation of the B model
In the current master [40f9ddcf], some components produce a lot of proof obligations (which takes quite some time to generate and will be most probably hard to prove).
We should improve the B model to reduce that. This has also been taken care of in a recent merge request (see #1007 (closed) and !864 (merged)).
A good start is the larger component: service_mgr_i
which produces 5625 POs.