Nonlinear constraint propagation with z3?

I am a Z3 newbie, and am trying to determine the marginal limits of a feasible region defined by a system of (in)equalities. My first (perhaps inefficient) approach is to define an Optimizer, assign limits, then minimize and maximize each variable in turn. This works great as long as the inequalities are linear. See the snippet below:

from z3 import *

# Create Z3 variables
a, b, = Reals('a b')

# Define the constraints
constraints = [
    a >= 0,
    a <= 5,
    b >= 0,
    b <= 5,
    a + b == 4]

# Creat3 a Z3 solver
solver = Optimize()
for constraint in constraints:
    solver.add(constraint)

for variable in [a,b]:

    # Minimum value    
    solver = Optimize()
    for constraint in constraints:
        solver.add(constraint)
    solver.minimize(variable)
    solver.check()
    model = solver.model()
    print("Lower limit for variable "+str(variable)+": "+str(model[variable]))

    # Maximum value   
    solver = Optimize()
    for constraint in constraints:
        solver.add(constraint)
    solver.maximize(variable)
    solver.check()
    model = solver.model()
    print("Lower limit for variable "+str(variable)+": "+str(model[variable]))

Now if I exchange the last equality a + b == 4 for a nonlinear equality a * b == 4, the solver suddenly freezes, even though the solution should be quite simple, with limits [0.8,5] for both a and b.

Any idea why this is happening? Do you know of a better way to solve such nonlinear constraint problems with z3?

Solution

z3's optimizer does not support non-linear constraints. See z3Opt optimize non-linear function using qfnra-nlsat for a related answer, and also the original paper https://www.microsoft.com/en-us/research/wp-content/uploads/2016/02/nbjorner-nuz.pdf which says:

νZ provides a portfolio of approaches for solving linear optimization problems over SMT formulas, MaxSMT, and their combinations.

Note that if your non-linear terms are over bit-vectors, then those will be supported (since they get bit-blasted anyhow.) But non-linear constraints over integers and reals are beyond the capabilities of z3. (This doesn't necessarily mean that z3 won't solve such problems: If there's enough other constraints, then heuristics might kick in to give an answer. The point is that, if you have non-linear constraints over reals or integers, then the solver isn't guaranteed to terminate.)