From 8c80fe944063a36acfd1c902d0fc6b7c363189a5 Mon Sep 17 00:00:00 2001
From: "copilot-swe-agent[bot]" <198982749+Copilot@users.noreply.github.com>
Date: Mon, 13 Jul 2026 04:08:24 +0000
Subject: [PATCH] Address code review: extract INIT_GLOBAL constant in
 browser-singlethread.ts and fix Web Worker README example

- browser-singlethread.ts: extract 'initZ3SingleThread' into INIT_GLOBAL
  constant to avoid duplication between the global lookup and error message
- PUBLISHED_README.md: replace the dynamic import() in classic-worker
  example with consistent importScripts() pattern; add a separate module
  worker example using ES module import syntax
---
 src/api/js/PUBLISHED_README.md         | 30 +++++++++++++++++++++-----
 src/api/js/src/browser-singlethread.ts |  7 ++++--
 2 files changed, 30 insertions(+), 7 deletions(-)

diff --git a/src/api/js/PUBLISHED_README.md b/src/api/js/PUBLISHED_README.md
index 59db2ef584..c2135d7f12 100644
--- a/src/api/js/PUBLISHED_README.md
+++ b/src/api/js/PUBLISHED_README.md
@@ -50,13 +50,18 @@ import { init } from 'z3-solver/singlethread';
 The API is identical to the default export. The key difference is that all Z3 operations run **synchronously in the calling thread** rather than in a background thread. To avoid blocking the UI, run your Z3 code inside a [Web Worker](https://developer.mozilla.org/en-US/docs/Web/API/Web_Workers_API/Using_web_workers):
 
 ```javascript
-// my-z3-worker.js  (loaded as a Web Worker)
+// my-z3-worker.js  (loaded as a classic Web Worker)
 
-// 1. Load the single-threaded WASM artifact.
-importScripts('z3-built-singlethread.js');   // exposes initZ3SingleThread
+// 1. Load the single-threaded WASM artifact (exposes initZ3SingleThread globally).
+importScripts('z3-built-singlethread.js');
 
-// 2. Initialise Z3 (browser entry point reads initZ3SingleThread from global scope).
-const { init } = await import('z3-solver/singlethread');
+// 2. Load the single-threaded entry point as a classic script bundle.
+//    Most bundlers can produce a CJS/UMD build that can be loaded with importScripts.
+//    Alternatively, switch to a module worker (new Worker(..., { type: 'module' }))
+//    and use ES module import syntax instead.
+importScripts('z3-solver-singlethread-bundle.js'); // exposes Z3SolverSingleThread
+
+const { init } = Z3SolverSingleThread;
 const { Context } = await init();
 const { Solver, Int } = new Context('main');
 
@@ -67,6 +72,21 @@ solver.add(x.ge(0));
 self.postMessage(await solver.check()); // 'sat'
 ```
 
+Or with a **module worker** (supported in modern browsers):
+
+```javascript
+// my-z3-worker.mjs  (loaded as new Worker('...', { type: 'module' }))
+import { init } from 'z3-solver/singlethread';
+
+const { Context } = await init();
+const { Solver, Int } = new Context('main');
+
+const x = Int.const('x');
+const solver = new Solver();
+solver.add(x.ge(0));
+self.postMessage(await solver.check()); // 'sat'
+```
+
 The single-threaded WASM file (`z3-built-singlethread.js` / `z3-built-singlethread.wasm`) is distributed alongside the default build in the npm package.
 
 ## High-level
diff --git a/src/api/js/src/browser-singlethread.ts b/src/api/js/src/browser-singlethread.ts
index ff7cc90e8f..5facb80e1c 100644
--- a/src/api/js/src/browser-singlethread.ts
+++ b/src/api/js/src/browser-singlethread.ts
@@ -4,6 +4,9 @@ export * from './high-level/types';
 export { Z3Core, Z3LowLevel } from './low-level';
 export * from './low-level/types.__GENERATED__';
 
+// Name of the global exposed by z3-built-singlethread.js when loaded as a script.
+const INIT_GLOBAL = 'initZ3SingleThread';
+
 /**
  * Browser entry point for the single-threaded Z3 build.
  *
@@ -17,10 +20,10 @@ export * from './low-level/types.__GENERATED__';
  * worker), so that `initZ3SingleThread` is available on the global object.
  * @category Global */
 export async function init(moduleOverrides: Z3ModuleOverrides = {}): Promise<Z3LowLevel & Z3HighLevel> {
-  const initZ3 = (global as any).initZ3SingleThread;
+  const initZ3 = (global as any)[INIT_GLOBAL];
   if (initZ3 === undefined) {
     throw new Error(
-      'initZ3SingleThread was not found. ' +
+      `${INIT_GLOBAL} was not found. ` +
         'Load z3-built-singlethread.js before calling init() ' +
         '(e.g. importScripts("z3-built-singlethread.js") in a Web Worker).',
     );