Add a "mode" option on .cfg file to define whether you are going for a bmc or an induction proof