From 79bc59b792db51b6c4b355171d7f145b59b8844a Mon Sep 17 00:00:00 2001 From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com> Date: Sat, 17 Jan 2026 20:29:46 +0000 Subject: [PATCH] Fix RCFNum cleanup callback to avoid capturing 'this' The cleanup callback was capturing 'this.ptr' which could cause issues with the FinalizationRegistry. Changed to use a local variable 'myPtr' instead, following the pattern used by other implementations in the codebase (e.g., SolverImpl, ModelImpl). Also format low-level rcf-example.ts for consistency. Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com> --- src/api/js/examples/low-level/rcf-example.ts | 10 +++++----- src/api/js/src/high-level/high-level.ts | 10 ++++++---- 2 files changed, 11 insertions(+), 9 deletions(-) diff --git a/src/api/js/examples/low-level/rcf-example.ts b/src/api/js/examples/low-level/rcf-example.ts index 6cead416c..cb516522c 100644 --- a/src/api/js/examples/low-level/rcf-example.ts +++ b/src/api/js/examples/low-level/rcf-example.ts @@ -1,12 +1,12 @@ /** * Example demonstrating the RCF (Real Closed Field) API in TypeScript. - * + * * This example shows how to use RCF numerals to work with: * - Transcendental numbers (pi, e) * - Algebraic numbers (roots of polynomials) * - Infinitesimals * - Exact real arithmetic - * + * * Note: The RCF API is exposed at the low-level API layer. * Import from 'z3-solver' for low-level access. */ @@ -96,9 +96,9 @@ async function rcfRootsExample() { // Find roots of x^2 - 2 = 0 // Polynomial: -2 + 0*x + 1*x^2 const coeffs = [ - Z3.rcf_mk_small_int(ctx, -2), // constant term - Z3.rcf_mk_small_int(ctx, 0), // x coefficient - Z3.rcf_mk_small_int(ctx, 1) // x^2 coefficient + Z3.rcf_mk_small_int(ctx, -2), // constant term + Z3.rcf_mk_small_int(ctx, 0), // x coefficient + Z3.rcf_mk_small_int(ctx, 1), // x^2 coefficient ]; const roots = new Array(coeffs.length); diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts index 22d2a98ba..1b8ada695 100644 --- a/src/api/js/src/high-level/high-level.ts +++ b/src/api/js/src/high-level/high-level.ts @@ -3413,14 +3413,16 @@ export function createApi(Z3: Z3Core): Z3HighLevel { constructor(ptr: Z3_rcf_num); constructor(valueOrPtr: string | number | Z3_rcf_num) { this.ctx = ctx; + let myPtr: Z3_rcf_num; if (typeof valueOrPtr === 'string') { - this.ptr = check(Z3.rcf_mk_rational(contextPtr, valueOrPtr)); + myPtr = check(Z3.rcf_mk_rational(contextPtr, valueOrPtr)); } else if (typeof valueOrPtr === 'number') { - this.ptr = check(Z3.rcf_mk_small_int(contextPtr, valueOrPtr)); + myPtr = check(Z3.rcf_mk_small_int(contextPtr, valueOrPtr)); } else { - this.ptr = valueOrPtr; + myPtr = valueOrPtr; } - cleanup.register(this, () => Z3.rcf_del(contextPtr, this.ptr), this); + this.ptr = myPtr; + cleanup.register(this, () => Z3.rcf_del(contextPtr, myPtr), this); } add(other: RCFNum): RCFNum {