diffblue/cbmc

Multidimensional arrays?

Opened this issue · 0 comments

Hi all.
Thank you all for hard work in developing such a wonderful tool!

I'm trying to solve sudoku using cbmc:
https://yurichev.com/tmp/cbmc/CBMC_sudoku_or.c

cbmc --trace --function check CBMC_sudoku_or.c

But it works partially:
https://yurichev.com/tmp/cbmc/output.txt
In 'tmp' variable you see the first row of solved sudoku puzzle, which is correct.
But the rest of multidimensional array isn't printed.
How to print it all?