Transformation with trunc to i1 doesn't verify when equivalent code using icmp verify

[andjo403]

When trying to verify a CVP fold for trunc %x to i1 the transformation doesn't verify but if changed to equivalent icmp ne (and %x, 1), 0 the transform verify.

the proof that fails and the equivalent can be found in https://alive2.llvm.org/ce/z/BTCf7c
the full set of proofs that I wanted to check where multiple works as expected https://alive2.llvm.org/ce/z/fTPEg6

[nunoplopes]

Your example is wrong; val != 0 doesn't imply trunc(val) == 1.
The counterexample clearly points out that when %a is 2, the transformation is incorrect.