Thomas Haas

The stack requires a double-width CAS, which we don't support (yet). The queue might be doable, but it has a lot of bit vector reasoning.

I remember that library. Maybe we could ask them about the concurrency aspect. According to their github, they are still changing the CFG representation to be as flexible as possible....

I'm not really a fan of the default naming for relations. I think I would prefer unnamed relations instead. They would only be identified by their definition. For example, the...

Another issue I see is that the active set (encodeSet) computation is now completely hidden inside the `WmmEncoder`/`EncodeSets`. How would one go about computing partial encode sets for lazy encodings?...

Those methods would be helpful. I agree that `alreadyEncoded` needs to be tracked elsewhere (e.g., in the `RefinementSolver`). I would probably name the second method like this: ``` BooleanFormula encodeRelations(Map...

Relations that are defined via `let r = ...` are unnamed now. The parser adds an alias but the relation itself remains unnamed.

I think I mentioned this before, but you would simply never merge relations if they are named. E.g. in your case, ```r=r1+r2``` is a named relation, so an instance of...

> In order to keep instances of WmmEncoder consistent with their environment (and to shorten parameter lists), they store references to VerificationTask, (analysis-) Context and SolverContext. Let me tell you...

It seems that this PR breaks a lot of tests. Also, together with Refinement it triggers some invariant exceptions (something about knowledge propagating downward).

I fixed most "easy" bugs. There are two remaining problems - One of the Svcomp stack benchmarks causes an out of memory problem. This is due to the `ext`-Relation containing...