Export killThreads from z3-solver to allow Node.js thread cleanup (#10320)

Emscripten worker threads spawned for long-running Z3 operations (e.g.
`solver.check()`) are never cleaned up, keeping the Node.js process
alive after Z3 is done.

The `killThreads` helper already existed internally in `jest.ts` but was
never part of the public package.

## Changes

- **`src/kill-threads.ts`** (new) — extracts `killThreads(em)` into a
standalone module; calls `em.PThread.terminateAllThreads()` then polls
until all workers are gone (5 s timeout)
- **`src/node.ts`** — re-exports `killThreads` so it is part of the
published `z3-solver` API
- **`src/jest.ts`** — simplified to re-export from `./kill-threads`
instead of duplicating ~45 lines
- **`src/kill-threads.test.ts`** (new) — unit tests for the exported
function
- **`PUBLISHED_README.md`** — documents the new API

## Usage

```typescript
import { init, killThreads } from 'z3-solver';

const api = await init();
// ... use Z3 ...
await killThreads(api.em);
```

<!-- START COPILOT CODING AGENT SUFFIX -->

- Fixes #7070

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>

src/api/js/PUBLISHED_README.md

@@ -27,7 +27,17 @@ const api = await init({
 });
 ```
 
-### Limitations
+### Thread cleanup (Node.js)
+
+Long-running Z3 operations run on background worker threads. In Node.js, these workers keep the process alive even after Z3 has finished. Once you are done using Z3, call `killThreads` to terminate them and allow the process to exit cleanly.
+
+```typescript
+import { init, killThreads } from 'z3-solver';
+
+const api = await init();
+// ... use Z3 ...
+await killThreads(api.em);
+```
 
 The package requires threads, which means you'll need to be running in an environment which supports `SharedArrayBuffer`. In browsers, in addition to ensuring the browser has implemented `SharedArrayBuffer`, you'll need to serve your page with [special headers](https://web.dev/coop-coep/). There's a [neat trick](https://github.com/gzuidhof/coi-serviceworker) for doing that client-side on e.g. Github Pages, though you shouldn't use that trick in more complex applications.
 

src/api/js/src/jest.ts

@@ -8,6 +8,7 @@ import initModule = require('../build/z3-built');
 export * from './high-level/types';
 export { Z3Core, Z3LowLevel } from './low-level';
 export * from './low-level/types.__GENERATED__';
+export { killThreads } from './kill-threads';
 
 export async function init(): Promise<Z3HighLevel & Z3LowLevel> {
   const lowLevel = await initWrapper(initModule);
@@ -15,48 +16,3 @@ export async function init(): Promise<Z3HighLevel & Z3LowLevel> {
   return { ...lowLevel, ...highLevel };
 }
 
-function delay(ms: number): Promise<void> & { cancel(): void };
-function delay(ms: number, result: Error): Promise<never> & { cancel(): void };
-function delay<T>(ms: number, result: T): Promise<T> & { cancel(): void };
-function delay<T>(ms: number, result?: T | Error): Promise<T | void> & { cancel(): void } {
-  let handle: any;
-  const promise = new Promise<void | T>(
-    (resolve, reject) =>
-      (handle = setTimeout(() => {
-        if (result instanceof Error) {
-          reject(result);
-        } else if (result !== undefined) {
-          resolve(result);
-        }
-        resolve();
-      }, ms)),
-  );
-  return { ...promise, cancel: () => clearTimeout(handle) };
-}
-
-function waitWhile(premise: () => boolean, pollMs: number = 100): Promise<void> & { cancel(): void } {
-  let handle: any;
-  const promise = new Promise<void>(resolve => {
-    handle = setInterval(() => {
-      if (premise()) {
-        clearTimeout(handle);
-        resolve();
-      }
-    }, pollMs);
-  });
-  return { ...promise, cancel: () => clearInterval(handle) };
-}
-
-export function killThreads(em: any): Promise<void> {
-  em.PThread.terminateAllThreads();
-
-  // Create a polling lock to wait for threads to return
-  // TODO(ritave): Threads should be killed automatically, or there should be a better way to wait for them
-  const lockPromise = waitWhile(() => !em.PThread.unusedWorkers.length && !em.PThread.runningWorkers.length);
-  const delayPromise = delay(5000, new Error('Waiting for threads to be killed timed out'));
-
-  return Promise.race([lockPromise, delayPromise]).finally(() => {
-    lockPromise.cancel();
-    delayPromise.cancel();
-  });
-}

src/api/js/src/kill-threads.test.ts

@@ -0,0 +1,45 @@
+import { killThreads } from './kill-threads';
+
+describe('killThreads', () => {
+  it('calls terminateAllThreads and resolves when workers are already gone', async () => {
+    const unusedWorkers: unknown[] = [];
+    const runningWorkers: unknown[] = [];
+    const mockEm = {
+      PThread: {
+        terminateAllThreads: jest.fn(),
+        get unusedWorkers() {
+          return unusedWorkers;
+        },
+        get runningWorkers() {
+          return runningWorkers;
+        },
+      },
+    };
+
+    await killThreads(mockEm);
+
+    expect(mockEm.PThread.terminateAllThreads).toHaveBeenCalledTimes(1);
+  });
+
+  it('resolves once running workers are terminated', async () => {
+    const runningWorkers: unknown[] = [{}];
+    const mockEm = {
+      PThread: {
+        terminateAllThreads: jest.fn(),
+        unusedWorkers: [] as unknown[],
+        get runningWorkers() {
+          return runningWorkers;
+        },
+      },
+    };
+
+    // Simulate workers being terminated after a short delay.
+    setTimeout(() => {
+      runningWorkers.length = 0;
+    }, 150);
+
+    await killThreads(mockEm);
+
+    expect(mockEm.PThread.terminateAllThreads).toHaveBeenCalledTimes(1);
+  });
+});

src/api/js/src/kill-threads.ts

@@ -0,0 +1,43 @@
+/**
+ * Terminates all Emscripten worker threads spawned by Z3.
+ *
+ * Long-running Z3 operations (such as `solver.check()`) run on background
+ * worker threads. In Node.js these workers keep the process alive even after
+ * Z3 has finished. Call this function once you are done using Z3 to allow the
+ * Node.js process to exit cleanly.
+ *
+ * ```typescript
+ * import { init, killThreads } from 'z3-solver';
+ *
+ * const api = await init();
+ * // ... use Z3 ...
+ * await killThreads(api.em);
+ * ```
+ * @category Global
+ */
+export function killThreads(em: any): Promise<void> {
+  em.PThread.terminateAllThreads();
+
+  // Poll until all workers have been terminated.
+  let intervalHandle: ReturnType<typeof setInterval>;
+  let timeoutHandle: ReturnType<typeof setTimeout>;
+
+  const lockPromise = new Promise<void>(resolve => {
+    intervalHandle = setInterval(() => {
+      if (!em.PThread.unusedWorkers.length && !em.PThread.runningWorkers.length) {
+        clearInterval(intervalHandle);
+        clearTimeout(timeoutHandle);
+        resolve();
+      }
+    }, 100);
+  });
+
+  const delayPromise = new Promise<never>((_, reject) => {
+    timeoutHandle = setTimeout(() => {
+      clearInterval(intervalHandle);
+      reject(new Error('Waiting for threads to be killed timed out'));
+    }, 5000);
+  });
+
+  return Promise.race([lockPromise, delayPromise]);
+}

src/api/js/src/node.ts

@@ -6,6 +6,7 @@ import { init as initWrapper, Z3LowLevel, Z3ModuleOverrides } from './low-level'
 export * from './high-level/types';
 export { Z3Core, Z3LowLevel } from './low-level';
 export * from './low-level/types.__GENERATED__';
+export { killThreads } from './kill-threads';
 
 /**
  * The main entry point to the Z3 API