Optimizers not producing optimal solutions when using `assert_and_track`

[poscat0x04]

from z3 import *

p0 = Int(0)
p1 = Int(1)
p2 = Int(2)

s = Optimize()
s2 = Optimize()

assertions = [p0 >= 0,
              p0 <= 3,
              p1 >= 0,
              p1 <= 1,
              p2 >= 0,
              p2 <= 2,
              Implies(p1 == 1, And(p0 >= 1, p0 <= 2)),
              Implies(p2 == 1, And(p0 >= 2, p0 <= 3)),
              Implies(p2 == 2, And(p0 >= 2, p0 <= 3)),
              p2 != 0,
              p1 == 1
              ]

for a, i in zip(assertions, range(len(assertions))):
    s.add(a)
    s2.assert_and_track(a, Bool(i))

e = If(p0 == 0, 0, 3 - p0) + If(p1 == 0, 0, 1 - p1) + If(p2 == 0, 0, 2 - p2)

s.minimize(e)
s2.minimize(e)

s.check()
s2.check()

print(s.model())
print(s2.model())

output:

[k!0 = 2, k!2 = 2, k!1 = 1]
[k!0 = True,
 k!4 = True,
 k!2 = 1,
 k!8 = True,
 k!1 = True,
 k!5 = True,
 k!9 = True,
 k!2 = True,
 k!0 = 2,
 k!6 = True,
 k!10 = True,
 k!3 = True,
 k!1 = 1,
 k!7 = True]

The models differ on the interpretation of k!2 which shouldn't happen.

I'm using z3 version 4.12.2 packaged by fedora.