[NodeJS] Z3 doesn't seem to clean up threads/workers after finishing its job

[the-docta]

I prepared a neat small example to reproduce the issue: https://bitbucket.org/u-niq/z3-incident/src/master/

basically, there seem to be some workers still being kept after running solver.check()

These need to be cleaned up either automatically, or the developer needs to be able to clean them up, once finished using Z3

Maybe there is even such a method already available in the low-level API, which I just couldnt find?

Thanks and best regads, Sergei

[hildjj]

See #6701 also

[the-docta]

the workaround mentioned in #6701 using following code:

const { Context, em } = await z3.init();
// ... use Z3
em.PThread.terminateAllThreads();

works for me. this takes off the urgency. Yet, I still think, that Z3 should be taking care of the cleanup by itself. Or, at least, offer a documented method in the high level API, which should be called by the Z3 user after using Z3.

Thanks!