Can I use Z3py in multi-threading?

[JohnLyu2]

Hi, I am writing python code using multi-threading to check the satisfiability of formulas in a benchmark. In each thread, I check the satisfiability of one formula using Z3py ( s = Solver(); s.add(formula); s.check() ). However, the code always run into segmentation fault. Then I found that even if I only do z3.parse_smt2_file(formula_file) in each thread, segmentation faults still happen. Probably the issues come from "Z3Py uses a default global context". May I ask can Z3py (python APIs) be used in python multi-threading? Are there ways to fix the problems I mentioned? Thanks!

[NikolajBjorner]

You need to use separate contexts (Context object) for each thread.
The Python API allows you to create contexts and pass them to Solver and other functions.
The default, global, context is not going to be thread safe.

[JohnLyu2]

It works, thanks!