z3Opt optimize non-linear function using qfnra-nls

问题:

I'm trying to use z3Opt for optimizing a real non-linear function, but even for simple cases like the following one

http://rise4fun.com/Z3Opt/JbaU

the result is not what it is expected to be. It's like z3 it is not optimizing at all.... anyone can help me understand?

回答1:

Optimization of non-linear functions is not supported at this point, so no guarantee is given on results. It would probably be better if the solver returns unknown (and not sat) for this case, which is something I should look into.