from z3 import *

state = 42

def dish(d):
	state = ((state + d) * 3294782) ^ 3159238819

s = Solver()
s.add(state==0xde11c105)
s.add(dish())

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