Unexpected result when calling count intrinsics with zero

[adpaco-aws]

CBMC version: 5.50.0
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: cbmc example.c, where example.c is

#include <assert.h>

int main() {
    unsigned char var = 0;
    assert(__builtin_clz(var) == 8);
}

What behaviour did you expect: Successful verification
What happened instead: Verification failed.
The result is unexpected because the commit that originally added support says "The result is always defined, even for zero (where the result is the bit width)". A similar thing happens if __builtin_clz is used instead.

[tautschnig]

I believe the behaviour is as expected: __builtin_clz (or __builtin_ctz) are undefined for zero. That's GCC's semantics, not ones of our own choosing. What is, however, defined, is the value of the underlying expression count_leading_zeros_exprt and count_trailing_zeros_exprt, respectively -- which is all that the comment is referring to.

[tautschnig]

Re-opening as it turns out there actually is an issue in count_trailing_zeros_exprt, which did mishandle zero. Bugfix forthcoming.