The main change here is a fix to IMC to produce correct inductive invariant for the given transition system.
The problem was that when IMC detects a fixed point, the state formula is an inductive invariant, but it is not necessarily safe on its own. We only know that it cannot reach bad states in k steps where k is the current value of the parameter of the procedure finiteRun.
While this is sound, because it still guarantees that bad states are unreachable, the witness has to be different.
For now I only was able to prove that the fixed point conjoined with the negation of bad states is k-inductive.
(It would be good to try to improve on this to avoid k-induction).
While working on this, I discovered a bug in BackTranslator for NodeEliminator which was not tracking the necessary information correctly and this resulted in incorrect final proofs.
Additionally, this PR adds the backtranslator for MultiEdgeMerger (which merges multiple edges with the same source and target to a single edge). This enables us to use MultiEdgeMerger for the preprocessing for all engines. This enabled IMC to solve more benchmarks and compute witnesses correctly for all UNSAT cases which it was able to solve.
The main change here is a fix to IMC to produce correct inductive invariant for the given transition system. The problem was that when IMC detects a fixed point, the state formula is an inductive invariant, but it is not necessarily safe on its own. We only know that it cannot reach bad states in
ksteps wherekis the current value of the parameter of the procedurefiniteRun. While this is sound, because it still guarantees that bad states are unreachable, the witness has to be different. For now I only was able to prove that the fixed point conjoined with the negation of bad states is k-inductive. (It would be good to try to improve on this to avoid k-induction).While working on this, I discovered a bug in
BackTranslatorforNodeEliminatorwhich was not tracking the necessary information correctly and this resulted in incorrect final proofs.Additionally, this PR adds the backtranslator for
MultiEdgeMerger(which merges multiple edges with the same source and target to a single edge). This enables us to useMultiEdgeMergerfor the preprocessing for all engines. This enabledIMCto solve more benchmarks and compute witnesses correctly for all UNSAT cases which it was able to solve.