Incorrect result in optimization problem

[merlinsun]

Hi Nikolaj and the Z3 team,

I came across an issue related to an optimization problem when using Z3 85d3041.
The instance involves a non-linear formula, and I am unsure if it is appropriate to report this type of issue at this time. Here is the instance:

$ cat test.smt2 
(declare-const a Int)
(declare-const b Int)
(assert (and (>= b a) (>= a (* b b))))
(maximize (* b b))
(check-sat)
(get-objectives)
$ z3 test.smt2 
sat
(objectives
 ((* b b) 3)
)
$ optimathsat test.smt2 
sat

(objectives
 ((* b b) 1)
)

If reporting non-linear formula issues is still not recommended at this stage, I will avoid submitting similar reports in the future.

Thank you for your time and guidance!

[NikolajBjorner]

non-linear objectives were never tested/supported so far

[merlinsun]

Thank you very much, @NikolajBjorner !
I will definitely keep it in mind.

[merlinsun]

Hi, @NikolajBjorner,
I’ve also encountered a potential issue related to handling linear objectives under the default box optimization mode, where each objective is expected to be treated independently. However, it seems this behavior is not consistently observed in the following example.

Single Objective Case

$ cat single.smt2 
(declare-const a Real)
(declare-const b Real)
(assert (> b (- 1 (- a 0))))
(minimize (- a 0))
(set-option :opt.priority box)
(check-sat)
(get-objectives)
$ z3 single.smt2 
sat
(objectives
 ((- a (to_real 0)) (* (- 1) oo))
)

Multiple Objectives Case

$ cat multiple.smt2
(declare-const a Real)
(declare-const b Real)
(assert (> b (- 1 (- a 0))))
(minimize (- 1 (- a 0)))
(minimize (- a 0))
(set-option :opt.priority box)
(check-sat)
(get-objectives)
$ z3 multiple.smt2
sat
(objectives
 ((- (to_real 1) (- a (to_real 0))) 1)
 ((- a (to_real 0)) 0)
)

In the single-objective case, Z3 produces the expected result. However, with multiple objectives, the results appear inconsistent, which seems to indicate a deviation from the intended independent handling of objectives.

Could you kindly take a look at this issue if it’s convenient for you?