From ce04a243488e02f7eb50bc98b72e01f219b5291f Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Tue, 24 Feb 2026 17:28:45 +0000
Subject: [PATCH] Improve TypeScript Optimize documentation for handle index
 clarity

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
---
 src/api/js/src/high-level/high-level.ts |  2 +-
 src/api/js/src/high-level/types.ts      | 26 +++++++++++++++++++++++--
 2 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/src/api/js/src/high-level/high-level.ts b/src/api/js/src/high-level/high-level.ts
index 9958af691..367696a12 100644
--- a/src/api/js/src/high-level/high-level.ts
+++ b/src/api/js/src/high-level/high-level.ts
@@ -2142,7 +2142,7 @@ export function createApi(Z3: Z3Core): Z3HighLevel {
       proof(): Expr<Name> | null {
         const result = Z3.solver_get_proof(contextPtr, this.ptr);
         throwIfError();
-        if (result === null) {
+        if (!result) {
           return null;
         }
         return _toExpr(result);
diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts
index 69a0f10eb..e070c4b58 100644
--- a/src/api/js/src/high-level/types.ts
+++ b/src/api/js/src/high-level/types.ts
@@ -1478,14 +1478,36 @@ export interface Optimize<Name extends string = 'main'> {
   /**
    * Add a maximization objective.
    * @param expr - The expression to maximize
-   * @returns A numeric handle index that can be used to retrieve bounds via {@link getLower}/{@link getUpper}
+   * @returns A zero-based numeric handle index for this objective, used to retrieve bounds
+   *          via {@link getLower}/{@link getUpper} after calling {@link check}
+   *
+   * @example
+   * ```typescript
+   * const opt = new Optimize();
+   * const x = Int.const('x');
+   * opt.add(x.ge(0), x.le(10));
+   * const h = opt.maximize(x);
+   * await opt.check();
+   * console.log('Max x:', opt.getUpper(h).toString()); // '10'
+   * ```
    */
   maximize(expr: Arith<Name> | BitVec<number, Name>): number;
 
   /**
    * Add a minimization objective.
    * @param expr - The expression to minimize
-   * @returns A numeric handle index that can be used to retrieve bounds via {@link getLower}/{@link getUpper}
+   * @returns A zero-based numeric handle index for this objective, used to retrieve bounds
+   *          via {@link getLower}/{@link getUpper} after calling {@link check}
+   *
+   * @example
+   * ```typescript
+   * const opt = new Optimize();
+   * const x = Int.const('x');
+   * opt.add(x.ge(0), x.le(10));
+   * const h = opt.minimize(x);
+   * await opt.check();
+   * console.log('Min x:', opt.getLower(h).toString()); // '0'
+   * ```
    */
   minimize(expr: Arith<Name> | BitVec<number, Name>): number;