The incremental smt2 decision procedure does not yet support casting from C booleans to C integers. This is straight forward to implement as both types are just bit vectors. Its just an extra case in the extension_for_type function. Note that old versions of C did not include a bool type, but from C99 onwards it is supported as the _Bool type intrinsic or if <stdbool.h> is included then as just bool. This affects the following regression tests -

• cbmc/Bool/bool2.desc
• cbmc/Bool/bool3.desc
• cbmc/c99_Bool/test.desc