Correctness issue on multi-objective optimization

[merlinsun]

Hi Nikolaj,

I’ve noticed an issue with Z3’s handling of multi-objective optimization.
When maximizing an unconstrained variable b, Z3 cd95c7e returns an incorrect optimal value of (* (- 1) oo) instead of the expected oo.

Minimal Example:

(set-option :opt.priority box)
(declare-const a Real)
(declare-const b Real)
(assert (> 0 a))
(maximize a)
(maximize b)
(minimize (- a))
(check-sat)
(get-objectives)

Output:

sat
(objectives
 (a (- 1))
 (b (* (- 1) oo))
 ((- a) 1)
)

Additional Note: Removing (minimize (- a)) yields the correct result:

(set-option :opt.priority box)
(declare-const a Real)
(declare-const b Real)
(assert (> 0 a))
(maximize a)
(maximize b)
(check-sat)
(get-objectives)

Output:

sat
(objectives
 (a (- 1))
 (b oo)
)

Thanks for looking into this!