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

int is_it_friday(uint32_t input)
{
        uint32_t SECS_DAY=24*60*60;
        uint32_t dayno = input / SECS_DAY;
        uint32_t wday = (dayno + 4) % 7;
        if (wday==5)
                return 1; // friday
        else
                return 0;
};

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