Hernan Ponce de Leon

Also PRs should got to `development` and not `master`.

Yes, this won't fit for verification of C programs unless such instructions end up in some compilation scheme. I think some (not sure if all) of those instructions are related...

This seems to also affect refinement (which inherently uses the incremental solver for the outer iteration): when running refinement tests on the litmus tests, we get problems in these benchmarks...

I tried disabling the `usePhantomReferences` option and the problem remains.

I think I came up with an idea that might solve this problem (and hopefully also #132 and #198). It will also have an impact in #137. As I see...

You are right (I should have read the 2nd msg in the issue). However, I think that the solution in the 3rd msg combined with (2) should also removed the...

Judging from [this](https://github.com/herd/herdtools7/blob/5f97d73b47293d5635e9322ee93d852622c010c4/herd/monad.mli#L102) ("read read" should be "read reg" I think) we don't want to have `ctrl` dependency between those events. Unfortunately the LKMM paper does not discuss CAS or...

I think any operation that is not intended to be placed in between the load and the store will be ordered by `ppo` so probably the compilation scheme you suggests...

I don't agree (or I'm missing something). The definition of `assume_abort_if_not` says that the program should abort execution if `cond` is false, however the program should *NOT* fail. If we...

[Here](https://github.com/sosy-lab/sv-benchmarks/issues/578) there is a description of problems that occurred in SVCOMP due to people understanding the semantics of `__VERIFIER_Assume` differently. As I see it, the semantics of our `Assume` event...