diff --git a/src/api/js/src/high-level/types.ts b/src/api/js/src/high-level/types.ts index 26036ad85..bd4f9dcc2 100644 --- a/src/api/js/src/high-level/types.ts +++ b/src/api/js/src/high-level/types.ts @@ -125,6 +125,7 @@ export type CheckSatResult = 'sat' | 'unsat' | 'unknown'; /** @hidden */ export interface ContextCtor { (name: Name, options?: Record): Context; + new (name: Name, options?: Record): Context; } export interface Context { diff --git a/src/api/js/src/node.ts b/src/api/js/src/node.ts index 6456d8979..9e503edcd 100644 --- a/src/api/js/src/node.ts +++ b/src/api/js/src/node.ts @@ -11,7 +11,7 @@ export * from './low-level/types.__GENERATED__'; * The main entry point to the Z3 API * * ```typescript - * import { init, sat } from 'z3-solver'; + * import { init } from 'z3-solver'; * * const { Context } = await init(); * const { Solver, Int } = new Context('main'); @@ -22,7 +22,7 @@ export * from './low-level/types.__GENERATED__'; * const solver = new Solver(); * solver.add(x.add(2).le(y.sub(10))); // x + 2 <= y - 10 * - * if (await solver.check() !== sat) { + * if (await solver.check() !== 'sat') { * throw new Error("couldn't find a solution") * } * const model = solver.model();