It has to do with the algorithm Z3 uses to do optimization I think (there are different ones).
It works in a "bottom-up" manner, first giving the minimization goal its lowest possible value and then it tries to "work its way up" to something satisfiable.
So in this case there's something like:
goal = c1 + c2 + c3
minimize goal
(even if you write minimize (c1 + c2 + c3), it's still creating that goal variable internally, so to speak)
It now wants to give goal the lowest possible value it can assign it, even if not satisfiable, to start the process. It looks at the bounds of c1, c2 and c3 to determine this, and they're all -infinity.
The lowest possible value of goal is -infinity, which the optimizer has no idea what to do with, and just basically gives up. When used as an application, Z3 will tell you something's wrong by spitting this out in the terminal:
(+ c1 c2 c3) |-> (* (- 1) oo)
A different optimization algorithm, like one that works "top-down" (find the first satisfiable assignment, then make it better) would actually be able to converge. I think OptiMathSAT would be able to handle it because it also does top-down reasoning for this.
CP solvers and MIP solvers all enforce variable bounds so they don't have this issue.
It works in a "bottom-up" manner, first giving the minimization goal its lowest possible value and then it tries to "work its way up" to something satisfiable.
So in this case there's something like:
goal = c1 + c2 + c3 minimize goal
(even if you write minimize (c1 + c2 + c3), it's still creating that goal variable internally, so to speak)
It now wants to give goal the lowest possible value it can assign it, even if not satisfiable, to start the process. It looks at the bounds of c1, c2 and c3 to determine this, and they're all -infinity.
The lowest possible value of goal is -infinity, which the optimizer has no idea what to do with, and just basically gives up. When used as an application, Z3 will tell you something's wrong by spitting this out in the terminal:
(+ c1 c2 c3) |-> (* (- 1) oo)
A different optimization algorithm, like one that works "top-down" (find the first satisfiable assignment, then make it better) would actually be able to converge. I think OptiMathSAT would be able to handle it because it also does top-down reasoning for this.
CP solvers and MIP solvers all enforce variable bounds so they don't have this issue.