Soundness of non-linear optimization

[Bogato]

I used Z3 to optimize some problems, including ones over non-linear integer constraints. Z3's documentation and the vZ paper state that optimization only work for LIA/LRA. Still, it seems to return a correct models on those instances. Moreover, various Stack Overflow answers[1][2] said that z3 may provide a model on some non-linear cases.

I would like to know if models returned by Z3 are correct (or at least a sound over-approximation) of optimum, even for non-linear constraints.

P.S.: Citing a recent issue (#1445):

For the second (non-linear) example, I get the "correct" result locally, but generally Z3 is not tested (and checked) for non-linear objectives or optimization in the context of non-linear constraints.

[NikolajBjorner]

As the comment says, Z3 isn't tested on non-linear objectives. There are many standard ways to deal with non-linear objectives (over linear constraints), but they are not implemented in Z3. Furthermore, I don't have a regression test set for non-linear objectives so I am highly reluctant to recommend this.
Under the hood, a non-linear objective is converted into a new variable and an equality constraint. Then, it uses the standard engine for arithmetic satisfiability to find solutions to this objective variable. The non-linear arithmetic solver has its own limitations, but if it is lucky it can find solutions or prove absense of solutions to non-linear constraints. Some (SMT) application scenarios with non-linear objectives may be useful to identify where it makes sense to make inroads in this area.