mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

[CMake] Guard Z3_API_LOG_SYNC against Z3_SINGLE_THREADED (#10088)

Browse source 
`Z3_API_LOG_SYNC` uses `std::mutex` to serialize API log writes across
threads. When combined with `Z3_SINGLE_THREADED`, all mutex operations
become no-ops (`SINGLE_THREAD` define strips them), silently defeating
the synchronization.

## Changes

- **`CMakeLists.txt`**: Emit `FATAL_ERROR` when both
`Z3_API_LOG_SYNC=ON` and `Z3_SINGLE_THREADED=ON` are set:
  ```
CMake Error: Z3_API_LOG_SYNC requires threading support and cannot be
combined with Z3_SINGLE_THREADED
  ```
- **`README-CMake.md`**: Expand `Z3_API_LOG_SYNC` description to clarify
its purpose and document the incompatibility with `Z3_SINGLE_THREADED`.

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
This commit is contained in:
Copilot 2026-07-11 19:20:15 -07:00 • committed by GitHub
parent 14e1dc9896
commit b0a77d2a58
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 5 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
CMakeLists.txt
View file

@ -258,6 +258,9 @@ option(Z3_SINGLE_THREADED
OFF
)
if (Z3_SINGLE_THREADED)
if (Z3_API_LOG_SYNC)
message(FATAL_ERROR "Z3_API_LOG_SYNC requires threading support and cannot be combined with Z3_SINGLE_THREADED")
endif()
list(APPEND Z3_COMPONENT_CXX_DEFINES "-DSINGLE_THREAD")
message(STATUS "Non-thread-safe build")
else()

2
README-CMake.md
View file

@ -441,6 +441,8 @@ The following useful options can be passed to CMake whilst configuring.
fail on other compilers. This does not require link time optimization. Control Flow Guard is enabled by default for MSVC builds.
Note: Control Flow Guard is incompatible with ``/ZI`` (Edit and Continue debug information) and ``/clr`` (Common Language Runtime compilation).
* ``Z3_API_LOG_SYNC`` - BOOL. If set to ``TRUE`` will enable experimental API log sync feature.
This uses locking to allow concurrent API log access across multiple threads. This option is
incompatible with ``Z3_SINGLE_THREADED``.
* ``WARNINGS_AS_ERRORS`` - STRING. If set to ``ON`` compiler warnings will be treated as errors. If set to ``OFF`` compiler warnings will not be treated as errors.
If set to ``SERIOUS_ONLY`` a subset of compiler warnings will be treated as errors.
* ``Z3_C_EXAMPLES_FORCE_CXX_LINKER`` - BOOL. If set to ``TRUE`` the C API examples will request that the C++ linker is used rather than the C linker.