THEORY bitvectors-cast;
LOGIC QF_UFBV;
SOLVER external;
SIGNATURE Xor, add_i1, lshr, sub_nuw, zext_i1, select, sub, shl_nsw, sub_nsw, add_nuw, add, shl_nuw, mul, sub_i1, add_nsw, sext, sdiv_i9, sext_i1, Or, And, sdiv, zext, shl, ashr, 

RULES
    add(add(Xor(Or(Z, C2), C1), bv32"#x00000001"), RHS) -> sub(RHS, And(Z, C1))  [ (C2 =.32 ~.32(C1))] ; /* AddSub:1040*/
    add(add(Xor(And(Z, C1), C1), bv32"#x00000001"), RHS) -> sub(RHS, Or(Z, ~.32(C1))); /* AddSub:1043*/
    add(Xor(And(Z, C2), C1), RHS) -> sub(RHS, Or(Z, ~.32(C2)))  [ ((countTrailingZeros.32(C1) =.32 bv32"#x00000000") /\ (C1 =.32 (C2 +.32 bv32"#x00000001")))] ; /* AddSub:1063*/
    add(x, C) -> Xor(x, C)  [ isSignBit.32(C)] ; /* AddSub:1088*/
    add(zext_i1(a), b) -> select(a, add(b, bv32"#x00000001"), b); /* AddSub:1098*/
    add(Xor(Y, C2), C1) -> ashr(shl(Y, CL0), CL0)  [ (((width.32(C1) -.32 (width.32(C1) -.32 (log2.32(C2) -.32 bv32"#x00000001"))) =.32 CL0) /\ ((C1 =.32 neg.32(C2)) /\ (isPowerOf2.32(C2) /\ not(MaskedValueIsZero.32(C2, (bv32"#xffffffff" <<.32 (width.32(C1) -.32 (width.32(C1) -.32 (log2.32(C2) -.32 bv32"#x00000001")))))))))] ; /* AddSub:1111*/
    add(Xor(Y, C2), C1) -> ashr(shl(Y, CL0), CL0)  [ (((width.32(C1) -.32 (log2.32(C1) -.32 bv32"#x00000001")) =.32 CL0) /\ ((C2 =.32 neg.32(C1)) /\ (isPowerOf2.32(C1) /\ MaskedValueIsZero.32(Y, (bv32"#xffffffff" <<.32 (log2.32(C1) +.32 bv32"#x00000001"))))))] ; /* AddSub:1126-1*/
    add(Xor(Y, C2), C1) -> ashr(shl(Y, CL0), CL0)  [ (((width.32(C2) -.32 (log2.32(C2) -.32 bv32"#x00000001")) =.32 CL0) /\ ((C2 =.32 neg.32(C1)) /\ (isPowerOf2.32(C2) /\ MaskedValueIsZero.32(Y, (bv32"#xffffffff" <<.32 (log2.32(C2) +.32 bv32"#x00000001"))))))] ; /* AddSub:1126-2*/
    add(Xor(Y, C2), C1) -> sub(CL0, Y)  [ (((C1 +.32 C2) =.32 CL0) /\ (hasOneUse.32 /\ (isPowerOf2.32((C2 +.32 bv32"#x00000001")) /\ ((C2 |.32 computeKnownZeroBits.32(Y)) =.32 bv32"#xffffffff"))))] ; /* AddSub:1131*/
    add(Xor(a, C1), C2) -> add(a, CL0)  [ (((C1 ^.32 C2) =.32 CL0) /\ isSignBit.32(C1))] ; /* AddSub:1142*/
    add_i1(x, y) -> Xor(x, y); /* AddSub:1152*/
    add(b, b) -> shl(b, bv32"#x00000001"); /* AddSub:1156*/
    add_nsw(b, b) -> shl_nsw(b, bv32"#x00000001"); /* AddSub:1156-2*/
    add_nuw(b, b) -> shl_nuw(b, bv32"#x00000001"); /* AddSub:1156-3*/
    add(sub(bv32"#x00000000", a), b) -> sub(b, a); /* AddSub:1164*/
    add(sub(bv32"#x00000000", a), sub(bv32"#x00000000", b)) -> sub(bv32"#x00000000", add(a, b)); /* AddSub:1165*/
    add(a, sub(bv32"#x00000000", b)) -> sub(a, b); /* AddSub:1176*/
    add(x, y) -> Or(x, y)  [ ((computeKnownZeroBits.32(x) |.32 computeKnownZeroBits.32(y)) =.32 bv32"#xffffffff")] ; /* AddSub:1184*/
    add(Xor(x, bv32"#xffffffff"), C) -> sub(CL0, x)  [ ((C -.32 bv32"#x00000001") =.32 CL0)] ; /* AddSub:1202*/
    add(And(x, C2), C1) -> And(add(x, C1), C2)  [ (hasOneUse.32 /\ (~.32(((C1 &.32 neg.32(C1)) -.32 bv32"#x00000001")) =.32 (~.32(((C1 &.32 neg.32(C1)) -.32 bv32"#x00000001")) &.32 C2)))] ; /* AddSub:1206*/
    add(select(x, bv32"#x00000000", sub(n, a)), a) -> select(x, a, n)  [ hasOneUse.32] ; /* AddSub:1251*/
    add(select(x, sub(n, a), bv32"#x00000000"), a) -> select(x, n, a)  [ hasOneUse.32] ; /* AddSub:1255*/
    add(sext(x), C) -> sext(add_nsw(x, CL0))  [ ((trunc.32(C) =.32 CL0) /\ (hasOneUse.32 /\ (WillNotOverflowSignedAdd.32(x, trunc.32(C)) /\ ((C &.32 (bv32"#xffffffff" <<.32 (width.32(x) -.32 bv32"#x00000001"))) =.32 bv32"#x00000000"))))] ; /* AddSub:1265*/
    add(sext(x), sext(y)) -> sext(add_nsw(x, y))  [ ((hasOneUse.32 \/ hasOneUse.32) /\ WillNotOverflowSignedAdd.32(x, y))] ; /* AddSub:1278*/
    add(And(a, b), Xor(a, b)) -> Or(a, b); /* AddSub:1295*/
    add(And(a, b), Or(a, b)) -> add(a, b); /* AddSub:1309*/
    add_nsw(And(a, b), Or(a, b)) -> add_nsw(a, b); /* AddSub:1309-2*/
    add_nuw(And(a, b), Or(a, b)) -> add_nuw(a, b); /* AddSub:1309-3*/
    add(lhs, rhs) -> add_nsw(lhs, rhs)  [ WillNotOverflowSignedAdd.32(lhs, rhs)] ; /* AddSub:1334*/
    add(lhs, rhs) -> add_nuw(lhs, rhs)  [ WillNotOverflowUnsignedAdd.32(lhs, rhs)] ; /* AddSub:1338*/
    sub(x, sub(bv32"#x00000000", a)) -> add(x, a); /* AddSub:1539*/
    sub(x, C) -> add(x, neg.32(C)); /* AddSub:1539-2*/
    sub_nsw(x, sub_nsw(bv32"#x00000000", a)) -> add_nsw(x, a); /* AddSub:1546*/
    sub_nsw(x, C) -> add_nsw(x, neg.32(C))  [ (C !=.32 (bv32"#x00000001" <<.32 (width.32(C) -.32 bv32"#x00000001")))] ; /* AddSub:1549*/
    sub_i1(x, y) -> Xor(x, y); /* AddSub:1556*/
    sub(bv32"#xffffffff", a) -> Xor(a, bv32"#xffffffff"); /* AddSub:1560*/
    sub(C, Xor(x, bv32"#xffffffff")) -> add(x, CL0)  [ ((C +.32 bv32"#x00000001") =.32 CL0)] ; /* AddSub:1564*/
    sub(C, add(X, C2)) -> sub(CL0, X)  [ ((C -.32 C2) =.32 CL0)] ; /* AddSub:1574*/
    sub(bv32"#x00000000", zext_i1(X)) -> sext(X); /* AddSub:1582*/
    sub(bv32"#x00000000", sext_i1(X)) -> zext(X); /* AddSub:1587*/
    sub(bv32"#x00000000", lshr(x, C)) -> ashr(x, C)  [ (C =.32 (width.32((x >>u.32 C)) -.32 bv32"#x00000001"))] ; /* AddSub:1599*/
    sub(bv32"#x00000000", ashr(x, C)) -> lshr(x, C)  [ (C =.32 (width.32((x >>s.32 C)) -.32 bv32"#x00000001"))] ; /* AddSub:1604*/
    sub(X, add(X, Y)) -> sub(bv32"#x00000000", Y); /* AddSub:1614*/
    sub(sub(X, Y), X) -> sub(bv32"#x00000000", Y); /* AddSub:1619*/
    sub(Or(A, B), Xor(A, B)) -> And(A, B); /* AddSub:1624*/
    sub(Or(Y, Op1), Op1) -> And(Xor(Op1, bv32"#xffffffff"), Y)  [ hasOneUse.32] ; /* AddSub:1633*/
    sub(X, sub(Y, Z)) -> add(X, sub(Z, Y))  [ hasOneUse.32] ; /* AddSub:1648*/
    sub(X, And(X, Y)) -> And(X, Xor(Y, bv32"#xffffffff"))  [ hasOneUse.32] ; /* AddSub:1654*/
    sub(bv32"#x00000000", sdiv_i9(X, C)) -> sdiv(X, neg.32(C))  [ (hasOneUse.32 /\ ((C !=.32 bv32"#x00000001") /\ (C !=.32 (bv32"#x00000001" <<.32 (width.32(C) -.32 bv32"#x00000001")))))] ; /* AddSub:1660*/
    sub(bv32"#x00000000", shl(C, Y)) -> shl(neg.32(C), Y)  [ hasOneUse.32] ; /* AddSub:1665*/
    sub(bv32"#x00000000", shl(sub(bv32"#x00000000", X), Y)) -> shl(X, Y)  [ hasOneUse.32] ; /* AddSub:1665-2*/
    sub(X, mul(A, sub(bv32"#x00000000", B))) -> add(X, mul(A, B))  [ hasOneUse.32] ; /* AddSub:1672*/
    sub(X, mul(A, C)) -> add(X, mul(A, neg.32(C)))  [ hasOneUse.32] ; /* AddSub:1678*/
    sub(A, B) -> sub_nsw(A, B)  [ WillNotOverflowSignedSub.32(A, B)] ; /* AddSub:1693*/
    sub(A, B) -> sub_nuw(A, B)  [ WillNotOverflowUnsignedSub.32(A, B)] ; /* AddSub:1697*/
    add_i1(X0, X1) -> add(X0, X1); /**/
    sub_nsw(X0, X1) -> sub(X0, X1); /**/
    sub_i1(X0, X1) -> sub(X0, X1); /**/
    sext_i1(X0) -> sext(X0); /**/
    zext_i1(X0) -> zext(X0); /**/
    shl_nuw(X0, X1) -> shl(X0, X1); /**/
    add_nuw(X0, X1) -> add(X0, X1); /**/
    add_nsw(X0, X1) -> add(X0, X1); /**/
    shl_nsw(X0, X1) -> shl(X0, X1); /**/
    sub_nuw(X0, X1) -> sub(X0, X1); /**/
    sdiv_i9(X0, X1) -> sdiv(X0, X1); /**/

NON-STANDARD IRREGULAR

QUERY loops