René Maseli

> How would one go about computing partial encode sets for lazy encodings? It should be no problem to add methods like below to `WmmEncoder`. Keeping track of `alreadyEncoded` would...

This exposes a bug in my default implementation of `Definition#substitute(Relation,Relation)`. I will have to add implementations to all definitions. ~~Since the method makes no sense to be public at all,...

Don't forget the `ctrl` edge between the `RMWReadCond` event and its connected `RMWWriteCond`, as well as the dependency to the compared value. It might be required to work with `Assume`...

`assume_abort_if_not` should be equivalent to `assert` instead of `assume`. See its definition in i.e. `rfi005_tso.oepc.c`: ```cpp void assume_abort_if_not(int cond) { if(!cond) {abort();} } ```

The difference to `__VERIFIER_assert` is the missing call to `reach_error()`. I assume `abort()` is just meant to be non-returning, while otherwise unimportant to the verification. ``` void __VERIFIER_assert(int expression) {...

I see now that `include/assert.h` effectively equalizes `assert` to `__VERIFIER_assert`. I propose removing the latter entirely, while reimplementing `assert` accordingly, since we already define built-ins `reach_error()` and `abort()`.

In our current implementation, the program from https://github.com/hernanponcedeleon/Dat3M/issues/127#issuecomment-932537343 contains dead code.

Currently, [`VisitorBoogie`](https://github.com/hernanponcedeleon/Dat3M/blob/517d6f9bbc6ecf9bb85503a2364f0486d9a51fa1/dartagnan/src/main/java/com/dat3m/dartagnan/parsers/program/visitors/boogie/VisitorBoogie.java) transforms `reach_error()` as it does `VERIFIER_assert(0)`. > Unfortunately, when converting to LLVM and then to boogie, I have seen `assert()` converted to many different variations including `__assert_rtn`, `assert_.i32`,...

This leaves us with six ways of inserting an reachability condition at Boogie-level: - function `assert_(i32)` translated from C-level function `assert(int)` from [`include/assert.h`](https://github.com/hernanponcedeleon/Dat3M/blob/517d6f9bbc6ecf9bb85503a2364f0486d9a51fa1/include/assert.h). Used in our benchmarks. - function `assert_.i32(i32)`...

Brief: This analysis is not robust against general flattening. However, it should be robust against flattening of addition. I looked into your example. It features flattening of an expression `r4...