Fixes related to Gazer 2.0

[sallaigy]

No description provided.

[hajduakos]

Seems like a lot of work! What are the longer term plans? It would be nice to have Gazer and Theta as part of a portfolio again, even if Theta does not (necesseraly) use Gazer as a frontend. Having a BMC pass first would still be super useful. Do you plan to incorporate other analyses? I think even if CEGAR-based methods do not align well with SSA, k-induction or IC3 could also work well.

[sallaigy]

Seems like a lot of work! What are the longer term plans? It would be nice to have Gazer and Theta as part of a portfolio again, even if Theta does not (necesseraly) use Gazer as a frontend. Having a BMC pass first would still be super useful. Do you plan to incorporate other analyses? I think even if CEGAR-based methods do not align well with SSA, k-induction or IC3 could also work well.

Indeed, and there are some other things I would like to do. I have two main points in mind:

1. Releasing a new major version of Gazer, compatible with the new Clang/LLVM versions, and fixing some weird dependency issues.
2. I am researching some ways to help the BMC algorithm prove correctness better. Currently I am experimenting with abstract interpretation to generate invariants, but it indeed would be interesting to explore k-induction and IC3 as well.

If you have the time, we could have a chat about this sometime :)