Simmo Saan

I think it's not worth complicating things by having another option for this feature, which probably made no performance difference. But I'll have a closer look before closing.

I cherry-picked 1f4bd6e9db07526c028aab14e4c3c6e0b59ba3b8 onto master because it's orthogonal cleanup, but let's leave the rest for now.

> can be run independently from the already existing apron analyses. > Abstract states in the newly added domain are represented by structs containing a matrix and an apron environment....

> Currently, it's for example not possible to run the polyhedra and affeq analysis simultaneously. That's what we wanted to change. Currently (on `master`) there's no affeq to begin with,...

> Having a completely apron-free implementation also didn't make sense for us since we wanted to keep the apron abstract syntax tree plus its conversion functions. For comparing our affeq...

> * Another major change is that functions with side effects (usually ending with "_with") defined inside `apronDomain` were replaced by functional equivalents This point is easily missed when looking...

> * implementations for vectors and matrices (realized through lists and lists of lists. Could be replaced in future This is also a major point when it comes to performance...

Indeed, we shouldn't make such significant changes right before SV-COMP. Based on a quick look at the related thesis, it seems like in SV-COMP this doesn't give us an advantage...

> The question is if we can perform some sort of relifting automatically or whether that will break invariants of those hash tables that are not fresh (as `reachable` is)....

> I fear one might have to clean the hashtable and repopulate it or some such nonsense to restore the invariants a hashtable relies upon. That's exactly what the relifting...