Hernan Ponce de Leon

Thanks @zvonimir for the pointer. Assuming you get the debug Information via `-g` flag, it seems clang is providing the correct one (see [sample.ll.zip](https://github.com/smackers/smack/files/5585338/sample.ll.zip)). The `$i4, $i5, $i6` instructions are...

@shaobo-he the code I gave above was obtained using directly clang (with no optimisations). However I would assume that if some debug information is lost during the optimisation passes, the...

@leventeBajczi I took a look to the bell extensions but it is not very clear to me how we can use this to define hardware fences at the C level....

I had a chat with one of my colleagues yesterday and I think now I have a better understanding of how to interpret these bell files. This is how I...

I might be missing something, but I don't see what is the aggregated value for this benchmarks. Besides the fact that the new benchmarks are larger than the base ones...

I can see the value in having loosely couple systems (microservices), but since "loosely" in here actually mean completely decoupled (exactly one of them is executed) one could argue that...

Thanks for the pointer. I see that in the context of evolving programs this makes sense.

I already understood why the "solution" using `assume_abort_if_not` does not work: the check would already overflow. @divyeshunadkat proposed in #1155 to use `long long` as the type or certain variables....

Now that #1155 has been merged, we can proceed to fix the inherited bugs in `nla-digbench-scaling`. @MartinSpiessl can you please re-run your script in the new fixed benchmarks from `nla-digbench`?...

I think there are still problems overflows with `egad2-ll` and `egad3-ll`. I tried checking overflows with CPAchecker and got violations: `scripts/cpa.sh -svcomp20 -heap 10000M -benchmark -timelimit '900 s' -64 -stats...