Multiple instance and thread safety?

[de...@eng.ucsd.edu]

Hi,

We'd like to use boolector in a new tool, possibly by extending the Haskell bindings. I'd like to understand if boolector is a good fit for our existing model or if we need to tweak it to work better with your library.

Is it safe to create multiple boolector instances to solve multiple equations, simultaneously? Importantly, is it safe to do this in different (separate) threads ? From the API design it seems like the answer is yes to both, but I couldn't find documentation to confirm this.

Thanks!

-deian

[Armin Biere]

It should be thread safe, except that printing verbose information etc. is not locked and most

likely will produce garbage if you run multiple instances producing verbose output in different

threads printing to the same output stream, but this should not influence correctness.

Armin

[de...@eng.ucsd.edu]

Fantastic, thanks! (I' not concerned about printing, makes sense that that would not be locked.)