Why3 should allow to compile several engines for invariant inference simultaneously
The function Vc.set_infer_invs
allows to record one engine to infer invariants, if one records a second it will replace the former recorded one. We should allow several such engines.