Following this issue #2216, look at the following example:

x, y, z = Reals('x y z')

s = Optimize()
s.set("opt.priority", "lex")
s.add(x > y)
s.add(y > z)
s.add(z > 0)
s.add_soft(x > y + 1)
h = s.minimize(x)
print(s.check())
print(s.model())
print(h.value())

s = Optimize()
s.set("opt.priority", "lex")
s.add(x > y)
s.add(y > z)
s.add(z > 0)
h = s.minimize(x)
s.add_soft(x > y + 1)
print(s.check())
print(s.model())
print(h.value())

The result is

sat
[z = 2/3, y = 4/3, x = 3]
1 + 3*epsilon

sat
[y = 2, z = 1, x = 3]
3*epsilon

I'm on Z3 v4.13.0.0

I find it very strange because it appears that the soft-assert and the minimize are reasoning on two different models.
In the first case the output model [z = 2/3, y = 4/3, x = 3] respects the soft assert while the model [z = epsilon, y= 2epsilon, x= 1+3epsilon] respects bot the soft asserts and is minimal w.r.t. x

In the second model [y = 2, z = 1, x = 3] is not the minimal and doesn't respect the soft-assert while [y = 2epsilon, z = epsilon, x=3epsilon] is the minimal one which doesn't respect the soft assert.

What is going on?