Completely eliminate __VERIFIER_assume from the sv-benchmarks repository.

[skanav]

Later, I will propose to completely eliminate __VERIFIER_assume from the sv-benchmarks repository.
For now, please change only those files that you encounter and that affect the result of some tool in a wrong way.

Originally posted by @dbeyer in #1028 (comment)

[skanav]

As per the description in #1031 and the discussion in #1028 there are two cases when the assumed expression evaluates to false

1. The call should be replaced by abort - this seems to be OK for each property specification expect memory cleanup
2. The call should be replaced by an non-terminating loop - this seems to be the acceptable interpretation for the memory cleanup tasks

My proposal is to do 2 for the memory cleanup tasks and 1 for the remaining ones.

Additionally, there has been a long discussion on it in #578 and #504.

[skanav]

There are only 3 benchmarks which use __VERIFIER_assume and are also memory cleanup tasks: (verifythis/tree_del_rec.c), (verifythis/tree_del_iter.c) and (verifythis/prefixsum_rec.c).

These three benchamarks check for the properties memory cleanup and unreach call. For these files I will use a non terminating loop. All the other occurrences of __VERIFIER_assume(p) will be replaced by if(!p) {abort();}