Why is this program 10x slowing using the NodeJS Z3 bindings instead of the Python ones

Question

I have written the following z3 program in JS and Python bindings. It appears Python is 10x faster for the same input problem (for the curious this is https://www.reddit.com/r/adventofcode/comments/a8s17l/2018_day_23_solutions/)

solver = Optimize()
x, y, z = Ints('x y z')
sp = []
for sensor in sensors:
    sp.append(If(Abs(sensor[0] - x) + Abs(sensor[1] - y) + Abs(sensor[2] - z) <= sensor[3], 1, 0))
solver.maximize(Sum(sp))
solver.minimize(x + y + z)
solver.check()
print(solver.model())

function abs(x: z3.Arith<'main'>): z3.Arith<'main'> {
    return If(x.ge(0), x, x.neg());
}


let {Z3, Context} = await z3.init();
let {Int, If, Optimize} = Context('main');

let x = Int.const('x');
let y = Int.const('y');
let z = Int.const('z');
let bs: z3.Arith<'main'>[] = [];
for (let s of sensors) {
    let d = abs(x.sub(s.x)).add(abs(y.sub(s.y)).add(abs(z.sub(s.z))));
    let b = If(d.le(s.r), 1, 0);
    bs.push(b);
}
let sum = bs.reduce((a, b) => a.add(b));
let opt = new Optimize();
opt.maximize(sum);
opt.minimize(x.add(y).add(z));
await opt.check();

Is there anything I can do to optimize the JS bindings (I rather keep using those, but not at such a runtime cost).