cbmc 5.6-1 (armhf binary) in ubuntu zesty

 CBMC generates traces that demonstrate how an assertion can be violated, or
 proves that the assertion cannot be violated within a given number of loop
 iterations.