Satisfiability of a formula having forall quantifier
<p>This is my Python code:</p>

<pre><code>s = z3.Solver()

f = z3.Function('f', z3.IntSort(), z3.IntSort())
g = z3.Function('g', z3.IntSort(), z3.IntSort())
h = z3.Function('h', z3.IntSort(), z3.IntSort())

a, b, c = z3.Ints('a b c')

imp_a = z3.And(f(a) == b, g(a) == c)
imp_b = h(c) == b
ax = z3.ForAll(a, z3.Implies(imp_a, imp_b))

l = [
    ax,
    f(1) == 5,
    g(1) == 2,
    h(2) != 5
]
s.add(l)

if s.check() == z3.sat:
    print s.model()
else:
    print 'Unsat'
</code></pre>

<p>In this code, I have written the following formula in Z3Py syntax:</p>

<pre><code>forall a, (f(a) == b and g(a) == c) =&gt; h(c) == b
</code></pre>

<p>When I run this script it finds a model, while I think it should be <code>unsat</code>. How could it be possible? Am I missing something? </p>