Oops, same issue in my cbmc version. 
Fixed: http://svn.clifford.at/handicraft/2018/cbmc/bsort.c …
Proving that what I do in check?b() is sufficient to prove that it is a permutation, given that elements of data[] are only copied, is left as an exercise for the reader. 
(Spoiler: It's probably not. :)
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
This Tweet is unavailable.
-
Assume an algorithm that checks if one of the data[] elements has all-bits set. Say if all bits are set on at one element, then we copy that to all the other elements, otherwise we sort. This will pass that checker even though it does not sort in all cases.
For the case where SZ<=8*sizeof(T) I can easily see that my check is sufficient for the case where all data elements are distinct. But there is an argument to be had here that we use SMT solvers because we don't want to make arguments like that using our inferior human brains. :)