Optimize Result - Expected or Not?

[AndrewJSchoen]

Hi all,

I am working on a problem, and was receiving some unexpected results with a model that I was trying to generate in z3py. I had gotten things working with the standard Solver, but when I moved over to the Optimize variant it doesn't produce the obvious result. I distilled the problem down to a much simpler one, shown below:

ctx = z3.Context()
solver = z3.Optimize(ctx)

length = 5

timeline = [z3.Int('t{0}'.format(i),ctx) for i in range(length)]
for i in range(length-1):
    solver.add(timeline[i+1] > timeline[i])
solver.add(timeline[0] >= 0)

print(solver.check())
solver.minimize(timeline[length-1])
print(solver.reason_unknown())
print(solver.model())

sat
unknown
[]

On the other hand, the Solver approach produces the expected [t0 = 0, t4 = 4, t3 = 3, t2 = 2, t1 = 1]. I also know there are some limitations with nonlinear problems with z3 optimization, but wasn't aware this problem qualified for that type of limitation. Am I mistaken, or just doing something incorrect?

[AndrewJSchoen]

Ah, nevermind - looks like I needed to run check before the minimize function. Swapping the two produces the expected output.