Conflicting optimization results

[paulKobi]

Dear Z3 team, In recent experiments, we ran into some problems with the Python API when optimizing over boolean constraints. We generate a large number of constrained assignment problem over bools and then minimize a sum over a subset of these bools. Roughly speaking the process looks like this.

def minimize(input):
    context = z3.Context()
    s = Optimize(ctx=context)
    # construct a model from input
    ...
    h = s.minimize(...)
    return h.lower().as_long()

After many iterations, we sometimes compute different results for the same problem.

result = minimize(input)
result1 = minimize(input)
assert result == result1 # this fails!

The behavior is history-dependent in that minimize(input) in isolation behaves as expected for the "problem" input, but the assertion fails after many previous computations. We have managed to generate a log that reproduces the problem (using simply open_log("foo.log") at the very beginning), but it is quite large (~11GiB). Trying to log and replay just the problematic input results in a segmentation fault. One solution to the problem is simply writing and reading the input from a file:

f.write(s.sexpr())
del s
s = Optimize(ctx=context)
s.from_file()
h = s.minimize(s.objectives()[0])

Two questions:

1. Is this known/expected behavior for the optimization mode?
2. If not, is there a way to isolate the problem further to produce a smaller log?

Any input owuld be greatly appreciated. Please excuse this rather informal description and thank you very much for any help.