Gyula Sallai

> 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...

@radl97 Indeed, we currently store large int literals in `int64_t`. I think we can handle this either with `llvm::APSInt` (like `APInt`, but also stores sign information) or `boost::multiprecision`. Both solutions...

Thanks for raising this point. Indeed, it would make sense to upgrade eventually: installing old LLVM versions just for Gazer is definately not fun. Now this raises another interesting question:...

Note that the LLVM version in the current Ubuntu LTS (20.04, focal) is LLVM 10: https://packages.ubuntu.com/focal/llvm. So if we are doing Ubuntu LTS, then it's either 10 or we will...

There does not seem to be any syntactical issues with programs in this category, but they make heavy use of large, constant-bounded loops, something that the BMC algorithm handles very...

Indeed, it seems that we support this category alright, we just have performance issues (these programs are quite complex).

I checked a few programs in this category, I do not see major blockers, but for a few programs there is one major pain point: they contain irreducible control flow...

All of these programs seem to require malloc support, something we do not yet have in our flat memory model. I opened a separate ticket #86 to track that issue.

I like the idea, even though I think it would make sense to implement this only after #68

@radl97 This seems feasible to me, however we probably should only do this for allocas the we do not immediately see clobbered by a store. Otherwise we probably would ruin...