Bajczi Levente
I might be wrong, but I think for example R[once], W[release], F[wmb], etc will be the new instructions. My idea was to use this specification to create specific instructions (or...
I think it's a good idea to include a check for that as well, but I'm not sure if #165 will change related checks in any way - @as3810t, what...
Will fix together with other CI issues, closing for now.
I tested this with native code calling MPFR functions (see code below), and it works surprisingly. This means that the java wrapper must be at fault. ``` c++ #include #include...
@Rorck Could you please check if Gamma still works with the new binaries (without any modification, _and_ with some of the new solvers)?
There were no objections (and this PR only adds functionality, it does not take any prior functionality away), so I'm merging this.
I think this has the same cause as #125, because the symptoms overlap.
Please see PR #127, I think I covered all important aspects for point 2.
I think this was solved with #143, closing.
Also note that while only one example is attached, many similar programs also produce the exception. The above example is transformed from an [SV-COMP task](https://github.com/sosy-lab/sv-benchmarks/blob/master/c/nla-digbench/cohencu-ll.c).