diff --git a/CMakeLists.txt b/CMakeLists.txt index 491cb996b7..ae57d5b2f4 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -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() diff --git a/README-CMake.md b/README-CMake.md index c9edb93783..f2ffca30fc 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -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.