#include <stdint.h>
#include <assert.h>

int lets_party(uint32_t input)
{
        uint32_t SECS_HOUR=60*60;
        uint32_t SECS_DAY=24*SECS_HOUR;
        uint32_t dayno = input / SECS_DAY;
        uint32_t wday = (dayno + 4) % 7;
        if (wday==5)
        {
                // friday

                uint32_t hour=(input % SECS_DAY) / SECS_HOUR;

                if (hour>=18 && hour<=23)
                        return 1;
                else
                        return 0;
        }
        else
                return 0;
};

int main()
{
    uint32_t input;
    klee_make_symbolic(&input, sizeof input, "input");
    if (lets_party(input))
            klee_assert (0);
};