% free variables:
R_EAX_5 : BITVECTOR(32);
% end free variables. 

ASSERT(
0bin1 =
(LET R_ECX_117_0 = BVPLUS(32, R_EAX_5,0hex11223344) IN
(LET R_ZF_144_1 = IF (0hex00000000=R_ECX_117_0) THEN 0bin1 ELSE 0bin0 ENDIF IN
(LET R_EBX_147_2 = (0bin0000000000000000000000000000000 @ R_ZF_144_1) IN
IF (R_EBX_147_2=0hex00000001) THEN 0bin1 ELSE 0bin0 ENDIF)))
);
QUERY(FALSE);
COUNTEREXAMPLE;
