one loop for pareto priority and objectives are 'False', what does this mean? (Z3)

Question

I've tried to replicate the below code for my own optimization problem.

However, I only get one loop.

When printing the objectives below without calling the method value(), each objective is True. For mine they are False.

How do I interpret these results?

Many thanks.

x, y = Ints('x y')
opt = Optimize()
opt.set(priority='pareto')
opt.add(x + y == 10, x >= 0, y >= 0)
mx = opt.maximize(x)
my = opt.maximize(y)
while opt.check() == sat:
    print (mx.value(), my.value())

Answer 1

It’s hard to decipher what you mean. By “I only get one loop” I assume you mean you get the values printed only once and that’s it. That’s perfectly fine, it simply means the Pareto front only has one element.

To get a better analysis, you’ll have to post the actual code (as simplified as you can). Without seeing exactly what you’re doing it’s impossible to opine further.