from z3 import *

s = Solver()

Type = BitVecSort(16)

x, y, z = Consts("x y z", Type)

def foo(x, y):
  return x & y

s.add(ForAll(z, y != foo(x, z)))

foo = s.check()
print (foo)
if str(foo) == "sat":
  print(s.model())