Incorrect real optimization results

[LeventErkok]

Looks like this is a recent regression, where optimizer no longer returns correct values for real variables:

(set-logic ALL)

(declare-fun x () Real)
(assert (> x 0.0))
(minimize x)

(check-sat)
(get-objectives)

Latest z3 says:

sat
(objectives
 (x 1)
)

Version of z3 from Apr 30 (about a month ago) produces the correct result:

sat
(objectives
 (x (* 2.0 epsilon))
)

(which can further be reduced to simply epsilon I suppose, though one can argue this is correct as well.)

[NikolajBjorner]

For strict bounds I can't guarantee generating epsilons. Generally, optimization has to support hybrid environments where theories are mixed so having also the infinitesimal information in the output hits against the integration requirement.

[LeventErkok]

@NikolajBjorner

Thanks Nikolaj.

Wouldn't it be more appropriate, then, to return unknown or unsupported as an answer in these cases, since the objective value now generated is clearly incorrect? This way the upstream tools can at least have a chance of trying to recover from a no-answer, instead of proceeding with an incorrect result.