Thomas Haas

Our approach is not a predicate abstraction. We verify parallel programs under weak memory models and have a custom theory solver for memory consistency that explores a program execution (a...

You have custom JNI files, so that snippet does not really show if they call just gets forwarded to Mathsat5. However, the JNI files don't seem to be suspicious either....

Ok, that is very interesting. I assume you evaluated both the boolean and the integer variables. If that is the case, and it is indeed that fast, then something is...

I noticed that `MathSAT5` also works on Windows (stupid me), so I could get around to actually run and debug the issue myself. And I can pinpoint where the time...

I did some more digging and found out that MathSAT5 has two ways to retrieve a model value according to their [API documentation](https://mathsat.fbk.eu/apireference.html). Both methods are also in JavaSMTs native...

Thank you for the effort. Unfortunately, it is quite hard to construct an explicit example of this behaviour because it's not just a matter of running some SMTLIB problem through...

Thanks, I'm looking forward to the new release :)

I see the issue with the strongly typed options. Would it be possible to allow the user to specify a type like e.g. ``` parallel.enable=(bool)true // Could also use different...

Note that `Sc-per-Loc` is enough to make this optimization possible for all memory models (not sure about C11 though). In full generality it may fail though. Unfortunately, this is the...

Local consistency =/= SC-per-Loc though. Local consistency is even weaker and is basically Sc-per-thread (or Sc-per-thread-per-loc?). I think we should add a second flag for SC-Per-Loc or alternatively a flag...