Fix unreach-call verdict in weaver buffer benchmarks
After discussing with weaver's developers @schuessf @klumppdo , we find the three "buffer benchmarks" in weaver have wrong verdicts, including popl20-bad-buffer-mult-alt.wvr.c, popl20-more-buffer-mult.wvr.c, and popl20-more-buffer-series.wvr.c.
For example, bad-buffer-mult-alt has
__VERIFIER_atomic_begin();
assume_abort_if_not(q1_back >= 0 && q1_back < n1 && q1[q1_back] == C);
q1_back++;
__VERIFIER_atomic_end();
__VERIFIER_atomic_begin();
i++;
__VERIFIER_atomic_end();
while bad-buffer-mult-alt2 replaces it with
__VERIFIER_atomic_begin();
assume_abort_if_not(q1_back >= 0 && q1_back < n1 && q1[q1_back] == C);
q1_back++;
i++;
__VERIFIER_atomic_end();
both of which won't cause property violations.
Additionally, we find that another order
__VERIFIER_atomic_begin();
assume_abort_if_not(q1_back >= 0 && q1_back < n1 && q1[q1_back] == C);
i++;
__VERIFIER_atomic_end();
__VERIFIER_atomic_begin();
q1_back++;
__VERIFIER_atomic_end();
may cause property violations. We implement this order into a new variant, called bad-buffer-mult-alt3.