THEORY bitvectors-cast;
LOGIC QF_UFBV;
SOLVER external;
SIGNATURE srem_i9, lshr, icmp_ne, mul_nuw_i7, shl_i7, udiv_exact_i9, select, icmp_eq, sub, shl_nsw_i7, zext_Ty, shl_nsw_i9, srem_i11, udiv_exact_i13, ashr, udiv_exact, add, ashr_exact, mul_nuw, shl_nuw, sdiv_exact_i33, mul, mul_nuw_nsw, mul_nsw, And, srem, urem_i9, mul_nsw_nuw, urem, shl_i13, udiv_i13, mul_nsw_i7, sdiv_i7, mul_i1, sdiv_i5, icmp, urem_i33, udiv_i5, udiv_i7, icmp_ult, lshr_i9, sdiv, mul_i11, udiv_i9, shl_i33, shl_nuw_i7, sdiv_exact, lshr_exact, shl_nsw_nuw_i9, mul_nuw_nsw_i7, shl_i23, mul_nuw_i11, udiv, zext, shl, sub_nsw_i11, shl_nuw_i9, 

RULES
    udiv(X, lshr(shl_i33(bv32"#x00000001", A), B)) -> udiv(X, shl(bv32"#x00000001", sub(A, B)))  [ hasOneUse.32] ; /* simplifyValueKnownNonZero 1*/
    udiv(X, lshr(A, B)) -> udiv(X, lshr_exact(A, B))  [ (isPowerOf2.32(A) /\ hasOneUse.32)] ; /* simplifyValueKnownNonZero 2*/
    udiv(X, shl(A, B)) -> udiv(X, shl_nuw(A, B))  [ (isPowerOf2.32(A) /\ hasOneUse.32)] ; /* simplifyValueKnownNonZero 3*/
    sdiv(X, lshr(shl_i33(bv32"#x00000001", A), B)) -> sdiv(X, shl(bv32"#x00000001", sub(A, B)))  [ hasOneUse.32] ; /* simplifyValueKnownNonZero 4*/
    sdiv(X, lshr(A, B)) -> sdiv(X, lshr_exact(A, B))  [ (isPowerOf2.32(A) /\ hasOneUse.32)] ; /* simplifyValueKnownNonZero 5*/
    sdiv(X, shl(A, B)) -> sdiv(X, shl_nuw(A, B))  [ (isPowerOf2.32(A) /\ hasOneUse.32)] ; /* simplifyValueKnownNonZero 6*/
    urem(X, lshr(shl_i33(bv32"#x00000001", A), B)) -> urem(X, shl(bv32"#x00000001", sub(A, B)))  [ hasOneUse.32] ; /* simplifyValueKnownNonZero 7*/
    urem(X, lshr(A, B)) -> urem(X, lshr_exact(A, B))  [ (isPowerOf2.32(A) /\ hasOneUse.32)] ; /* simplifyValueKnownNonZero 8*/
    urem(X, shl(A, B)) -> urem(X, shl_nuw(A, B))  [ (isPowerOf2.32(A) /\ hasOneUse.32)] ; /* simplifyValueKnownNonZero 9*/
    srem(X, lshr(shl_i33(bv32"#x00000001", A), B)) -> srem(X, shl(bv32"#x00000001", sub(A, B)))  [ hasOneUse.32] ; /* simplifyValueKnownNonZero 10*/
    srem(X, lshr(A, B)) -> srem(X, lshr_exact(A, B))  [ (isPowerOf2.32(A) /\ hasOneUse.32)] ; /* simplifyValueKnownNonZero 11*/
    srem(X, shl(A, B)) -> srem(X, shl_nuw(A, B))  [ (isPowerOf2.32(A) /\ hasOneUse.32)] ; /* simplifyValueKnownNonZero 12*/
    mul(x, bv32"#xffffffff") -> sub(bv32"#x00000000", x); /* 152*/
    mul(shl_i7(x, C2), C1) -> mul(x, CL0)  [ ((C1 <<.32 C2) =.32 CL0)] ; /* 160*/
    mul_i11(x, C1) -> shl(x, CL0)  [ ((log2.32(C1) =.32 CL0) /\ isPowerOf2.32(C1))] ; /* 168*/
    mul_nuw_i11(x, C1) -> shl_nuw(x, CL0)  [ ((log2.32(C1) =.32 CL0) /\ isPowerOf2.32(C1))] ; /* 168-2*/
    mul(sub(Y, X), C) -> mul(sub(X, Y), CL0)  [ ((abs.32(C) =.32 CL0) /\ ((C <s.32 bv32"#x00000000") /\ isPowerOf2.32(abs.32(C))))] ; /* 201*/
    mul(add(Y, C1), C) -> mul(sub(neg.32(C1), Y), CL0)  [ ((abs.32(C) =.32 CL0) /\ ((C <s.32 bv32"#x00000000") /\ isPowerOf2.32(abs.32(C))))] ; /* 203*/
    mul(add(X, C1), Op1) -> add(mul(X, Op1), mul(C1, Op1)); /* 229*/
    mul(sub(bv32"#x00000000", X), sub(bv32"#x00000000", Y)) -> mul(X, Y); /* 239*/
    mul(udiv_exact(X, Y), Y) -> X; /* 265*/
    mul(sdiv_exact(X, Y), Y) -> X; /* 265-2*/
    mul(udiv_exact(X, Y), sub(bv32"#x00000000", Y)) -> sub(bv32"#x00000000", X); /* 266*/
    mul(sdiv_exact(X, Y), sub(bv32"#x00000000", Y)) -> sub(bv32"#x00000000", X); /* 266-2*/
    mul(udiv_i5(X, Y), Y) -> sub(X, urem(X, Y)); /* 275*/
    mul(sdiv_i5(X, Y), Y) -> sub(X, srem(X, Y)); /* 275-2*/
    mul(sdiv_i5(X, Y), sub(bv32"#x00000000", Y)) -> sub(srem(X, Y), X); /* 276*/
    mul(udiv_i5(X, Y), sub(bv32"#x00000000", Y)) -> sub(urem(X, Y), X); /* 276-2*/
    mul_i1(X, Y) -> And(X, Y); /* 283*/
    mul(shl(bv32"#x00000001", Y), Op1) -> shl(Op1, Y); /* 290 & 292*/
    mul(Op0, Op1) -> And(sub(bv32"#x00000000", Op0), Op1)  [ MaskedValueIsZero.32(Op0, bv32"#xfffffffe")] ; /* 304*/
    udiv(X, select(c, Y, bv32"#x00000000")) -> udiv(X, Y); /* SimplifyDivRemOfSelect*/
    sdiv(sdiv_i7(X, C1), C2) -> sdiv(X, CL0)  [ (((C1 *.32 C2) =.32 CL0) /\ WillNotOverflowSignedMul.32(C1, C2))] ; /* 735*/
    udiv(udiv_i7(X, C1), C2) -> udiv(X, CL0)  [ (((C1 *.32 C2) =.32 CL0) /\ WillNotOverflowUnsignedMul.32(C1, C2))] ; /* 735*/
    sdiv(mul_nsw_i7(X, C1), C2) -> sdiv(X, CL0)  [ (((C2 /s.32 C1) =.32 CL0) /\ ((C2 %s.32 C1) =.32 bv32"#x00000000"))] ; /* 748*/
    sdiv_exact(mul_nsw_i7(X, C1), C2) -> sdiv_exact(X, CL0)  [ (((C2 /s.32 C1) =.32 CL0) /\ ((C2 %s.32 C1) =.32 bv32"#x00000000"))] ; /* 748*/
    udiv(mul_nuw_i7(X, C1), C2) -> udiv(X, CL0)  [ (((C2 /u.32 C1) =.32 CL0) /\ ((C2 %u.32 C1) =.32 bv32"#x00000000"))] ; /* 748*/
    udiv_exact(mul_nuw_i7(X, C1), C2) -> udiv_exact(X, CL0)  [ (((C2 /u.32 C1) =.32 CL0) /\ ((C2 %u.32 C1) =.32 bv32"#x00000000"))] ; /* 748*/
    sdiv(mul_nsw_i7(X, C1), C2) -> mul_nsw(X, CL0)  [ (((C1 /s.32 C2) =.32 CL0) /\ ((C1 %s.32 C2) =.32 bv32"#x00000000"))] ; /* 756*/
    udiv(mul_nuw_i7(X, C1), C2) -> mul_nuw(X, CL0)  [ (((C1 /u.32 C2) =.32 CL0) /\ ((C1 %u.32 C2) =.32 bv32"#x00000000"))] ; /* 756*/
    udiv(mul_nuw_nsw_i7(X, C1), C2) -> mul_nuw_nsw(X, CL0)  [ (((C1 /u.32 C2) =.32 CL0) /\ ((C1 %u.32 C2) =.32 bv32"#x00000000"))] ; /* 756*/
    sdiv(shl_nsw_i9(X, C1), C2) -> sdiv(X, CL0)  [ (((C2 /s.32 (bv32"#x00000001" <<.32 C1)) =.32 CL0) /\ (((C2 %s.32 (bv32"#x00000001" <<.32 C1)) =.32 bv32"#x00000000") /\ (C1 !=.32 (width.32(C1) -.32 bv32"#x00000001"))))] ; /* 764*/
    sdiv_exact(shl_nsw_i7(X, C1), C2) -> sdiv_exact(X, CL0)  [ (((C2 /s.32 (bv32"#x00000001" <<.32 C1)) =.32 CL0) /\ (((C2 %s.32 (bv32"#x00000001" <<.32 C1)) =.32 bv32"#x00000000") /\ (C1 !=.32 (width.32(C1) -.32 bv32"#x00000001"))))] ; /* 764*/
    udiv(shl_nuw_i9(X, C1), C2) -> udiv(X, CL0)  [ (((C2 /u.32 (bv32"#x00000001" <<.32 C1)) =.32 CL0) /\ ((C2 %u.32 (bv32"#x00000001" <<.32 C1)) =.32 bv32"#x00000000"))] ; /* 764*/
    udiv_exact(shl_nuw_i7(X, C1), C2) -> udiv_exact(X, CL0)  [ (((C2 /u.32 (bv32"#x00000001" <<.32 C1)) =.32 CL0) /\ ((C2 %u.32 (bv32"#x00000001" <<.32 C1)) =.32 bv32"#x00000000"))] ; /* 764*/
    sdiv(shl_nsw_i9(X, C1), C2) -> mul_nsw(X, CL0)  [ ((((bv32"#x00000001" <<.32 C1) /s.32 C2) =.32 CL0) /\ ((((bv32"#x00000001" <<.32 C1) %s.32 C2) =.32 bv32"#x00000000") /\ (C1 !=.32 (width.32(C1) -.32 bv32"#x00000001"))))] ; /* 772*/
    udiv(shl_nuw_i9(X, C1), C2) -> mul_nuw(X, CL0)  [ ((((bv32"#x00000001" <<.32 C1) /u.32 C2) =.32 CL0) /\ (((bv32"#x00000001" <<.32 C1) %u.32 C2) =.32 bv32"#x00000000"))] ; /* 772*/
    udiv(shl_nsw_nuw_i9(X, C1), C2) -> mul_nsw_nuw(X, CL0)  [ ((((bv32"#x00000001" <<.32 C1) /u.32 C2) =.32 CL0) /\ (((bv32"#x00000001" <<.32 C1) %u.32 C2) =.32 bv32"#x00000000"))] ; /* 772*/
    sdiv(bv32"#x00000001", X) -> select(icmp_ult(add(X, bv32"#x00000001"), bv32"#x00000003"), X, bv32"#x00000000"); /* 805*/
    udiv(bv32"#x00000001", X) -> zext(icmp_eq(X, bv32"#x00000001")); /* 809*/
    sdiv(sub(X, srem_i9(X, Op1)), Op1) -> sdiv(X, Op1); /* 820*/
    udiv(sub(X, urem_i9(X, Op1)), Op1) -> udiv(X, Op1); /* 820*/
    udiv_i9(x, C) -> lshr(x, CL0)  [ ((log2.32(C) =.32 CL0) /\ isPowerOf2.32(C))] ; /* 865*/
    udiv_exact_i9(x, C) -> lshr_exact(x, CL0)  [ ((log2.32(C) =.32 CL0) /\ isPowerOf2.32(C))] ; /* 865*/
    udiv(x, C) -> select(icmp_ult(x, C), bv32"#x00000000", bv32"#x00000001")  [ (C >=u.32 (bv32"#x00000001" <<.32 (width.32(C) -.32 bv32"#x00000001")))] ; /* 876*/
    udiv(x, shl_i13(bv32"#x00000001", N)) -> lshr(x, N); /* 891*/
    udiv_exact(x, shl_i13(bv32"#x00000001", N)) -> lshr_exact(x, N); /* 891-exact*/
    udiv(x, shl_i13(C, N)) -> lshr(x, add(N, CL0))  [ ((log2.32(C) =.32 CL0) /\ isPowerOf2.32(C))] ; /* 891-2*/
    udiv_exact(x, shl_i13(C, N)) -> lshr_exact(x, add(N, CL0))  [ ((log2.32(C) =.32 CL0) /\ isPowerOf2.32(C))] ; /* 891-2*/
    udiv_i13(x, zext(shl(C, N))) -> lshr(x, zext(add(N, CL0)))  [ ((log2.32(C) =.32 CL0) /\ isPowerOf2.32(C))] ; /* 891-3*/
    udiv_exact_i13(x, zext(shl(C, N))) -> lshr_exact(x, zext(add(N, CL0)))  [ ((log2.32(C) =.32 CL0) /\ isPowerOf2.32(C))] ; /* 891-3*/
    udiv(lshr_i9(X, C1), C2) -> udiv(X, CL0)  [ (((C2 <<.32 C1) =.32 CL0) /\ WillNotOverflowUnsignedShl.32(C2, C1))] ; /* 968*/
    udiv(zext_Ty(X), zext_Ty(Y)) -> zext(udiv(X, Y)); /* 976*/
    udiv_exact_i9(zext_Ty(X), zext_Ty(Y)) -> zext(udiv_exact(X, Y)); /* 976-exact*/
    sdiv(X, bv32"#xffffffff") -> sub(bv32"#x00000000", X); /* 1030*/
    sdiv_exact_i33(Op0, C) -> ashr_exact(Op0, CL0)  [ ((log2.32(C) =.32 CL0) /\ ((C >=s.32 bv32"#x00000000") /\ isPowerOf2.32(C)))] ; /* 1033*/
    sdiv(Op0, C) -> zext(icmp_eq(Op0, C))  [ isSignBit.32(C)] ; /* 1045*/
    sdiv(sub_nsw_i11(bv32"#x00000000", X), C) -> sdiv(X, neg.32(C)); /* 1049*/
    sdiv(Op0, Op1) -> udiv(Op0, Op1)  [ (MaskedValueIsZero.32(Op0, (bv32"#x00000001" <<.32 (width.32(Op0) -.32 bv32"#x00000001"))) /\ MaskedValueIsZero.32(Op1, (bv32"#x00000001" <<.32 (width.32(Op0) -.32 bv32"#x00000001"))))] ; /* 1062*/
    sdiv(Op0, shl_i23(C, X)) -> udiv(Op0, shl_i23(C, X))  [ (MaskedValueIsZero.32(Op0, (bv32"#x00000001" <<.32 (width.32(Op0) -.32 bv32"#x00000001"))) /\ isPowerOf2.32(C))] ; /* 1065*/
    urem(zext_Ty(X), zext_Ty(Y)) -> zext(urem(X, Y)); /* 1285*/
    urem_i33(Op0, Op1) -> And(Op0, add(Op1, bv32"#xffffffff"))  [ isPowerOf2OrZero.32(Op1)] ; /* 1291*/
    urem(bv32"#x00000001", Op1) -> zext(icmp_ne(Op1, bv32"#x00000001")); /* 1298*/
    srem_i11(Op0, C) -> srem(Op0, neg.32(C))  [ ((C <s.32 bv32"#x00000000") /\ not(isSignBit.32(C)))] ; /* 1321*/
    srem(Op0, Op1) -> urem(Op0, Op1)  [ (MaskedValueIsZero.32(Op1, (bv32"#x00000001" <<.32 (width.32(Op1) -.32 bv32"#x00000001"))) /\ MaskedValueIsZero.32(Op0, (bv32"#x00000001" <<.32 (width.32(Op0) -.32 bv32"#x00000001"))))] ; /* 1333*/
    shl_nuw_i9(X0, X1) -> shl(X0, X1); /**/
    zext_Ty(X0) -> zext(X0); /**/
    shl_nsw_nuw_i9(X0, X1) -> shl(X0, X1); /**/
    urem_i9(X0, X1) -> urem(X0, X1); /**/
    srem_i11(X0, X1) -> srem(X0, X1); /**/
    sdiv_exact_i33(X0, X1) -> sdiv(X0, X1); /**/
    mul_nuw(X0, X1) -> mul(X0, X1); /**/
    mul_nuw_nsw(X0, X1) -> mul(X0, X1); /**/
    shl_i7(X0, X1) -> shl(X0, X1); /**/
    urem_i33(X0, X1) -> urem(X0, X1); /**/
    icmp_eq(X0, X1) -> icmp(X0, X1); /**/
    mul_nuw_nsw_i7(X0, X1) -> mul(X0, X1); /**/
    udiv_exact_i9(X0, X1) -> udiv(X0, X1); /**/
    shl_i33(X0, X1) -> shl(X0, X1); /**/
    shl_nsw_i7(X0, X1) -> shl(X0, X1); /**/
    mul_nsw(X0, X1) -> mul(X0, X1); /**/
    udiv_i9(X0, X1) -> udiv(X0, X1); /**/
    shl_i23(X0, X1) -> shl(X0, X1); /**/
    icmp_ne(X0, X1) -> icmp(X0, X1); /**/
    sdiv_i7(X0, X1) -> sdiv(X0, X1); /**/
    icmp_ult(X0, X1) -> icmp(X0, X1); /**/
    udiv_exact(X0, X1) -> udiv(X0, X1); /**/
    mul_nuw_i7(X0, X1) -> mul(X0, X1); /**/
    udiv_i13(X0, X1) -> udiv(X0, X1); /**/
    shl_nuw(X0, X1) -> shl(X0, X1); /**/
    srem_i9(X0, X1) -> srem(X0, X1); /**/
    udiv_i5(X0, X1) -> udiv(X0, X1); /**/
    sdiv_i5(X0, X1) -> sdiv(X0, X1); /**/
    mul_nuw_i11(X0, X1) -> mul(X0, X1); /**/
    mul_i11(X0, X1) -> mul(X0, X1); /**/
    mul_i1(X0, X1) -> mul(X0, X1); /**/
    lshr_exact(X0, X1) -> lshr(X0, X1); /**/
    sdiv_exact(X0, X1) -> sdiv(X0, X1); /**/
    shl_nuw_i7(X0, X1) -> shl(X0, X1); /**/
    udiv_exact_i13(X0, X1) -> udiv(X0, X1); /**/
    udiv_i7(X0, X1) -> udiv(X0, X1); /**/
    mul_nsw_nuw(X0, X1) -> mul(X0, X1); /**/
    ashr_exact(X0, X1) -> ashr(X0, X1); /**/
    mul_nsw_i7(X0, X1) -> mul(X0, X1); /**/
    shl_i13(X0, X1) -> shl(X0, X1); /**/
    shl_nsw_i9(X0, X1) -> shl(X0, X1); /**/
    sub_nsw_i11(X0, X1) -> sub(X0, X1); /**/
    lshr_i9(X0, X1) -> lshr(X0, X1); /**/

NON-STANDARD IRREGULAR

QUERY loops