I’ve made a small PR for Z3’s OCaml API to release the runtime lock when calling some costly functions (check and simplify). Are there downsides or risks associated to that? I’ve never used these particular calls before…
Make sure you haven’t installed any callbacks that lead to Z3 calling back into OCaml code. The error handler is one way to do this. I’m not sure of the current API, but the plugin interface used to allow registering OCaml callbacks that would get called from reasonably deep within Z3.
That’s a good point, thank you. I don’t see any higher-order function in z3.mli and, as far as I know, they removed the plugin API a while ago.