Draft: Fix #941 k-induction unsound validation

This branch implements a fix for the problem described in #941 (closed). In short, it changes how k-induction selects ARG states for induction hypothesis and property violation.

k-induction was evaluated before and after the fix under three configurations: ki-df, ki-ki, and ki-kipdr. Here are the table and the diff. The results show that the change does not affect the performance of the code.