Combine k-induction with IMC

This MR combines k-induction with IMC. Before trying to compute fixed point with interpolation (the inner loop of IMC), we check whether the safety property is inductive (the step-case of k-induction).

In theory, IMC should always able to find a proof if the property is inductive. However, in practice, IMC might spend too much time computing a fixed point for such case and went into timeout, whereas k-induction can prove it a lot faster. From our evaluation (results.2022-10-28_16-53-25.table.html), running k-induction and IMC together can solve 30+ cases than running IMC alone.