1from z3 import *
2from multiprocessing.pool import ThreadPool
3from copy import deepcopy
4
5pool = ThreadPool(8)
6x = Int('x')
7
8assert x.ctx == main_ctx()
9
10
11def calculate(x, n, ctx):
12    """ Do a simple computation with a context"""
13    assert x.ctx == ctx
14    assert x.ctx != main_ctx()
15
16    # Parallel creation of z3 object
17    condition = And(x < 2, x > n, ctx)
18
19    # Parallel solving
20    solver = Solver(ctx=ctx)
21    solver.add(condition)
22    solver.check()
23
24
25for i in range(100):
26    # Create new context for the computation
27    # Note that we need to do this sequentially, as parallel access to the current context or its objects
28    # will result in a segfault
29    i_context = Context()
30    x_i = deepcopy(x).translate(i_context)
31
32    # Kick off parallel computation
33    pool.apply_async(calculate, [x_i, i, i_context])
34
35pool.close()
36pool.join()
37