$ cbmc --trace --function check isXMLdigit.c

...

** Results:
[check.assertion.1] assertion isXMLDigit_optimized(c) == isXMLDigit(c): SUCCESS

** 0 of 1 failed (1 iteration)
VERIFICATION SUCCESSFUL