#!/usr/bin/env python3

from z3 import *

s=Solver()

x=Int("x")
s.add(x>0)

dayno=Int("dayno")
s.add(dayno==x/86400)
s.add((dayno+4)%7==5) # must be Friday

s.check()
print (s.model())