Fix memory lifetime bug in async array parameter handling for JS API (#8125)

* Initial plan

* Fix async array parameter handling in JS API wrappers

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add test for solver.check() with assumptions

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Address code review feedback: add null checks and improve readability

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

* Add unsatCore() method to Solver class

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

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

src/api/js/src/high-level/high-level.test.ts

@@ -174,6 +174,29 @@ describe('high-level', () => {
       expect(await solver.check()).toStrictEqual('unsat');
     });
 
+    it('can check with assumptions and get unsat core', async () => {
+      const { Bool, Solver } = api.Context('main');
+      const solver = new Solver();
+      solver.set('unsat_core', true);
+      
+      const x = Bool.const('x');
+      const y = Bool.const('y');
+      const z = Bool.const('z');
+
+      // Add conflicting assertions
+      solver.add(x.or(y));
+      solver.add(x.or(z));
+
+      // Check with assumptions that create a conflict
+      // This tests the async array parameter fix
+      const result = await solver.check(x.not(), y.not(), z.not());
+      expect(result).toStrictEqual('unsat');
+      
+      // Verify we can get the unsat core
+      const core = solver.unsatCore();
+      expect(core.length()).toBeGreaterThan(0);
+    });
+
     it("proves De Morgan's Law", async () => {
       const { Bool, Not, And, Eq, Or } = api.Context('main');
       const [x, y] = [Bool.const('x'), Bool.const('y')];

src/api/js/src/high-level/high-level.ts

@@ -1463,6 +1463,10 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
         return new ModelImpl(check(Z3.solver_get_model(contextPtr, this.ptr)));
       }
 
+      unsatCore(): AstVector<Name, Bool<Name>> {
+        return new AstVectorImpl(check(Z3.solver_get_unsat_core(contextPtr, this.ptr)));
+      }
+
       toString() {
         return check(Z3.solver_to_string(contextPtr, this.ptr));
       }

src/api/js/src/high-level/types.ts

@@ -713,6 +713,8 @@ export interface Solver<Name extends string = 'main'> {
 
   model(): Model<Name>;
 
+  unsatCore(): AstVector<Name, Bool<Name>>;
+
   /**
    * Manually decrease the reference count of the solver
    * This is automatically done when the solver is garbage collected,