Added proper support for __VERIFIER_assert

[ThomasHaas]

This PR adds support for __VERIFIER_assert. Unlike standard assertions, the verifier version will not create control-flow branching (i.e. it does not termiante the program when violated) and hence does not create control dependencies.
However, the user still has to be careful to avoid short-circuiting connectives because those will induce control-flow dependencies:

int r = x;
__VERIFIER_assert(r == 0)
y = 5 // No ctrl-dep to load

--------

int r = x;
__VERIFIER_assert(r == 0 || r == 1) // short-circuiting adds ctrl-dep: use "bitwise or" instead
y = 5 // Accidental ctrl-dep to load

[hernanponcedeleon]

Did you notice any visible performance change now that the SMT solver needs to find full executions rather than terminating them soon?

[ThomasHaas]

No, this is not used anywhere (except the one new benchmark I added). You would need to recompile all benchmarks to use __VERIFIER_assert. For programs that use assert from <assert.h>, nothing changes.

[hernanponcedeleon]

Right. I will make a full run of svcomp benchmarks to test this.

[hernanponcedeleon]

The svcomp results show no problems, thus I'll merge

[ThomasHaas]

The svcomp results show no problems, thus I'll merge

Does this even make sense? I think Svcomp uses no __VERIFIER_assert because our previous code didn't even handle it correctly.
I think they use the standard assert from <assert.h> which is witnessed by the implementation of reach_error:

#include <assert.h>
void reach_error() { assert(0); }