Correctness issue regarding `abs` in multi-objective optimization

[merlinsun]

Hi Nikolaj,

I’ve encountered an issue with Z3 c002c77.
For the following instance, when maximizing (abs (to_int a)) alongside another objective, Z3 returns an incorrect optimal value of 1 instead of the expected oo.

Minimal Example:

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

Output:

sat
(objectives
 (a (- 1))
 ((abs (to_int a)) 1)
)

Expected Behavior:

The issue only occurs when (maximize (abs (to_int a))) is combined with another objective like (maximize a). When (maximize a) is removed, Z3 correctly reports (abs (to_int a)) as oo.

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

Output (Correct):

sat
(objectives
 ((abs (to_int a)) oo)
)

Thanks for looking into this!