mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-08-02 20:23:27 +00:00
Code Activity
z3/src/api
History
Copilot 88612e329e
Export killThreads from z3-solver to allow Node.js thread cleanup (#10320) 
Emscripten worker threads spawned for long-running Z3 operations (e.g.
`solver.check()`) are never cleaned up, keeping the Node.js process
alive after Z3 is done.

The `killThreads` helper already existed internally in `jest.ts` but was
never part of the public package.

## Changes

- **`src/kill-threads.ts`** (new) — extracts `killThreads(em)` into a
standalone module; calls `em.PThread.terminateAllThreads()` then polls
until all workers are gone (5 s timeout)
- **`src/node.ts`** — re-exports `killThreads` so it is part of the
published `z3-solver` API
- **`src/jest.ts`** — simplified to re-export from `./kill-threads`
instead of duplicating ~45 lines
- **`src/kill-threads.test.ts`** (new) — unit tests for the exported
function
- **`PUBLISHED_README.md`** — documents the new API

## Usage

```typescript
import { init, killThreads } from 'z3-solver';

const api = await init();
// ... use Z3 ...
await killThreads(api.em);
```

<!-- START COPILOT CODING AGENT SUFFIX -->

- Fixes #7070

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
2026-07-31 12:00:04 -07:00
..
c++ Fixes necessary to compile z3 included in clang-tidy via FetchContents. (#9768) 2026-06-08 19:44:01 -07:00
dll Tabs, formatting. 2017-09-17 14:54:09 +01:00
dotnet Fix .NET API memory leak: NativeContext finalizer, delegate lifetime, GC memory pressure (#10090) 2026-07-11 21:15:36 -07:00
go Go bindings: enable concurrent dec_ref for GC-driven finalizers (#10002) 2026-06-29 13:14:41 -06:00
java Java API: return EnumSort instead of DatatypeSort from Sort.create() (#10104) 2026-07-12 21:46:46 -07:00
js Export killThreads from z3-solver to allow Node.js thread cleanup (#10320) 2026-07-31 12:00:04 -07:00
julia fix issues 1-10: add missing API bindings across Go, Julia, TypeScript, OCaml, and Java (#9432) 2026-05-04 09:29:47 -07:00
mcp remove non-working ts mcp server, settle with python variant 2025-04-18 10:10:12 -07:00
ml Expose Seq.mk_re_diff in ocaml bindings (#9584) 2026-05-21 10:29:08 -07:00
python Load versioned libz3 soname in Python bindings on Linux (#10290) 2026-07-29 14:01:55 -07:00
api_algebraic.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_arith.cpp Use macros to disable semi-colon warnings for blocks of macros. (#10192) 2026-07-22 18:01:50 -07:00
api_array.cpp Use macros to disable semi-colon warnings for blocks of macros. (#10192) 2026-07-22 18:01:50 -07:00
api_ast.cpp Use macros to disable semi-colon warnings for blocks of macros. (#10192) 2026-07-22 18:01:50 -07:00
api_ast_map.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_ast_map.h booyah 2020-07-04 15:56:30 -07:00
api_ast_vector.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_ast_vector.h Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_bv.cpp Use macros to disable semi-colon warnings for blocks of macros. (#10192) 2026-07-22 18:01:50 -07:00
api_config_params.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_context.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_context.h Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_datalog.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_datalog.h Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_datatype.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_finite_set.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_fpa.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_goal.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_goal.h Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
api_log.cpp api: avoid some string copies when using mk_external_string 2024-12-28 09:42:54 +00:00
api_model.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_model.h Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
api_numeral.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_opt.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_params.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_parsers.cpp add py_value to selected classes in python bindings, add mode for input-assertion based lookahead solving 2025-01-04 13:40:49 -08:00
api_pb.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_polynomial.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_polynomial.h remove a hundred implicit constructors/destructors 2021-05-23 14:25:01 +01:00
api_qe.cpp filter out terms that are not solved 2025-04-30 09:40:45 -07:00
api_quant.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_rcf.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_seq.cpp Use macros to disable semi-colon warnings for blocks of macros. (#10192) 2026-07-22 18:01:50 -07:00
api_solver.cpp Prevent Z3_solver_reset abort after memory_max_size OOM by making reset memory-limit-safe (#10254) 2026-07-27 12:46:32 -07:00
api_solver.h add API for creating and attaching simplifiers 2023-01-31 17:06:03 -08:00
api_special_relations.cpp Use macros to disable semi-colon warnings for blocks of macros. (#10192) 2026-07-22 18:01:50 -07:00
api_stats.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_stats.h Remove empty leaf destructors. (#6211) 2022-07-30 10:07:03 +01:00
api_tactic.cpp Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
api_tactic.h add API for creating and attaching simplifiers 2023-01-31 17:06:03 -08:00
api_util.h Remove unnecessary semicolons (Attempt 2) (#10020) 2026-07-02 12:47:29 -07:00
CMakeLists.txt Fixes necessary to compile z3 included in clang-tidy via FetchContents. (#9768) 2026-06-08 19:44:01 -07:00
z3.h z3.h: Don't include stdio.h (#7014) 2023-11-24 16:46:32 +01:00
z3_algebraic.h fix grouping for latest doxygen (#5626) 2021-10-27 23:46:31 +02:00
z3_api.h Fix documentation for Z3_solver_to_dimacs_string (#9053) 2026-03-20 10:18:13 -07:00
z3_ast_containers.h fix grouping for latest doxygen (#5626) 2021-10-27 23:46:31 +02:00
z3_fixedpoint.h Added function to select the next variable to split on (User-Propagator) (#6096) 2022-06-19 10:49:25 -07:00
z3_fpa.h Return sign from Z3_fpa_get_numeral_sign as bool instead of int (#8047) 2026-02-18 20:56:01 -08:00
z3_logger.h Make sure all headers do #pragma once. (#6188) 2022-07-23 10:41:14 -07:00
z3_macros.h Make sure all headers do #pragma once. (#6188) 2022-07-23 10:41:14 -07:00
z3_optimization.h Implement Z3_optimize_translate for context translation (#8072) 2026-02-18 20:56:58 -08:00
z3_polynomial.h fix grouping for latest doxygen (#5626) 2021-10-27 23:46:31 +02:00
z3_private.h remove '#include <iostream>' from headers and from unneeded places 2022-06-17 14:10:19 +01:00
z3_rcf.h Return bool instead of int from Z3_rcf_interval (#8046) 2026-02-18 20:56:01 -08:00
z3_replayer.cpp Fix clang warnings about casting away const. (#9933) 2026-06-23 19:57:46 -06:00
z3_replayer.h Return sign from Z3_fpa_get_numeral_sign as bool instead of int (#8047) 2026-02-18 20:56:01 -08:00
z3_spacer.h add projection with witnesses 2024-11-27 10:26:34 -08:00
z3_v1.h booyah 2020-07-04 15:56:30 -07:00