Hello, I'm glad to see my question has already been asked and answered. I was wondering if there has been any consideration given to making this specific fork of BuDDy thread-safe, or it’s just because there would be too much work. Are there any plans to make this parallel in the future? If it's a matter of simply wrapping static variables into a "Context" argument, I might be able to assist (I assume breaking the C API of BuDDy would be acceptable, as it's not intended for direct user access). ----- To provide some context, for my master's thesis, I'm using Spot for ω-automata operations, specifically performing product and product-or operations on a large number of automata. While other parts of my program are multithreaded, I've found that the only way to parallelize the product and product-or operations is by starting multiple autfilt processes. I did attempt to achieve parallelism by importing Spot via FFI and do stuff in threads. However, after reviewing some of the code of Spot, I noticed the extensive use of static variables. Fangsong Long