Is it a bug in Z3? Incorrect answer on Real and ForAll applied

Question

I'm trying to find the minimal value of the Parabola y=(x+2)**2-3, apparently, the answer should be y==-3, when x ==-2. But z3 gives the answer [x = 0, y = 1], which doesn't meet the ForAll assertion.

Am I assuming wrongly with something?

Here is the python code:

from z3 import *

x, y, z = Reals('x y z')

print(Tactic('qe').apply(And(y == (x + 2) ** 2 - 3,
                             ForAll([z], y <= (z + 2) ** 2 - 3))))

solve(y == x * x + 4 * x +1,
      ForAll([z], y <= z * z + 4 * z +1))

And the result:

[[y == (x + 2)**2 - 3, True]]
[x = 0, y = 1]

The result shows that 'qe' tactic eliminated that ForAll assertion into True, although it's NOT always true. Is that the reason that solver gives a wrong answer? What should I code to find the minimal (or maximal) value of such an expression?

BTW, the Z3 version is 4.3.2 for Mac.

Answer 1

I refered How does Z3 handle non-linear integer arithmetic? and found a partial solution, using 'qfnra-nlsat' and 'smt' tactics.

from z3 import *

x, y, z = Reals('x y z')

s1 = Then('qfnra-nlsat','smt').solver()
print s1.check(And(y == (x + 2) ** 2 - 3,
                             ForAll([z], y <= (z + 2) ** 2 - 3)))
print s1.model()

s2 = Then('qe', 'qfnra-nlsat','smt').solver()
print s2.check(And(y == (x + 2) ** 2 - 3,
                             ForAll([z], y <= (z + 2) ** 2 - 3)))
print s2.model()

And the result:

sat
[x = -2, y = -3]
sat
[x = 0, y = 1]

Still the 'qe' tactic and the default solver seem buggy. They don't give the correct result. Further comments and discussions are needed.