JBMC 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.