Python Z3 and concurrent.futures

I want to solve a set of contained problems in parallel, after which addition information is added to solve a new problem.

Below is an example of the structure of the program used to solve the problem:

from z3 import *
import concurrent.futures


# solver test function
def add(a, b, solver, index):
    solver.append(a > b)
    assert solver.check()
    model = solver.model()
    return {
        'solver': solver,
        'av': model[a],
        'a': a,
        'b': b,
        'bv': model[b],
        'index': index
    }


with concurrent.futures.ThreadPoolExecutor(max_workers=5) as executor:
    # start solving the problems
    to_compute = []
    for i in range(3):
        sol = z3.Solver()
        to_compute.append(executor.submit(
            add,
            Int('a{}'.format(i)),
            Int('b{}'.format(i)),
            sol,
            i
        ))
    # wait for the solution to the computations
    next_to_solve = []
    for result_futures in concurrent.futures.as_completed(to_compute):
        results = result_futures.result()
        print(results)
        sol = results['solver']
        sol.append(results['a'] > results['av'])
        next_to_solve.append(
            executor.submit(
                add,
                results['a'],
                results['b'],
                sol,
                results['index']
            )
        )

The results is different each time the program is run, the results includes:

Z3Exception 'invalid dec_ref command'
python that crash
No error

What do I need to do, to make the program more reliable?

Solution

Did you see this example: http://github.com/Z3Prover/z3/blob/master/examples/python/parallel.py

I'm not an expert on the concurrent features in z3py, but it seems to be you need to be very careful about creating the variables in the same context that you're running the solvers in. There are some hints in that very file.