Michael Tautschnig

@animeshbchowdhury I'm not sure why it would be my call, but I certainly do appreciate all your work on this! I think we just need a pull request relabelling the...

Isn't the specific benchmark false for _any_ implementation? As discussed elsewhere, it might be best to exclude benchmarks using trigonometric functions. For the particular benchmark in question, however, it seems...

If they were `false-unreach-call` then I'd say "ok, needs to be added to #480". But claiming the call is truly unreachable in presence of undefined behaviour is much harder. Please...

If you are asking for exploits, we might just keep it simple. Just link the following against the benchmarks: ````c void ldv_initialize() { __VERIFIER_error(); } ```` That's me making use...

I don't even know whether `unreach-call` is violated in absence of a memory safety error in test27-2.c, so, yes, I'm all for adding them to memory safety. I'm not going...

@PhilippWendler could we please document (in the README file in the long run, but as first step just in here) what the system is we should be preprocessing on, and...

If anyone has Ubuntu 16.04 at hand, running the below script should hopefully yield the most reasonable diff. Neither 14.04 nor 18.04 seemed like the best candidates. ````bash #!/bin/bash set...

Just for the record: Ubuntu 16.04 doesn't help much either. @kfriedberger What OS have you been working on when preparing e76bcd95? I would then re-try processing on that OS.

@kfriedberger Thanks, I'll try to set up a machine with one of those.

I have tried both Ubuntu 12.04 and Arch Linux (though a very recent one for the latter), and neither provide particularly good results. I'll now simply go for Ubuntu 18.04...