Z3 doesn't work in Bun #19453
Description
What version of Bun is running?
1.2.11+cb6abd211
What platform is your computer?
Microsoft Windows NT 10.0.19045.0 x64
What steps can reproduce the bug?
Run this code for z3 in bun (which perfectly works via tsx but not in bun unless it is compiled to js for node).
import { init } from 'z3-solver';
const { Context } = await init()
const { Solver, Int, And } = Context('main');
const x = Int.const('x');
const y = Int.const('y')
const solver = new Solver();
solver.add(x.mul(3).add(y.mul(2)).eq(0));
solver.add(y.mul(3).sub(x.mul(2)).eq(0))
let numSolutions = 0;
while (await solver.check() === 'sat') {
const model = solver.model();
console.log(`Solution #${++numSolutions}:`);
console.log(` x = ${model.eval(x).toString()}`);
console.log(` y = ${model.eval(y).toString()}`);
const block = And(x.neq(model.eval(x)),
y.neq(model.eval(y)));
solver.add(block);
}
if (numSolutions === 0) {
console.log('No solution found.');
}What is the expected behavior?
Console output:
Solution #1:
x = 0
y = 0
What do you see instead?
Aborted(Assertion failed)
worker: onmessage() captured an uncaught exception: RuntimeError: Aborted(Assertion failed)
RuntimeError: Aborted(Assertion failed)
at abort (C:\Users\Duck\Desktop\Projects\node_modules\z3-solver\build\z3-built.js:848:27)
at assert (C:\Users\Duck\Desktop\Projects\node_modules\z3-solver\build\z3-built.js:396:5)
at removeRunDependency (C:\Users\Duck\Desktop\Projectst\node_modules\z3-solver\build\z3-built.js:805:5)
at receiveInstance (C:\Users\Duck\Desktop\Projects\node_modules\z3-solver\build\z3-built.js:1019:5)
at wasmModuleReceived (C:\Users\Duck\Desktop\Projects\node_modules\z3-solver\build\z3-built.js:1062:9)
at handleMessage (C:\Users\Duck\Desktop\Projects\node_modules\z3-solver\build\z3-built.js:539:9)
Pthread 0x01d1dfc8 sent an error! undefined:undefined: 843 | // Suppress closure compiler warning here. Closure compiler's builtin extern
844 | // definition for WebAssembly.RuntimeError claims it takes no arguments even
845 | // though it can.
846 | // TODO(https://github.com/google/closure-compiler/pull/3913): Remove if/when upstream closure gets fixed.
847 | /** @suppress {checkTypes} */
848 | var e = new WebAssembly.RuntimeError(what);
^
RuntimeError: Aborted(Assertion failed)
at abort (C:\Users\Duck\Desktop\Projects\node_modules\z3-solver\build\z3-built.js:848:27)
1616 | var message = 'worker sent an error!';
1617 | if (worker.pthread_ptr) {
1618 | message = `Pthread ${ptrToString(worker.pthread_ptr)} sent an error!`;
1619 | }
1620 | err(`${message} ${e.filename}:${e.lineno}: ${e.message}`);
1621 | throw e;
^
error: 843 | // Suppress closure compiler warning here. Closure compiler's builtin extern
844 | // definition for WebAssembly.RuntimeError claims it takes no arguments even
845 | // though it can.
846 | // TODO(https://github.com/google/closure-compiler/pull/3913): Remove if/when upstream closure gets fixed.
847 | /** @suppress {checkTypes} */
848 | var e = new WebAssembly.RuntimeError(what);
^
RuntimeError: Aborted(Assertion failed)
at abort (C:\Users\Duck\Desktop\Projects\node_modules\z3-solver\build\z3-built.js:848:27)
at <anonymous> (C:\Users\Duck\Desktop\Projects\node_modules\z3-solver\build\z3-built.js:1621:17)
at <anonymous> (C:\Users\Duck\Desktop\Projects\node_modules\z3-solver\build\z3-built.js:1626:44)
at emitError (node:events:20:23)
at #onError (node:worker_threads:210:14)
Additional information
After outputting the error, the process doesn't exit. It's just stuck there.