void sub_1404E7E00(void) {
    // 0x1404e7e00
    int64_t v1; // 0x1404e7e00
    char * v2 = (char *)v1; // 0x1404e7e1e
    *v2 = 0;
    int32_t v3 = v1;
    if (v3 >= 9) {
        // 0x1404e7ef1
        *v2 = 1;
        int64_t v4; // 0x1404e7e00
        __security_check_cookie(__security_cookie, v4);
        return;
    }
    int64_t v5 = v1 & 0xffffffff; // 0x1404e7e15
    int64_t v6 = 8 * v5; // 0x1404e7e2f
    if ((int32_t)v6 < 64) {
        uint64_t v7 = v6 & 56; // 0x1404e7e43
        int64_t v8 = 1; // 0x1404e7e43
        if (v7 != 0) {
            klee_overshift_check(64, v7);
            klee_overshift_check(64, v7 - 1);
            v8 = 1 << v7;
        }
        if (v1 >= v8) {
            uint64_t v9 = (v6 + 63) % 64; // 0x1404e7e54
            klee_overshift_check(64, v9);
            int64_t v10 = v9 - 1; // 0x1404e7e54
            klee_overshift_check(64, v10);
            if (-1 << v9 > v1) {
                // 0x1404e7ef1
                *v2 = 1;
                __security_check_cookie(__security_cookie, 1);
                return;
            }
            // 0x1404e7e60
            klee_overshift_check(64, v9);
            int64_t v11 = 1 << v9; // 0x1404e7e60
            klee_overshift_check(64, v10);
            if (v1 >= v11) {
                // 0x1404e7ef1
                *v2 = 1;
                __security_check_cookie(__security_cookie, v11);
                return;
            }
        }
    }
    // 0x1404e7e73
    int64_t v12; // bp-72, 0x1404e7e00
    int64_t v13 = (int64_t)&v12 + 48;
    int64_t v14 = 0; // 0x1404e7e7e
    int64_t v15 = 0; // 0x1404e7e7e
    int64_t v16 = 0; // 0x1404e7e7e
    if (*(char *)(*(int64_t *)(*(int64_t *)(v1 + 16) + 8) + 16) == 0) {
        uint64_t v17 = 8 * (v5 - v16) + 56 & 56; // 0x1404e7eaf
        int64_t v18; // 0x1404e7e00
        if (v17 != 0) {
            klee_overshift_check(64, v17);
            klee_overshift_check(64, v17 - 1);
            v18 = v1 >> v17;
        }
        *(char *)(v16 + v13) = (char)v18;
        int64_t v19 = v16 + 1; // 0x1404e7eb7
        v16 = v19 & 0xffffffff;
        while ((int32_t)v19 != v3) {
            // 0x1404e7ea0
            v17 = 8 * (v5 - v16) + 56 & 56;
            if (v17 != 0) {
                klee_overshift_check(64, v17);
                klee_overshift_check(64, v17 - 1);
                v18 = v1 >> v17;
            }
            *(char *)(v16 + v13) = (char)v18;
            v19 = v16 + 1;
            v16 = v19 & 0xffffffff;
        }
    } else {
        uint64_t v20 = v15 % 64; // 0x1404e7e89
        int64_t v21; // 0x1404e7e00
        if (v20 != 0) {
            klee_overshift_check(64, v20);
            klee_overshift_check(64, v20 - 1);
            v21 = v1 >> v20;
        }
        *(char *)(v14 + v13) = (char)v21;
        int64_t v22 = v14 + 1; // 0x1404e7e94
        v14 = v22 & 0xffffffff;
        v15 = v15 + 8 & 0xffffffff;
        while ((int32_t)v22 != v3) {
            // 0x1404e7e83
            v20 = v15 % 64;
            if (v20 != 0) {
                klee_overshift_check(64, v20);
                klee_overshift_check(64, v20 - 1);
                v21 = v1 >> v20;
            }
            *(char *)(v14 + v13) = (char)v21;
            v22 = v14 + 1;
            v14 = v22 & 0xffffffff;
            v15 = v15 + 8 & 0xffffffff;
        }
    }
    // 0x1404e7ebe
    int64_t v23; // bp-24, 0x1404e7e00
    int64_t v24 = &v23; // bp-40, 0x1404e7ec8
    __security_check_cookie(__security_cookie, (int64_t)&v24);
}