8 This contains the first full application. CBMC is a bounded model
9 checker that uses the front ends (`ansi-c`, `cpp`, goto-program or
10 others) to create a goto-program, `goto-symex` to unwind the loops the
11 given number of times and to produce and equation system and finally
12 `solvers` to find a counter-example (technically, `goto-symex` is then
13 used to construct the counter-example trace).