Puzzling result from lexicographic optimization

[ngoodman]

Dear amazing Z3 devs / community. I am seeing some behavior I don't understand from a simple optimization when I have two objectives and the first has a symmetry broken by the second objective. Here is a minimal repro:

import z3

v1 = z3.Bool("1exist")
v2 = z3.Bool("2exist")
s2 = z3.Int("2start")

#constraint is v1 xor v2
constraints = [z3.Xor(v1, v2)]
#first objective is optimal if either v1 or v2 is true
obj1 = z3.If(v1, 60, 0) + z3.If(v2, 60, 0)
#second objective is optimal if v2 is true and s2 is 0
obj2 = z3.If(v2, z3.If(s2 == 0, 10, 0), 0)

solver = z3.Optimize()
z3.set_param(verbose=1)
solver.assert_exprs(constraints)
objectives = [obj1, obj2]
objs = [solver.maximize(ob) for ob in objectives]

result=solver.check()
print(f"result: {result}, model: {solver.model()}")
bounds = [(ob.lower(),ob.upper()) for ob in objs]
print(f"bounds {bounds}")

this yields:

output:
result: sat, model: [1exist = True, 2exist = False, 2start = 0]
bounds [(60, 60), (0, 0)]
z3 info (4, 12, 1, 0)

This is not the global optimum of the (lexicographically ordered) objective, which would be model: [1exist = False, 2exist = True, 2start = 0].

Is this the correct behavior due to subtleties I'm missing? A bug? Thanks for your help!

[ngoodman]

Here is a slightly more minimal version (the Int variable wasn't needed):

import z3

v1 = z3.Bool("1exist")
v2 = z3.Bool("2exist")

#constraint is v1 xor v2
constraints = [z3.Xor(v1, v2)]
#first objective is optimal if either v1 or v2 is true
obj1 = z3.If(v1, 60, 0) + z3.If(v2, 60, 0)
#second objective is optimal if v2 is true
obj2 = z3.If(v2, 10, 0)

solver = z3.Optimize()
z3.set_param(verbose=100)
solver.assert_exprs(constraints)
objectives = [obj1, obj2]
objs = [solver.maximize(ob) for ob in objectives]

result=solver.check()
print(f"result: {result}, model: {solver.model()}")
bounds = [(ob.lower(),ob.upper()) for ob in objs]
print(f"bounds {bounds}")
print(f"z3 info {z3.get_version()}")

This yields (including some of the debug text in case it's useful):

[...]
(optimize:check-sat)
(sat.solver)
(sat.stats   :conflicts  :restarts     :learned/bin    :gc          :time)
(sat.stats          :decisions   :clauses/bin :units       :memory       )
(sat.stats      0      0    0     2/2     0/0   0       0    17.12   0.00)
(sat.stats      0      2    0     2/2     0/0   0       0    17.12   0.00)
(optimize:sat)
(smt.collecting-features)
(smt.preprocessing :time 0.00 :before-memory 17.21 :after-memory 17.21)
(opt :lex)
(maxsmt)
(opt.maxlex [60:120])
(sat.solver)
(opt.maxlex [60:60])
is-sat: l_true
Satisfying soft constraints
60: |1exist| |-> true 
60: |2exist| |-> false 
(maxsmt)
(sat.solver)
(opt.maxlex [0:0])
is-sat: l_true
Satisfying soft constraints
10: |2exist| |-> false 
result: sat, model: [1exist = True, 2exist = False]
bounds [(60, 60), (0, 0)]
z3 info (4, 12, 1, 0)

If i simply change the order of the terms in the first objective (i.e. obj1 = z3.If(v2, 60, 0) + z3.If(v1, 60, 0)) I get the expected result instead.