Javascript & Typescript API Runs Forever

[AZ-AdamDiehl]

There seems to be an issue with the async mechanism used in the Javascript/Typescript API (ref: https://www.npmjs.com/package/z3-solver). Specifically, the async process spawned never terminates (and the undocumented workaround in the tests also seems to be failing).

Minimal Working Example

A minimal example is the following test in Jest, which will produce the warning seen below (or will hang forever if the code is extracted and run outside a test environment):

import { init } from 'z3-solver';

test('basic example', async () => {
    const { Context } = await init();
    const Z3 = Context('main');

    const x = Z3.Int.const('x');
    const y = Z3.Int.const('y');

    const solver = new Z3.Solver();
    solver.add(x.add(2).le(y.sub(10))); // x + 2 <= y - 10

    let sat = await solver.check();
    expect(sat).toBe("sat");

    const model = solver.model();
    expect(`${model.get(x)}`).toBe("0");
    expect(`${model.get(y)}`).toBe("12");
});

Result:

A worker process has failed to exit gracefully and has been force exited. This is likely caused by tests leaking due to improper teardown.  ...

For context, if you runt this outside a test environment, the spawned thread never yields/terminates and must be manually killed.

Failing Workaround

The test file here appears to show an undocumented workaround, which is to import em alongside Context and run em.PThread.terminateAllThreads();.

However, I tried this, and it produces the same result.

Code:

import { init } from 'z3-solver';

test('basic example', async () => {
    const { Context, em } = await init();
    const Z3 = Context('main');

    const x = Z3.Int.const('x');
    const y = Z3.Int.const('y');

    const solver = new Z3.Solver();
    solver.add(x.add(2).le(y.sub(10))); // x + 2 <= y - 10

    let sat = await solver.check();
    expect(sat).toBe("sat");

    const model = solver.model();
    expect(`${model.get(x)}`).toBe("0");
    expect(`${model.get(y)}`).toBe("12");
    em.PThread.terminateAllThreads();
});

Result:

A worker process has failed to exit gracefully and has been force exited. This is likely caused by tests leaking due to improper teardown. 

[AZ-AdamDiehl]

Following up on this, I found another workaround in the test files here. It seems like the thread handling issue is known. https://github.com/Z3Prover/z3/blob/87dd837b551fa8650ef1be10f0ee3c1f56e106b9/src/api/js/src/jest.ts

However, this killThreads function doesn't seem to resolve the issue for me either (still have to force timeout).

[bboysteed]

same trouble!

[the-docta]

@bboysteed

I was able to work around like this:

// init
const { Context, em } = await z3.init();

/* do stuff */

// clean up threads
em.PThread.terminateAllThreads();

which is basically the workaround in the test liked above