z3 optimize and soft constraints

Question

The following code sets a to True when only_2 is True, but sets a to False otherwise. I don't understand, because if we are minimizing the soft constraints, we should always pick a that has highest probability. What am I missing? How can I minimize across all soft constraints?

from z3 import *
from math import exp

only_2 = True

pa1 = 0.8
pa2 = 0.8
pa3 = 0.2
pb1 = 0.7
pb2 = 0.8
pb3 = 0.2

a = Bool('a')
b = Bool('b')
a1 = Bool('a1')
a2 = Bool('a2')
a3 = Bool('a3')
b1 = Bool('b1')
b2 = Bool('b2')
b3 = Bool('b3')

all_xps = [(a1,pa1), (b1,pb1), (a2,pa2), (b2,pb2), (a3,pa3), (b3,pb3)]
all_as = [a1, a2, a3]
all_bs = [b1, b2, b3]

if only_2:
    all_xps = all_xps[0:-2]
    all_as = all_as[0:-1]
    all_bs = all_bs[0:-1]

s = Optimize()
for (x,p) in all_xps:
    s.add_soft(Not(x), exp(-p))
    s.add_soft(x, exp(-(1-p)))
s.add(Implies(And(*all_as), a))
s.add(Implies(Not(And(*all_as)), Not(a)))
s.add(Implies(And(*all_bs), b))
s.add(Implies(Not(And(*all_bs)), Not(b)))
s.add(Xor(a, b))

assert s.check() == sat
model = s.model()
print(model[a])

Answer 1

I figured it out: the a3/b3 constraints are smaller, so it can fail either one of those, instead of falling the bigger inequal constraints.