cbmc --object-bits 9 --trace --function check -DLEN=10 -DCBMC --unwind 9 --unwinding-assertions BM_cat_v1.c
cbmc --object-bits 9 --trace --function check -DLEN=10 -DCBMC --unwind 9 --unwinding-assertions BM_cat_v2.c