Z3Prover / z3

The Z3 Theorem Prover
Other
10.35k stars 1.48k forks source link

NodeJs process won't stop after using 'solve' or 'solver.check()' #6512

Open eliachiarucci opened 1 year ago

eliachiarucci commented 1 year ago

I'm using Z3 on a personal project, I am able to get the results form the solve function, however, the process won't stop unless I force it with 'process.exit()'. This means that the return statement also doesn't work.

I'm now using some test code I found on the example folder to keep things simple. Using 'process._getActiveHandles()' reveals a couple of writeStream that gets created right after the solve function, I don't know if they are responsible for keeping the process open.

I'm using Node 18 but this problems also appears on Node 16, the code is running on an M1 Mac with MacOS.

async function test() {
  // Create 3 integer variables
  const { Context } = await init();

  const Z3 = new Context('main');
  const dog = Z3.Int.const('dog');
  const cat = Z3.Int.const('cat');
  const mouse = Z3.Int.const('mouse');

  const a = await Z3.solve(
    // there is at least one dog, one cat, and one mouse
    dog.ge(1),
    cat.ge(1),
    mouse.ge(1),

    // we want to buy 100 animals
    dog.add(cat.add(mouse)).eq(100),

    // We have 100 dollars (10000 cents):
    // dogs cost 15 dollars (1500 cents),
    // cats cost 1 dollar (100 cents), and
    // mice cost 25 cents
    dog.mul(1500).add(cat.mul(100)).add(mouse.mul(25)).eq(10000)
  );
  return a;
 }

return test();
bboysteed commented 3 months ago

same with you