Non-deterministic correctness bug in QF_LIA optimization

[mikand]

Z3 (4.13.0) sometimes (non-deterministically) produces invalid optimal models for a simple QFLIA optimization problem.

I tried to create a minimal problem that reproduces the issue. On my linux machine, the following script highlights the error in at most a couple of seconds.

from z3 import *

print("Z3 Version: %s" % str(z3.get_version()))

x1 = Int("x1")
x2 = Int("x2")
x3 = Int("x3")
x4 = Int("x4")
x5 = Int("x5")
x6 = Int("x6")
x7 = Int("x7")
x8 = Int("x8")

all_vars = [x1, x2, x3, x4, x5, x6, x7, x8]

assertions = [0 <= x1, 0 <= x2, 0 <= x3, 0 <= x4, 0 <= x5, 0 <= x6, 0 <= x7, 0 <= x8,
              Or(x1 + 1240 < x2, x2 + 629 < x1),
              Or(x1 + 1240 < x3, x3 + 1240 < x1),
              Or(x1 + 1240 < x4, x4 + 1240 < x1),
              Or(x1 + 835 < x5, x5 + 835 < x1),
              Or(x1 + 705 < x6, x6 + 1240 < x1),
              Or(x1 + 705 < x7, x7 + 835 < x1),
              Or(x1 + 835 < x8, x8 + 629 < x1),
              Or(x2 + 629 < x3, x3 + 1240 < x2),
              Or(x2 + 629 < x4, x4 + 581 < x2),
              Or(x2 + 1240 < x5, x5 + 804 < x2),
              Or(x2 + 1240 < x8, x8 + 1240 < x2),
              Or(x3 + 1240 < x4, x4 + 1240 < x3),
              Or(x3 + 835 < x5, x5 + 835 < x3),
              Or(x3 + 705 < x6, x6 + 1240 < x3),
              Or(x3 + 705 < x7, x7 + 835 < x3),
              Or(x3 + 835 < x8, x8 + 629 < x3),
              Or(x4 + 629 < x5, x5 + 835 < x4),
              Or(x4 + 1240 < x6, x6 + 1240 < x4),
              Or(x4 + 1240 < x7, x7 + 835 < x4),
              Or(x4 + 629 < x8, x8 + 629 < x4),
              Or(x5 + 1240 < x6, x6 + 629 < x5),
              Or(x5 + 1240 < x7, x7 + 1240 < x5),
              Or(x5 + 1240 < x8, x8 + 1240 < x5),
              Or(x6 + 1240 < x7, x7 + 1240 < x6),
              Or(x6 + 629 < x8, x8 + 486 < x6),
              Or(x7 + 1240 < x8, x8 + 486 < x7)]

OPTIMUM = 4268

for i in range(1000):
    s = Optimize()
    for f in assertions:
        s.add(f)

    maximum = Int("maximum")
    for v in all_vars:
        s.add(v <= maximum)
    h = s.minimize(maximum)

    res = s.check()
    max_val = s.model()[maximum]
    if str(max_val) == str(OPTIMUM):
        print("%d - OK, optimal value is %s" % (i, OPTIMUM))
    else:
        print("%d - ERROR, optimal value is %s but Z3 returned %s" % (i, OPTIMUM, max_val))
        print("")
        print("The returned model is:")
        print(s.model())
        break

The output on my machine is:

Z3 Version: (4, 13, 0, 0)
0 - OK, optimal value is 4268
1 - OK, optimal value is 4268
2 - OK, optimal value is 4268
[...]
35 - OK, optimal value is 4268
36 - ERROR, optimal value is 4268 but Z3 returned 4459

The returned model is:
[x6 = 3008,
 x8 = 3638,
 x2 = 206,
 maximum = 4459,
 x5 = 1466,
 x1 = 4268,
 x7 = 0,
 x3 = 2302,
 x4 = 836]