About Z3_MUTEX

[black-binary]

I'm currently developing a multi-threaded program, but it seems like almost every function call to the z3 library is mutex-guarded. My threads will frequently create expressions and eval() them, and each thread has its own Context (unsafe impl Send for Context)

I'm wondering if the Z3_MUTEX will slow down my code. If so, is it safe to remove the Z3_MUTEX in my code? Thanks :)

[waywardmonkeys]

The last time that I looked at this, a couple of years ago now, I guess, it was necessary because of bugs in Z3, perhaps on macOS. I think those bugs were fixed, but I don't know if there are new ones or not.

You might be able to investigate whether or not it can be removed. :)

[black-binary]

@waywardmonkeys Thanks for your reply. I plan to run a stress test parallelly after removing the mutex, and see if it will crash.

[waywardmonkeys]

This has been removed now in #211 (follow on to #143).