THEORY bitvectors-cast;
LOGIC QF_UFBV;
SOLVER external;
SIGNATURE Xor, icmp_sge, icmp_ugt, lshr, icmp_sgt, icmp_uge, icmp_ne, select, icmp_eq, sub, add, zext_11, True, trunc_11, add_i29, sext_11, sext, sext_i1, icmp, Or, trunc, And, icmp_ult, False, icmp_slt, icmp_ule, zext, shl, ashr, 

RULES
    And(Xor(X, C1), C2) -> Xor(And(X, C2), CL0)  [ ((C1 &.32 C2) =.32 CL0)] ; /* AndOrXor:135*/
    And(Or(X, C1), C2) -> And(Or(X, CL0), C2)  [ ((C1 &.32 C2) =.32 CL0)] ; /* AndOrXor:144*/
    And(Or(X, C1), C2) -> Or(And(X, CL0), C1)  [ (((C2 ^.32 (C1 &.32 C2)) =.32 CL0) /\ ((C1 &.32 C2) =.32 C1))] ; /* AndOrXor:151*/
    And(add(X, C1), C2) -> And(X, C2)  [ (isPowerOf2.32(C2) /\ (((C1 &.32 (C2 -.32 bv32"#x00000001")) =.32 bv32"#x00000000") /\ ((C2 &.32 C1) =.32 bv32"#x00000000")))] ; /* AndOrXor:185*/
    And(add(X, C1), C2) -> Xor(And(X, C2), C2)  [ (isPowerOf2.32(C2) /\ (((C1 &.32 (C2 -.32 bv32"#x00000001")) =.32 bv32"#x00000000") /\ ((C2 &.32 C1) !=.32 bv32"#x00000000")))] ; /* AndOrXor:190*/
    And(shl(X, C1), C2) -> shl(X, C1)  [ ((C2 &.32 (bv32"#xffffffff" <<.32 C1)) =.32 (bv32"#xffffffff" <<.32 C1))] ; /* AndOrXor:206*/
    And(shl(X, C1), C2) -> And(shl(X, C1), CL0)  [ (((C2 &.32 (bv32"#xffffffff" <<.32 C1)) =.32 CL0) /\ (((C2 &.32 (bv32"#xffffffff" <<.32 C1)) !=.32 (bv32"#xffffffff" <<.32 C1)) /\ ((C2 &.32 (bv32"#xffffffff" <<.32 C1)) !=.32 C2)))] ; /* AndOrXor:210*/
    And(lshr(X, C1), C2) -> lshr(X, C1)  [ ((C2 &.32 (bv32"#xffffffff" >>u.32 C1)) =.32 (bv32"#xffffffff" >>u.32 C1))] ; /* AndOrXor:226*/
    And(lshr(X, C1), C2) -> And(lshr(X, C1), CL0)  [ (((C2 &.32 (bv32"#xffffffff" >>u.32 C1)) =.32 CL0) /\ ((C2 &.32 (bv32"#xffffffff" >>u.32 C1)) !=.32 (bv32"#xffffffff" >>u.32 C1)))] ; /* AndOrXor:230*/
    And(ashr(X, C1), C2) -> And(lshr(X, C1), C2)  [ (hasOneUse.32 /\ ((C2 &.32 (bv32"#xffffffff" >>u.32 C1)) =.32 C2))] ; /* AndOrXor:246*/
    And(icmp_sge(X, C1), icmp_slt(X, C2)) -> False  [ ((C1 <=s.32 C2) /\ (C1 =.32 C2))] ; /* AndOrXor:270*/
    And(icmp_sge(X, C1), icmp_slt(X, C2)) -> icmp_slt(X, C2)  [ ((C1 <=s.32 C2) /\ (C1 =.32 (bv32"#x00000001" <<.32 (width.32(C1) -.32 bv32"#x00000001"))))] ; /* AndOrXor:273*/
    And(icmp_sge(X, C1), icmp_slt(X, C2)) -> icmp_ult(add(X, neg.32(C1)), CL0)  [ (((neg.32(C1) +.32 C2) =.32 CL0) /\ (C1 <=s.32 C2))] ; /* AndOrXor:280*/
    Or(icmp_slt(X, C1), icmp_sge(X, C2)) -> True  [ ((C1 <=s.32 C2) /\ (C1 =.32 C2))] ; /* AndOrXor:287*/
    Or(icmp_slt(X, C1), icmp_sge(X, C2)) -> icmp_sgt(X, CL0)  [ (((C2 -.32 bv32"#x00000001") =.32 CL0) /\ ((C1 <=s.32 C2) /\ ((C1 !=.32 C2) /\ (C1 =.32 (bv32"#x00000001" <<.32 (width.32(C1) -.32 bv32"#x00000001"))))))] ; /* AndOrXor:290*/
    Or(icmp_slt(X, C1), icmp_sge(X, C2)) -> icmp_ugt(add(X, neg.32(C1)), CL0)  [ (((neg.32(C1) +.32 (C2 -.32 bv32"#x00000001")) =.32 CL0) /\ ((C1 <=s.32 C2) /\ (C1 !=.32 C2)))] ; /* AndOrXor:298*/
    And(add(And(A, C1), B), C2) -> And(add(A, B), C2)  [ (((C1 &.32 C2) =.32 C2) /\ (isPowerOf2OrZero.32((C2 +.32 bv32"#x00000001")) \/ (isShiftedMask.32(C2) /\ MaskedValueIsZero.32(B, ((bv32"#x00000001" <<.32 (width.32(C2) -.32 countLeadingZeros.32(((C2 -.32 bv32"#x00000001") ^.32 C2)))) -.32 bv32"#x00000001")))))] ; /* AndOrXor:343*/
    And(add(Or(A, C1), B), C2) -> And(add(A, B), C2)  [ (isPowerOf2OrZero.32((C2 +.32 bv32"#x00000001")) /\ ((C1 &.32 C2) =.32 bv32"#x00000000"))] ; /* AndOrXor:363*/
    And(sub(Xor(A, C1), B), C2) -> And(sub(A, B), C2)  [ (isPowerOf2OrZero.32((C2 +.32 bv32"#x00000001")) /\ ((C1 &.32 C2) =.32 bv32"#x00000000"))] ; /* AndOrXor:364*/
    icmp_slt(X, bv32"#x00000000") -> icmp_ne(And(X, CL0), bv32"#x00000000")  [ ((bv32"#x00000001" <<.32 (width.32(X) -.32 bv32"#x00000001")) =.32 CL0)] ; /* AndOrXor:516*/
    icmp_sgt(X, bv32"#xffffffff") -> icmp_eq(And(X, CL0), bv32"#x00000000")  [ ((bv32"#x00000001" <<.32 (width.32(X) -.32 bv32"#x00000001")) =.32 CL0)] ; /* AndOrXor:523*/
    icmp_ult(X, C) -> icmp_eq(And(X, neg.32(C)), bv32"#x00000000")  [ isPowerOf2.32(C)] ; /* AndOrXor:530*/
    icmp_ugt(X, C) -> icmp_ne(And(X, ~.32(C)), bv32"#x00000000")  [ isPowerOf2.32((C +.32 bv32"#x00000001"))] ; /* AndOrXor:537*/
    And(icmp_eq(And(a, b), bv32"#x00000000"), icmp_eq(And(a, d), bv32"#x00000000")) -> icmp_eq(And(a, Or(b, d)), bv32"#x00000000"); /* AndOrXor:698*/
    And(icmp_eq(And(a, b), b), icmp_eq(And(a, d), d)) -> icmp_eq(And(a, Or(b, d)), Or(b, d)); /* AndOrXor:709*/
    And(icmp_eq(And(a, b), a), icmp_eq(And(a, d), a)) -> icmp_eq(And(a, And(b, d)), a); /* AndOrXor:716*/
    And(icmp_ne(And(a, C1), bv32"#x00000000"), icmp_ne(And(a, C2), bv32"#x00000000")) -> icmp_ne(And(a, C1), bv32"#x00000000")  [ ((C1 &.32 C2) =.32 C1)] ; /* AndOrXor:732-1*/
    And(icmp_ne(And(a, C1), C1), icmp_ne(And(a, C2), C2)) -> icmp_ne(And(a, C1), C1)  [ ((C1 &.32 C2) =.32 C1)] ; /* AndOrXor:732-2*/
    And(icmp_ne(And(a, C1), a), icmp_ne(And(a, C2), a)) -> icmp_ne(And(a, C1), a)  [ ((C1 |.32 C2) =.32 C1)] ; /* AndOrXor:745*/
    And(icmp_eq(And(a, C1), C2), icmp_eq(And(a, C3), C4)) -> icmp_eq(And(a, CL0), CL1)  [ (((C1 |.32 C3) =.32 CL0) /\ (((C2 |.32 C4) =.32 CL1) /\ ((((C1 &.32 C3) &.32 (C2 ^.32 C4)) =.32 bv32"#x00000000") /\ (((C1 &.32 C2) =.32 C2) /\ ((C3 &.32 C4) =.32 C4)))))] ; /* AndOrXor:757*/
    And(icmp_sgt(a, b), icmp_ne(a, b)) -> icmp_sgt(a, b); /* AndOrXor:794*/
    And(icmp_ult(a, C), icmp_ult(b, C)) -> icmp_ult(Or(a, b), C)  [ isPowerOf2.32(C)] ; /* AndOrXor:819*/
    And(icmp_eq(a, bv32"#x00000000"), icmp_eq(b, bv32"#x00000000")) -> icmp_eq(Or(a, b), bv32"#x00000000"); /* AndOrXor:827*/
    And(icmp_eq(CL0, C1), icmp_eq(And(x, C3), C2)) -> icmp_eq(And(x, CL1), CL2)  [ (((zext.32(C1) |.32 C2) =.32 CL2) /\ ((trunc.32(x) =.32 CL0) /\ (((C3 |.32 ((bv32"#x00000001" <<.32 width.32(C1)) -.32 bv32"#x00000001")) =.32 CL1) /\ (((((bv32"#x00000001" <<.32 width.32(C1)) -.32 bv32"#x00000001") &.32 C3) =.32 bv32"#x00000000") /\ ((((bv32"#x00000001" <<.32 width.32(C1)) -.32 bv32"#x00000001") &.32 C2) =.32 bv32"#x00000000")))))] ; /* AndOrXor:842*/
    And(icmp_eq(a, C1), icmp_eq(a, C2)) -> False  [ (C1 !=.32 C2)] ; /* AndOrXor:887-1*/
    And(icmp_eq(a, C1), icmp_ne(a, C1)) -> False; /* AndOrXor:887-2*/
    And(icmp_eq(a, C1), icmp_ne(a, C2)) -> icmp_eq(a, C1)  [ (C1 <u.32 C2)] ; /* AndOrXor:922*/
    And(icmp_eq(a, C1), icmp_ult(a, C2)) -> icmp_eq(a, C1)  [ (C1 <u.32 C2)] ; /* AndOrXor:923*/
    And(icmp_eq(a, C1), icmp_slt(a, C2)) -> icmp_eq(a, C1)  [ (C1 <s.32 C2)] ; /* AndOrXor:924*/
    And(icmp_ne(a, C1), icmp_ult(a, C2)) -> icmp_ult(a, C1)  [ ((C1 <u.32 C2) /\ (C1 =.32 (C2 -.32 bv32"#x00000001")))] ; /* AndOrXor:931*/
    And(icmp_ne(a, C1), icmp_slt(a, C2)) -> icmp_slt(a, C1)  [ ((C1 <s.32 C2) /\ (C1 =.32 (C2 -.32 bv32"#x00000001")))] ; /* AndOrXor:937*/
    And(icmp_ne(a, C1), icmp_eq(a, C2)) -> icmp_eq(a, C2)  [ (C1 <u.32 C2)] ; /* AndOrXor:940*/
    And(icmp_ne(a, C1), icmp_ugt(a, C2)) -> icmp_ugt(a, C2)  [ (C1 <u.32 C2)] ; /* AndOrXor:941*/
    And(icmp_ne(a, C1), icmp_sgt(a, C2)) -> icmp_sgt(a, C2)  [ (C1 <s.32 C2)] ; /* AndOrXor:942*/
    And(icmp_ne(a, C1), icmp_ne(a, C2)) -> icmp_ugt(add(a, neg.32(C1)), bv32"#x00000001")  [ ((C1 <u.32 C2) /\ (C1 =.32 (C2 -.32 bv32"#x00000001")))] ; /* AndOrXor:949*/
    And(icmp_ult(a, C1), icmp_eq(a, C2)) -> False  [ (C1 <u.32 C2)] ; /* AndOrXor:961*/
    And(icmp_ult(a, C1), icmp_ugt(a, C2)) -> False  [ (C1 <u.32 C2)] ; /* AndOrXor:962*/
    And(icmp_ult(a, C1), icmp_ne(a, C2)) -> icmp_ult(a, C1)  [ (C1 <u.32 C2)] ; /* AndOrXor:966*/
    And(icmp_ult(a, C1), icmp_ult(a, C2)) -> icmp_ult(a, C1)  [ (C1 <u.32 C2)] ; /* AndOrXor:967*/
    And(icmp_slt(a, C1), icmp_ne(a, C2)) -> icmp_slt(a, C1)  [ (C1 <s.32 C2)] ; /* AndOrXor:978*/
    And(icmp_slt(a, C1), icmp_slt(a, C2)) -> icmp_slt(a, C1)  [ (C1 <s.32 C2)] ; /* AndOrXor:979*/
    And(icmp_ugt(a, C1), icmp_eq(a, C2)) -> icmp_eq(a, C2)  [ (C1 <u.32 C2)] ; /* AndOrXor:988*/
    And(icmp_ugt(a, C1), icmp_ugt(a, C2)) -> icmp_ugt(a, C2)  [ (C1 <u.32 C2)] ; /* AndOrXor:989*/
    And(icmp_ugt(a, C1), icmp_ne(a, C2)) -> icmp_ugt(a, C2)  [ ((C1 <u.32 C2) /\ (C2 =.32 (C1 +.32 bv32"#x00000001")))] ; /* AndOrXor:994*/
    And(icmp_sgt(a, C1), icmp_eq(a, C2)) -> icmp_eq(a, C2)  [ (C1 <s.32 C2)] ; /* AndOrXor:1006*/
    And(icmp_sgt(a, C1), icmp_sgt(a, C2)) -> icmp_sgt(a, C2)  [ (C1 <s.32 C2)] ; /* AndOrXor:1007*/
    And(icmp_sgt(a, C1), icmp_ne(a, C2)) -> icmp_sgt(a, C2)  [ ((C1 <s.32 C2) /\ (C2 =.32 (C1 +.32 bv32"#x00000001")))] ; /* AndOrXor:1012*/
    And(Xor(op0LHS, op0RHS), C) -> Xor(op0LHS, And(op0RHS, C))  [ MaskedValueIsZero.32(op0LHS, ~.32(C))] ; /* AndOrXor:1140-1*/
    And(Or(op0LHS, op0RHS), C) -> Or(op0LHS, And(op0RHS, C))  [ MaskedValueIsZero.32(op0LHS, ~.32(C))] ; /* AndOrXor:1140-2*/
    And(Xor(op0LHS, op0RHS), C) -> Xor(And(op0LHS, C), op0RHS)  [ MaskedValueIsZero.32(op0RHS, ~.32(C))] ; /* AndOrXor:1146-1*/
    And(Or(op0LHS, op0RHS), C) -> Or(And(op0LHS, C), op0RHS)  [ MaskedValueIsZero.32(op0RHS, ~.32(C))] ; /* AndOrXor:1146-2*/
    And(sub(A, B), C) -> And(sub(bv32"#x00000000", B), C)  [ MaskedValueIsZero.32(A, (bv32"#xffffffff" >>u.32 countLeadingZeros.32(C)))] ; /* AndOrXor:1175*/
    And(shl(bv32"#x00000001", op0RHS), bv32"#x00000001") -> zext(icmp_eq(op0RHS, bv32"#x00000000")); /* AndOrXor:1191-1*/
    And(lshr(bv32"#x00000001", op0RHS), bv32"#x00000001") -> zext(icmp_eq(op0RHS, bv32"#x00000000")); /* AndOrXor:1191-2*/
    And(trunc(And(x, C1)), C2) -> And(trunc(x), CL0)  [ ((trunc.32(C1) &.32 C2) =.32 CL0)] ; /* AndOrXor:1207*/
    And(Xor(notOp0, bv32"#xffffffff"), Xor(notOp1, bv32"#xffffffff")) -> Xor(Or(notOp0, notOp1), bv32"#xffffffff"); /* AndOrXor:1230  ~A & ~B -> ~(A | B)*/
    And(Or(A, B), Xor(And(A, B), bv32"#xffffffff")) -> Xor(A, B); /* AndOrXor:1241 (A|B) & ~(A&B) => A^B*/
    And(Xor(And(A, B), bv32"#xffffffff"), Or(A, B)) -> Xor(A, B); /* AndOrXor:1247 ~(A&B) & (A|B) => A^B*/
    And(Xor(A, B), A) -> And(A, Xor(B, bv32"#xffffffff")); /* AndOrXor:1253 A & (A^B) -> A & ~B*/
    And(Or(Xor(A, bv32"#xffffffff"), B), A) -> And(A, B); /* AndOrXor:1280 (~A|B)&A -> A&B*/
    And(Xor(A, B), Xor(Xor(B, C), A)) -> And(Xor(A, B), Xor(C, bv32"#xffffffff")); /* AndOrXor:1288 (A ^ B) & ((B ^ C) ^ A) -> (A ^ B) & ~C*/
    And(Or(A, B), Xor(Xor(A, bv32"#xffffffff"), B)) -> And(A, B); /* AndOrXor:1294 (A | B) & ((~A) ^ B) -> (A & B)*/
    And(sext(x), sext(y)) -> sext(And(x, y)); /* AndOrXor:1346 (sext)*/
    And(zext(x), zext(y)) -> zext(And(x, y)); /* AndOrXor:1346 (zext)*/
    And(trunc(x), trunc(y)) -> trunc(And(x, y)); /* AndOrXor:1346 (trunc)*/
    And(sext_i1(a), b) -> select(a, b, bv32"#x00000000"); /* AndOrXor:1388*/
    And(Xor(sext_i1(a), bv32"#xffffffff"), b) -> select(a, bv32"#x00000000", b); /* AndOrXor:1395*/
    Or(And(sext(Cond), C), And(B, Xor(sext(Cond), bv32"#xffffffff"))) -> select(Cond, C, B); /* AndOrXor:1574*/
    Or(And(sext(Cond), C), And(B, sext(Xor(Cond, bv32"#xffffffff")))) -> select(Cond, C, B); /* AndOrXor:1577*/
    Or(And(sext(Cond), C), And(Xor(sext(Cond), bv32"#xffffffff"), D)) -> select(Cond, C, D); /* AndOrXor:1581*/
    Or(And(sext(Cond), C), And(sext(Xor(Cond, bv32"#xffffffff")), D)) -> select(Cond, C, D); /* AndOrXor:1583*/
    Or(icmp_eq(And(A, K1), bv32"#x00000000"), icmp_eq(And(A, K2), bv32"#x00000000")) -> icmp_ne(And(A, Or(K1, K2)), Or(K1, K2))  [ (isPowerOf2.32(K1) /\ isPowerOf2.32(K2))] ; /* AndOrXor:1593*/
    Or(icmp_ult(add_i29(A, C1), C3), icmp_ult(add(A, C2), C3)) -> icmp_ult(add(And(A, ~.32(CL0)), CL1), C3)  [ (((C1 ^.32 C2) =.32 CL0) /\ ((umax.32(C1, C2) =.32 CL1) /\ ((C1 >u.32 C3) /\ ((C2 >u.32 C3) /\ (isPowerOf2.32((C1 ^.32 C2)) /\ (isPowerOf2.32((neg.32(C2) ^.32 neg.32(C1))) /\ (((neg.32(C2) ^.32 neg.32(C1)) =.32 ((C3 -.32 C2) ^.32 (C3 -.32 C1))) /\ (abs.32((C1 -.32 C2)) >u.32 C3))))))))] ; /* AndOrXor:1628-1*/
    Or(icmp_ule(add_i29(A, C1), C3), icmp_ule(add(A, C2), C3)) -> icmp_ule(add(And(A, ~.32(CL0)), CL1), C3)  [ (((C1 ^.32 C2) =.32 CL0) /\ ((umax.32(C1, C2) =.32 CL1) /\ ((C1 >u.32 C3) /\ ((C2 >u.32 C3) /\ (isPowerOf2.32((C1 ^.32 C2)) /\ (isPowerOf2.32((neg.32(C2) ^.32 neg.32(C1))) /\ (((neg.32(C2) ^.32 neg.32(C1)) =.32 ((C3 -.32 C2) ^.32 (C3 -.32 C1))) /\ (abs.32((C1 -.32 C2)) >u.32 C3))))))))] ; /* AndOrXor:1628-2*/
    Or(icmp_ugt(a, b), icmp_eq(a, b)) -> icmp_uge(a, b); /* AndOrXor:1683-1*/
    Or(icmp_uge(a, b), icmp_ne(a, b)) -> True; /* AndOrXor:1683-2*/
    Or(icmp_eq(B, bv32"#x00000000"), icmp_ult(A, B)) -> icmp_uge(add(B, bv32"#xffffffff"), A); /* AndOrXor:1704*/
    Or(icmp_eq(B, bv32"#x00000000"), icmp_ugt(B, A)) -> icmp_uge(add(B, bv32"#xffffffff"), A); /* AndOrXor:1705*/
    Or(icmp_ne(A, bv32"#x00000000"), icmp_ne(B, bv32"#x00000000")) -> icmp_ne(Or(A, B), bv32"#x00000000"); /* AndOrXor:1733*/
    Or(icmp_ult(add(X, C3), C1), icmp_eq(X, C2)) -> icmp_ule(add(X, C3), C1)  [ ((C2 +.32 C3) =.32 C1)] ; /* AndOrXor:1740*/
    Or(icmp_eq(X, C1), icmp_eq(X, C2)) -> icmp_eq(And(X, ~.32(CL0)), C1)  [ (((C1 ^.32 C2) =.32 CL0) /\ ((C1 <u.32 C2) /\ isPowerOf2.32((C1 ^.32 C2))))] ; /* AndOrXor:1795*/
    Or(icmp_eq(X, C1), icmp_eq(X, C2)) -> icmp_ult(add(X, neg.32(C1)), bv32"#x00000002")  [ (C1 =.32 (C2 -.32 bv32"#x00000001"))] ; /* AndOrXor:1806*/
    Or(icmp_eq(X, C1), icmp_ne(X, C2)) -> icmp_ne(X, C2)  [ (C1 <u.32 C2)] ; /* AndOrXor:1818*/
    Or(icmp_eq(X, C1), icmp_ult(X, C2)) -> icmp_ult(X, C2)  [ (C1 <u.32 C2)] ; /* AndOrXor:1819*/
    Or(icmp_eq(X, C1), icmp_slt(X, C2)) -> icmp_slt(X, C2)  [ (C1 <s.32 C2)] ; /* AndOrXor:1820*/
    Or(icmp_ne(X, C1), icmp_eq(X, C2)) -> icmp_ne(X, C1)  [ (C1 <u.32 C2)] ; /* AndOrXor:1827*/
    Or(icmp_ne(X, C1), icmp_ugt(X, C2)) -> icmp_ne(X, C1)  [ (C1 <u.32 C2)] ; /* AndOrXor:1828*/
    Or(icmp_ne(X, C1), icmp_sgt(X, C2)) -> icmp_ne(X, C1)  [ (C1 <s.32 C2)] ; /* AndOrXor:1829*/
    Or(icmp_ne(X, C1), icmp_ne(X, C2)) -> True  [ (C1 <u.32 C2)] ; /* AndOrXor:1831*/
    Or(icmp_ne(X, C1), icmp_ult(X, C2)) -> True  [ (C1 <u.32 C2)] ; /* AndOrXor:1832*/
    Or(icmp_ne(X, C1), icmp_slt(X, C2)) -> True  [ (C1 <s.32 C2)] ; /* AndOrXor:1833*/
    Or(icmp_ult(X, C1), icmp_ugt(X, C2)) -> icmp_ult(X, C1)  [ ((C1 <u.32 C2) /\ (C2 =.32 bv32"#xffffffff"))] ; /* AndOrXor:1844*/
    Or(icmp_ult(X, C1), icmp_ne(X, C2)) -> icmp_ne(X, C2)  [ (C1 <u.32 C2)] ; /* AndOrXor:1849*/
    Or(icmp_ult(X, C1), icmp_ult(X, C2)) -> icmp_ult(X, C2)  [ (C1 <u.32 C2)] ; /* AndOrXor:1850*/
    Or(icmp_slt(X, C1), icmp_sgt(X, C2)) -> icmp_slt(X, C1)  [ ((C1 <s.32 C2) /\ (C2 =.32 (bv32"#x00000001" <<.32 (width.32(C2) -.32 bv32"#x00000001"))))] ; /* AndOrXor:1864*/
    Or(icmp_slt(X, C1), icmp_ne(X, C2)) -> icmp_ne(X, C2)  [ (C1 <s.32 C2)] ; /* AndOrXor:1869*/
    Or(icmp_slt(X, C1), icmp_slt(X, C2)) -> icmp_slt(X, C2)  [ (C1 <s.32 C2)] ; /* AndOrXor:1870*/
    Or(icmp_ugt(X, C1), icmp_eq(X, C2)) -> icmp_ugt(X, C1)  [ (C1 <u.32 C2)] ; /* AndOrXor:1879*/
    Or(icmp_ugt(X, C1), icmp_ugt(X, C2)) -> icmp_ugt(X, C1)  [ (C1 <u.32 C2)] ; /* AndOrXor:1880*/
    Or(icmp_ugt(X, C1), icmp_ne(X, C2)) -> True  [ (C1 <u.32 C2)] ; /* AndOrXor:1884*/
    Or(icmp_ugt(X, C1), icmp_ult(X, C2)) -> True  [ (C1 <u.32 C2)] ; /* AndOrXor:1885*/
    Or(icmp_sgt(X, C1), icmp_eq(X, C2)) -> icmp_sgt(X, C1)  [ (C1 <s.32 C2)] ; /* AndOrXor:1894*/
    Or(icmp_sgt(X, C1), icmp_sgt(X, C2)) -> icmp_sgt(X, C1)  [ (C1 <s.32 C2)] ; /* AndOrXor:1895*/
    Or(icmp_sgt(X, C1), icmp_ne(X, C2)) -> True  [ (C1 <s.32 C2)] ; /* AndOrXor:1899*/
    Or(icmp_sgt(X, C1), icmp_slt(X, C2)) -> True  [ (C1 <s.32 C2)] ; /* AndOrXor:1900*/
    Or(And(Or(A, B), C1), And(B, C2)) -> Or(And(A, C1), B)  [ ((C1 ^.32 C2) =.32 bv32"#xffffffff")] ; /* AndOrXor:1979*/
    Or(And(Xor(A, B), C1), And(B, C2)) -> Xor(And(A, C1), B)  [ ((C1 ^.32 C2) =.32 bv32"#xffffffff")] ; /* AndOrXor:2008*/
    Or(And(x, C1), C) -> And(Or(x, C), CL0)  [ (((C |.32 C1) =.32 CL0) /\ ((C &.32 C1) !=.32 bv32"#x00000000"))] ; /* AndOrXor:2052  (X & C1) | C2 --> (X | C2) & (C1|C2)*/
    Or(Xor(x, C1), C) -> Xor(Or(x, C), CL0)  [ ((C1 &.32 ~.32(C)) =.32 CL0)] ; /* AndOrXor:2063  (X ^ C1) | C2 --> (X | C2) ^ (C1 & ~C2)*/
    Or(Xor(A, C1), op1) -> Xor(Or(A, op1), C1)  [ MaskedValueIsZero.32(op1, C1)] ; /* AndOrXor:2095   (X^C)|Y -> (X|Y)^C iff Y&C == 0*/
    Or(And(Xor(A, bv32"#xffffffff"), B), A) -> Or(A, B); /* AndOrXor:2113   ((~A & B) | A) -> (A | B)*/
    Or(And(A, B), Xor(A, bv32"#xffffffff")) -> Or(Xor(A, bv32"#xffffffff"), B); /* AndOrXor:2118   ((A & B) | ~A) -> (~A | B)*/
    Or(And(A, Xor(B, bv32"#xffffffff")), Xor(A, B)) -> Xor(A, B); /* AndOrXor:2123   (A & (~B)) | (A ^ B) -> (A ^ B)*/
    Or(And(Or(B, V2), C1), And(B, C2)) -> And(Or(B, V2), CL0)  [ (((C1 |.32 C2) =.32 CL0) /\ (((C1 &.32 C2) =.32 bv32"#x00000000") /\ MaskedValueIsZero.32(V2, ~.32(C1))))] ; /* AndOrXor:2142*/
    Or(And(Or(V1, C3), C1), And(Or(V1, C4), C2)) -> And(Or(V1, CL0), CL1)  [ (((C1 |.32 C2) =.32 CL1) /\ (((C3 |.32 C4) =.32 CL0) /\ (((C1 &.32 C2) =.32 bv32"#x00000000") /\ (((C3 &.32 ~.32(C1)) =.32 bv32"#x00000000") /\ ((C4 &.32 ~.32(C2)) =.32 bv32"#x00000000")))))] ; /* AndOrXor:2160*/
    Or(And(A, Xor(D, bv32"#xffffffff")), And(Xor(A, bv32"#xffffffff"), D)) -> Xor(A, D); /* AndOrXor:2188*/
    Or(Xor(A, B), Xor(Xor(B, C), A)) -> Or(Xor(A, B), C); /* AndOrXor:2231  (A ^ B) | ((B ^ C) ^ A) -> (A ^ B) | C*/
    Or(And(Or(B, C), A), B) -> Or(B, And(A, C)); /* AndOrXor:2243  ((B | C) & A) | B -> B | (A & C)*/
    Or(Xor(A, bv32"#xffffffff"), Xor(B, bv32"#xffffffff")) -> Xor(And(A, B), bv32"#xffffffff"); /* AndOrXor:2247  (~A | ~B) == (~(A & B))*/
    Or(op0, Xor(op0, B)) -> Or(op0, B); /* AndOrXor:2263*/
    Or(A, Xor(Xor(A, bv32"#xffffffff"), B)) -> Or(A, Xor(B, bv32"#xffffffff")); /* AndOrXor:2264*/
    Or(And(A, B), Xor(A, B)) -> Or(A, B); /* AndOrXor:2265*/
    Or(A, Xor(Or(A, B), bv32"#xffffffff")) -> Or(A, Xor(B, bv32"#xffffffff")); /* AndOrXor:2284*/
    Or(A, Xor(Xor(A, B), bv32"#xffffffff")) -> Or(A, Xor(B, bv32"#xffffffff")); /* AndOrXor:2285*/
    Or(And(A, B), Xor(Xor(A, bv32"#xffffffff"), B)) -> Xor(Xor(A, bv32"#xffffffff"), B); /* AndOrXor:2297*/
    Or(zext(A), zext(B)) -> zext(Or(A, B)); /* AndOrXor:2321-1*/
    Or(sext(A), sext(B)) -> sext(Or(A, B)); /* AndOrXor:2321-2*/
    Or(trunc(A), trunc(B)) -> trunc(Or(A, B)); /* AndOrXor:2321-3*/
    Or(sext_i1(A), op1) -> select(A, bv32"#xffffffff", op1); /* AndOrXor:2356*/
    Or(Or(A, C1), op1) -> Or(Or(A, op1), C1); /* AndOrXor:2367*/
    Or(select(x, A, B), select(x, C, D)) -> select(x, Or(A, C), Or(B, D)); /* AndOrXor:2375*/
    Xor(And(Xor(nx, bv32"#xffffffff"), y), bv32"#xffffffff") -> Or(nx, Xor(y, bv32"#xffffffff")); /* AndOrXor:2416*/
    Xor(Or(Xor(nx, bv32"#xffffffff"), y), bv32"#xffffffff") -> And(nx, Xor(y, bv32"#xffffffff")); /* AndOrXor:2417*/
    Xor(And(x, y), bv32"#xffffffff") -> Or(Xor(x, bv32"#xffffffff"), Xor(y, bv32"#xffffffff")); /* AndOrXor:2429*/
    Xor(Or(x, y), bv32"#xffffffff") -> And(Xor(x, bv32"#xffffffff"), Xor(y, bv32"#xffffffff")); /* AndOrXor:2430*/
    Xor(ashr(Xor(x, bv32"#xffffffff"), y), bv32"#xffffffff") -> ashr(x, y); /* AndOrXor:2443*/
    Xor(icmp_slt(x, y), bv32"#xffffffff") -> icmp_sge(x, y); /* AndOrXor:2453*/
    Xor(CL0, bv32"#x00000001") -> zext(icmp_sge(x, y))  [ (zext.32(icmp_slt.32(x, y)) =.32 CL0)] ; /* AndOrXor:2459-1*/
    Xor(CL0, bv32"#xffffffff") -> sext(icmp_sge(x, y))  [ (sext.32(icmp_slt.32(x, y)) =.32 CL0)] ; /* AndOrXor:2459-2*/
    Xor(sub(C, x), bv32"#xffffffff") -> add(x, CL0)  [ ((bv32"#xffffffff" -.32 C) =.32 CL0)] ; /* AndOrXor:2475*/
    Xor(add(x, C), bv32"#xffffffff") -> sub(CL0, x)  [ ((bv32"#xffffffff" -.32 C) =.32 CL0)] ; /* AndOrXor:2486*/
    Xor(add(x, C), C1) -> add(x, CL0)  [ (((C +.32 C1) =.32 CL0) /\ isSignBit.32(C1))] ; /* AndOrXor:2494*/
    Xor(Or(x, C1), C2) -> Xor(x, CL0)  [ (((C1 ^.32 C2) =.32 CL0) /\ MaskedValueIsZero.32(x, C1))] ; /* AndOrXor:2500*/
    Xor(lshr(Xor(x, C1), C2), C3) -> Xor(lshr(x, C2), CL0)  [ (((C1 >>u.32 C2) ^.32 C3) =.32 CL0)] ; /* AndOrXor:2515   ((X^C1) >> C2)^C3 -> (X>>C2) ^ ((C1>>C2)^C3)*/
    Xor(Or(a, op1), op1) -> And(a, Xor(op1, bv32"#xffffffff")); /* AndOrXor:2581  (B|A)^B -> A & ~B*/
    Xor(And(a, op1), op1) -> And(Xor(a, bv32"#xffffffff"), op1); /* AndOrXor:2587  (B&A)^A -> ~B & A*/
    Xor(And(a, b), Or(a, b)) -> Xor(a, b); /* AndOrXor:2595*/
    Xor(Or(a, Xor(b, bv32"#xffffffff")), Or(Xor(a, bv32"#xffffffff"), b)) -> Xor(a, b); /* AndOrXor:2607*/
    Xor(And(a, Xor(b, bv32"#xffffffff")), And(Xor(a, bv32"#xffffffff"), b)) -> Xor(a, b); /* AndOrXor:2617*/
    Xor(Xor(a, c), Or(a, b)) -> Xor(And(Xor(a, bv32"#xffffffff"), b), c); /* AndOrXor:2627*/
    Xor(And(a, b), Xor(a, b)) -> Or(a, b); /* AndOrXor:2647*/
    Xor(And(a, Xor(b, bv32"#xffffffff")), Xor(a, bv32"#xffffffff")) -> Xor(And(a, b), bv32"#xffffffff"); /* AndOrXor:2658*/
    Xor(icmp_ule(a, b), icmp_ne(a, b)) -> icmp_uge(a, b); /* AndOrXor:2663*/
    Xor(zext(a), zext(b)) -> zext(Xor(a, b)); /* AndOrXor:2681-1*/
    Xor(sext(a), sext(b)) -> sext(Xor(a, b)); /* AndOrXor:2681-2*/
    Xor(trunc(a), trunc(b)) -> trunc(Xor(a, b)); /* AndOrXor:2681-3*/
    zext_11(X0) -> zext(X0); /**/
    icmp_ugt(X0, X1) -> icmp(X0, X1); /**/
    add_i29(X0, X1) -> add(X0, X1); /**/
    sext_i1(X0) -> sext(X0); /**/
    icmp_sgt(X0, X1) -> icmp(X0, X1); /**/
    sext_11(X0) -> sext(X0); /**/
    icmp_slt(X0, X1) -> icmp(X0, X1); /**/
    icmp_ule(X0, X1) -> icmp(X0, X1); /**/
    icmp_uge(X0, X1) -> icmp(X0, X1); /**/
    trunc_11(X0) -> trunc(X0); /**/
    icmp_eq(X0, X1) -> icmp(X0, X1); /**/
    icmp_ne(X0, X1) -> icmp(X0, X1); /**/
    icmp_sge(X0, X1) -> icmp(X0, X1); /**/
    icmp_ult(X0, X1) -> icmp(X0, X1); /**/

NON-STANDARD IRREGULAR

QUERY loops