There are builtin bit wise intrinsics which are not yet implemented for incremental smt2 decision procedure

[thomasspriggs]

There are builtin bitwise intrinsics which are not yet implemented for incremental smt2 decision procedure. These include -

• Count leading zeros - __builtin_clzl
• Count trailing zeros - __builtin_ctz
• Find first set - __builtin_ffs
• Population count - __builtin_popcount
• Rotation - __builtin_rotateleft*
• Bit reverse expressions - bitreverse_exprt
• Bitwise nand - ID_bitnand

The tests known to be affected by this include -

• cbmc/__builtin_clz-01/test.desc
• cbmc/__builtin_ctz-01/big-endian.desc
• cbmc/__builtin_ctz-01/test.desc
• cbmc/__builtin_ffs-01/big-endian.desc
• cbmc/__builtin_ffs-01/test.desc
• cbmc/clang_builtins/bitreverse.desc
• cbmc/atomic_fetch_X-1/test.desc
• cbmc/clang_builtins/rotate.desc
• cbmc/gcc_popcount1/test.desc