Python使用threading调用z3-solver报Context mismatch的解决方法

问题背景 #

求解SAT问题时，流程为先构建约束列表，由于各约束相互独立，计划对约束构建步骤做并行化处理。并行运行代码时触发z3.z3types.Z3Exception: Context mismatch报错，报错触发后Python会直接崩溃停止运行，若在Jupyter环境下运行，需要重启kernel才能继续操作。

复现前置准备 #

执行以下命令安装z3依赖包：
pip install z3-solver

最小复现代码 #

from z3 import *
from threading import Thread

def test():
    And(Bool('x'), Bool('y'))

for i in range(20):
    Thread(target=test).start()

完整报错栈 #

Exception in thread Exception in thread Exception in thread Thread-8:
Traceback (most recent call last):
  File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 973, in _bootstrap_inner
Thread-25:
Traceback (most recent call last):
  File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 973, in _bootstrap_inner
Thread-18:
Traceback (most recent call last):
  File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 973, in _bootstrap_inner
    Exception in thread     self.run()
  File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 910, in run
self.run()        self._target(*self._args, **self._kwargs)Thread-20self.run()
  File "/var/folders/0b/4x6686_n1n19cgncddmh0zym0000gn/T/ipykernel_40113/248907556.py", line 5, in test
:
Traceback (most recent call last):
  File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 973, in _bootstrap_inner

  File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 910, in run

  File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 910, in run
Exception in thread Thread-23        :
self._target(*self._args, **self._kwargs)
  File "/var/folders/0b/4x6686_n1n19cgncddmh0zym0000gn/T/ipykernel_40113/248907556.py", line 5, in test
self._target(*self._args, **self._kwargs)
  File "/var/folders/0b/4x6686_n1n19cgncddmh0zym0000gn/T/ipykernel_40113/248907556.py", line 5, in test
Traceback (most recent call last):
  File "/Users/mz/opt/anaconda3/lib/python3.9/threading.py", line 973, in _bootstrap_inner
  File "/Users/mz/opt/anaconda3/lib/python3.9/site-packages/z3/z3.py", line 1856, in And
  File "/Users/mz/opt/anaconda3/lib/python3.9/site-packages/z3/z3.py", line 1856, in And
      File "/Users/mz/opt/anaconda3/lib/python3.9/site-packages/z3/z3.py", line 1856, in And
    self.run()ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))    
  File "/Users/mz/opt/anaconda3/lib/python3.9/site-packages/z3/z3.py", line 499, in _ctx_from_ast_arg_list
ctx = _get_ctx(_ctx_from_ast_arg_list(args, ctx))
  File "/Users/mz/opt/anaconda3/lib/python3.9/site-packages/z3/z3.py", line 499, in _ctx_from_ast_arg_list
    
_z3_assert(ctx == a.ctx, "Context mismatch")
  File "/Users/mz/opt/anaconda3/lib/python3.9/site-packages/z3/z3.py", line 107, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: Context mismatch

运行环境配置 #

• Python版本：3.9.7 (default, Sep 16 2021, 08:50:36) [Clang 10.0.0 ]
• 操作系统：MacOS Monterey 版本12.2.1
• z3-solver版本：4.8.17.0

内容的提问来源于stack exchange，提问作者MohammadReza Hosseini