Programs handling arrays. Taken or adapted from the benchmark suites of
the BOOSTER software verifier (http://verify.inf.usi.ch/booster)
and the SAFARI model-checker (http://verify.inf.usi.ch/safari).

relax_true-unreach-call.c was built for the purpose of VerifyThis 2015.