#!/usr/bin/env python3

from z3 import *

s=Solver()

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

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

# 2nd constraint:
hour=Int("hour")
s.add(hour==(x%86400)/3600) # get hour (UTC time)
s.add(hour>=18)
s.add(hour<=23)

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