diff --git a/.gitignore b/.gitignore
index 7236839d31..1bc2c93453 100644
--- a/.gitignore
+++ b/.gitignore
@@ -60,6 +60,5 @@ tags
 
 /arch_flags
 
-/cmake
 /cscope
 abc.history
\ No newline at end of file
diff --git a/CMakeLists.txt b/CMakeLists.txt
index bbb153e642..6fc0f5f567 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,130 +1,333 @@
-cmake_minimum_required(VERSION 3.5.0)
+cmake_minimum_required(VERSION 3.25)
 
-include(CMakeParseArguments)
-include(CheckCCompilerFlag)
-include(CheckCXXCompilerFlag)
-# Generate compilation database compile_commands.json
-set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
+project(abc
+    VERSION 1.0.0
+    DESCRIPTION "ABC: System for Sequential Logic Synthesis and Formal Verification"
+    HOMEPAGE_URL "https://people.eecs.berkeley.edu/~alanmi/abc/"
+    LANGUAGES C CXX
+)
+
+include(GNUInstallDirs)
+
+if (MSVC)
+
+    set(CMAKE_C_STANDARD 11)
+    set(CMAKE_C_STANDARD_REQUIRED ON)
+    set(CMAKE_C_EXTENSIONS ON)
+    set(CMAKE_CXX_STANDARD 17)
+    set(CMAKE_CXX_STANDARD_REQUIRED ON)
 
-# Default c++ standard used unless otherwise specified in target_compile_features.
-set(CMAKE_CXX_STANDARD 17 CACHE STRING "the C++ standard to use for this project")
-set(CMAKE_CXX_STANDARD_REQUIRED ON)
+    # Embed debug info in each .obj instead of writing to a shared .pdb. With
+    # ~1370 parallel TUs the shared PDB triggers C1041 even with /FS.
+    # CMP0141 (CMake 3.25+) routes this through MSBuild's
+    # <DebugInformationFormat> rather than injecting /Zi into CMAKE_*_FLAGS_*.
+    set(CMAKE_MSVC_DEBUG_INFORMATION_FORMAT "$<$<CONFIG:Debug,RelWithDebInfo>:Embedded>")
 
-function(addprefix var prefix)
-    foreach( s ${ARGN} )
-        list(APPEND tmp "-I${s}")
+
+    # Source discovery: parse the per-directory module.make files. The upstream 
+    # Makefile (Makefile:35-53,91,171) treats those module.make files as the canonical
+    # source list;
+    file(READ "${CMAKE_CURRENT_SOURCE_DIR}/Makefile" abc_mk_text)
+    string(REGEX REPLACE "\\\\[\r\n]+" " " abc_mk_text "${abc_mk_text}")
+    string(REGEX MATCH "MODULES[ \t]*:=[^\n]*" abc_mk_init "${abc_mk_text}")
+    string(REGEX MATCHALL "MODULES[ \t]*\\+=[^\n]+" abc_mk_appends "${abc_mk_text}")
+    set(abc_mk_modules "${abc_mk_init}")
+    foreach(abc_mk_line IN LISTS abc_mk_appends)
+        string(APPEND abc_mk_modules " ${abc_mk_line}")
     endforeach()
-    set(${var} ${tmp} PARENT_SCOPE)
-endfunction()
-
-# filter out flags that are not appropriate for the compiler being used
-function(target_compile_options_filtered target visibility)
-    foreach( flag ${ARGN} )
-        if( flag MATCHES "^-D.*" )
-            target_compile_options( ${target} ${visibility} ${flag} )
-        else()
-            check_c_compiler_flag( ${flag} C_COMPILER_SUPPORTS__${flag} )
-            if( C_COMPILER_SUPPORTS__${flag} )
-                target_compile_options( ${target} ${visibility} $<$<COMPILE_LANGUAGE:C>:${flag}> )
-            endif()
 
-            check_cxx_compiler_flag( ${flag} CXX_COMPILER_SUPPORTS__${flag} )
-            if( CXX_COMPILER_SUPPORTS__${flag} )
-                target_compile_options( ${target} ${visibility} $<$<COMPILE_LANGUAGE:CXX>:${flag}>  )
-            endif()
+    file(GLOB abc_ext_dirs RELATIVE "${CMAKE_CURRENT_SOURCE_DIR}"
+        "${CMAKE_CURRENT_SOURCE_DIR}/src/ext*")
+    string(JOIN " " abc_ext_str ${abc_ext_dirs})
+    string(REGEX REPLACE "\\$\\(wildcard[^)]+\\)" "${abc_ext_str}"
+        abc_mk_modules "${abc_mk_modules}")
+
+    string(REGEX MATCHALL "src/[A-Za-z0-9_/]+" ABC_MODULES "${abc_mk_modules}")
+    list(REMOVE_DUPLICATES ABC_MODULES)
+    list(LENGTH ABC_MODULES ABC_MODULES_COUNT)
+    message(STATUS "abc: ${ABC_MODULES_COUNT} module dirs discovered from Makefile")
+
+    set(ABC_SRC "")
+    foreach(abc_mod IN LISTS ABC_MODULES)
+        set(abc_mod_file "${CMAKE_CURRENT_SOURCE_DIR}/${abc_mod}/module.make")
+        if(NOT EXISTS "${abc_mod_file}")
+            message(WARNING "abc: missing ${abc_mod_file}")
+            continue()
         endif()
+        file(READ "${abc_mod_file}" abc_mod_text)
+        # collapse "\<newline>" line continuations so each path is one token
+        string(REGEX REPLACE "\\\\[\r\n]+" " " abc_mod_text "${abc_mod_text}")
+        # alternation must list cpp before c — CMake regex picks the first match, not the longest
+        string(REGEX MATCHALL "src/[A-Za-z0-9_/]+\\.(cpp|c)" abc_mod_srcs "${abc_mod_text}")
+        foreach(abc_src_rel IN LISTS abc_mod_srcs)
+            set(abc_src_abs "${CMAKE_CURRENT_SOURCE_DIR}/${abc_src_rel}")
+            if(NOT EXISTS "${abc_src_abs}")
+                message(FATAL_ERROR "abc: ${abc_mod_file} references missing ${abc_src_rel}")
+            endif()
+            list(APPEND ABC_SRC "${abc_src_abs}")
+        endforeach()
     endforeach()
-endfunction()
 
-project(abc)
+    list(LENGTH ABC_SRC ABC_SRC_COUNT)
+    message(STATUS "abc: ${ABC_SRC_COUNT} sources from module.make files")
 
-if(READLINE_FOUND MATCHES TRUE)
-    addprefix(ABC_READLINE_INCLUDES_FLAGS "-I" ${READLINE_INCLUDE})
-    string(REPLACE ";" " " ABC_READLINE_INCLUDES_FLAGS "${ABC_READLINE_INCLUDES_FLAGS}")
-    list(APPEND ABC_READLINE_FLAGS "ABC_READLINE_INCLUDES=${ABC_READLINE_INCLUDES_FLAGS}")
+    # UfarPth.cpp unconditionally references pthread_*; supply no-op stubs for the linker
+    list(APPEND ABC_SRC "${CMAKE_CURRENT_SOURCE_DIR}/src/opt/ufar/UfarPthStub.c")
 
-    string(REPLACE ";" " " ABC_READLINE_LIBRARIES_FLAGS "${READLINE_LIBRARIES}")
-    list(APPEND ABC_READLINE_FLAGS "ABC_READLINE_LIBRARIES=${ABC_READLINE_LIBRARIES_FLAGS}")
-elseif(READLINE_FOUND MATCHES FALSE)
-    list(APPEND ABC_READLINE_FLAGS "ABC_USE_NO_READLINE=1")
-endif()
+    set(ABC_MAIN_SRC "${CMAKE_CURRENT_SOURCE_DIR}/src/base/main/main.c")
+    list(REMOVE_ITEM ABC_SRC "${ABC_MAIN_SRC}")
 
-if(ABC_USE_NAMESPACE)
-    set(ABC_USE_NAMESPACE_FLAGS "ABC_USE_NAMESPACE=${ABC_USE_NAMESPACE}")
-endif()
+    add_library(libabc STATIC ${ABC_SRC})
+    add_executable(abc "${ABC_MAIN_SRC}")
+    target_link_libraries(abc PRIVATE libabc)
+
+    set(ABC_COMMON_DEFS
+        WIN32=1
+        NT=1
+        NT64=1
+        ABC_USE_CUDD=1
+        ABC_USE_STDINT_H=1
+        # Static build: make ABC_DLLEXPORT/IMPORT (and thus ABC_DLL) expand to nothing.
+        # Defining ABC_DLL=1 would substitute the literal "1" into every
+        # `extern ABC_DLL int Foo();` declaration in the headers.
+        WIN32_NO_DLL=1
+        # Keeps <windows.h> from pulling in <winsock.h>, which would re-define
+        # struct timeval without setting _TIMEVAL_DEFINED and break the
+        # in-tree timeval guards in util.h / UfarMgr.h.
+        WIN32_LEAN_AND_MEAN=1
+        # Tells the in-tree pthreads-win32 shim (lib/pthread.h) that struct
+        # timespec is already available (UCRT defines it in <time.h>).
+        HAVE_STRUCT_TIMESPEC=1
+        # Tells lib/pthread.h to declare pthread_* as plain extern (not
+        # dllimport), so our local stubs in UfarPthStub.c can satisfy them.
+        PTW32_STATIC_LIB=1
+        _CRT_SECURE_NO_WARNINGS=1
+        _CRT_NONSTDC_NO_DEPRECATE=1
+        # giaCTas2.c reuses fVal/fValOld as bitfield names; remap to avoid clash with local helpers
+        fVal=Value
+        fValOld=ValueOld
+    )
+
+    set(ABC_COMMON_OPTS /W1 /Zc:preprocessor /wd4005)
+
+    set(ABC_COMMON_INCS
+        "${CMAKE_CURRENT_SOURCE_DIR}/src"
+        "${CMAKE_CURRENT_SOURCE_DIR}/src/misc/util"
+        "${CMAKE_CURRENT_SOURCE_DIR}/src/aig"
+        "${CMAKE_CURRENT_SOURCE_DIR}/src/opt"
+    )
+
+    foreach(abc_tgt libabc abc)
+        target_compile_definitions(${abc_tgt} PRIVATE ${ABC_COMMON_DEFS})
+        target_compile_options(${abc_tgt} PRIVATE ${ABC_COMMON_OPTS})
+        # /TC + /std:c11 only apply to C TUs (a few module sources are .cpp)
+        target_compile_options(${abc_tgt} PRIVATE
+            $<$<COMPILE_LANGUAGE:C>:/TC>
+            $<$<COMPILE_LANGUAGE:C>:/std:c11>
+        )
+        target_include_directories(${abc_tgt} PRIVATE ${ABC_COMMON_INCS})
+    endforeach()
+
+else()
+
+    include(CMakeParseArguments)
+    include(CheckCCompilerFlag)
+    include(CheckCXXCompilerFlag)
+    # Generate compilation database compile_commands.json
+    set(CMAKE_EXPORT_COMPILE_COMMANDS ON)
+
+    # Default c++ standard used unless otherwise specified in target_compile_features.
+    set(CMAKE_CXX_STANDARD 17 CACHE STRING "the C++ standard to use for this project")
+    set(CMAKE_CXX_STANDARD_REQUIRED ON)
+
+    function(addprefix var prefix)
+        foreach( s ${ARGN} )
+            list(APPEND tmp "-I${s}")
+        endforeach()
+        set(${var} ${tmp} PARENT_SCOPE)
+    endfunction()
+
+    # filter out flags that are not appropriate for the compiler being used
+    function(target_compile_options_filtered target visibility)
+        foreach( flag ${ARGN} )
+            if( flag MATCHES "^-D.*" )
+                target_compile_options( ${target} ${visibility} ${flag} )
+            else()
+                check_c_compiler_flag( ${flag} C_COMPILER_SUPPORTS__${flag} )
+                if( C_COMPILER_SUPPORTS__${flag} )
+                    target_compile_options( ${target} ${visibility} $<$<COMPILE_LANGUAGE:C>:${flag}> )
+                endif()
+
+                check_cxx_compiler_flag( ${flag} CXX_COMPILER_SUPPORTS__${flag} )
+                if( CXX_COMPILER_SUPPORTS__${flag} )
+                    target_compile_options( ${target} ${visibility} $<$<COMPILE_LANGUAGE:CXX>:${flag}>  )
+                endif()
+            endif()
+        endforeach()
+    endfunction()
+
+    if(READLINE_FOUND MATCHES TRUE)
+        addprefix(ABC_READLINE_INCLUDES_FLAGS "-I" ${READLINE_INCLUDE})
+        string(REPLACE ";" " " ABC_READLINE_INCLUDES_FLAGS "${ABC_READLINE_INCLUDES_FLAGS}")
+        list(APPEND ABC_READLINE_FLAGS "ABC_READLINE_INCLUDES=${ABC_READLINE_INCLUDES_FLAGS}")
+
+        string(REPLACE ";" " " ABC_READLINE_LIBRARIES_FLAGS "${READLINE_LIBRARIES}")
+        list(APPEND ABC_READLINE_FLAGS "ABC_READLINE_LIBRARIES=${ABC_READLINE_LIBRARIES_FLAGS}")
+    elseif(READLINE_FOUND MATCHES FALSE)
+        list(APPEND ABC_READLINE_FLAGS "ABC_USE_NO_READLINE=1")
+    endif()
 
-if( APPLE )
-    set(make_env ${CMAKE_COMMAND} -E env SDKROOT=${CMAKE_OSX_SYSROOT})
+    if(ABC_USE_NAMESPACE)
+        set(ABC_USE_NAMESPACE_FLAGS "ABC_USE_NAMESPACE=${ABC_USE_NAMESPACE}")
+    endif()
+
+    if( APPLE )
+        set(make_env ${CMAKE_COMMAND} -E env SDKROOT=${CMAKE_OSX_SYSROOT})
+    endif()
+
+    # run make to extract compiler options, linker options and list of source files
+    execute_process(
+    COMMAND
+        ${make_env}
+        make
+            ${ABC_READLINE_FLAGS}
+            ${ABC_USE_NAMESPACE_FLAGS}
+            ARCHFLAGS_EXE=${CMAKE_CURRENT_BINARY_DIR}/abc_arch_flags_program.exe
+            ABC_MAKE_NO_DEPS=1
+            CC=${CMAKE_C_COMPILER}
+            CXX=${CMAKE_CXX_COMPILER}
+            LD=${CMAKE_CXX_COMPILER}
+            cmake_info
+    WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+    OUTPUT_VARIABLE MAKE_OUTPUT
+    )
+
+    # extract options from make output
+    function(extract_var SEPARATOR DEST_VARIABLE MAKE_OUTPUT)
+    string(REGEX MATCH "${SEPARATOR} .* ${SEPARATOR}" TMP "${MAKE_OUTPUT}")
+    string(REGEX REPLACE "${SEPARATOR} (.*) ${SEPARATOR}" "\\1" TMP "${TMP}")
+
+    separate_arguments(TMP)
+
+    set(${DEST_VARIABLE} ${TMP} PARENT_SCOPE)
+    endfunction()
+
+    extract_var(SEPARATOR_SRC ABC_SRC ${MAKE_OUTPUT})
+    extract_var(SEPARATOR_LIBS ABC_LIBS ${MAKE_OUTPUT})
+    extract_var(SEPARATOR_CFLAGS ABC_CFLAGS ${MAKE_OUTPUT})
+    extract_var(SEPARATOR_CXXFLAGS ABC_CXXFLAGS ${MAKE_OUTPUT})
+
+    if(ABC_USE_NAMESPACE)
+        set_source_files_properties(${ABC_SRC} PROPERTIES LANGUAGE CXX)
+    endif()
+
+    function(abc_properties target visibility)
+        target_include_directories(${target} ${visibility} $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/src>)
+        target_compile_options_filtered(${target} ${visibility} ${ABC_CFLAGS} ${ABC_CXXFLAGS} -Wno-unused-but-set-variable )
+        target_link_libraries(${target} ${visibility} ${ABC_LIBS})
+    endfunction()
+
+    set(ABC_MAIN_SRC src/base/main/main.c)
+    list(REMOVE_ITEM ABC_SRC ${ABC_MAIN_SRC})
+
+    add_library(libabc EXCLUDE_FROM_ALL ${ABC_SRC})
+    abc_properties(libabc PUBLIC)
+    set_property(TARGET libabc PROPERTY OUTPUT_NAME abc)
+
+    add_executable(abc ${ABC_MAIN_SRC})
+    target_link_libraries(abc PRIVATE libabc)
+    abc_properties(abc PRIVATE)
+
+    add_library(libabc-pic EXCLUDE_FROM_ALL ${ABC_SRC})
+    abc_properties(libabc-pic PUBLIC)
+    set_property(TARGET libabc-pic PROPERTY POSITION_INDEPENDENT_CODE ON)
+    set_property(TARGET libabc-pic PROPERTY OUTPUT_NAME abc-pic)
+
+    if(NOT DEFINED ABC_SKIP_TESTS)
+        enable_testing()
+        include(FetchContent)
+        FetchContent_Declare(
+        googletest
+        DOWNLOAD_EXTRACT_TIMESTAMP TRUE
+        # Specify the commit you depend on and update it regularly.
+        URL "https://github.com/google/googletest/archive/refs/tags/v1.14.0.zip"
+        )
+        FetchContent_MakeAvailable(googletest)
+        include(GoogleTest)
+        add_subdirectory(test)
+    endif()
 endif()
 
-# run make to extract compiler options, linker options and list of source files
-execute_process(
-  COMMAND
-    ${make_env}
-    make
-        ${ABC_READLINE_FLAGS}
-        ${ABC_USE_NAMESPACE_FLAGS}
-        ARCHFLAGS_EXE=${CMAKE_CURRENT_BINARY_DIR}/abc_arch_flags_program.exe
-        ABC_MAKE_NO_DEPS=1
-        CC=${CMAKE_C_COMPILER}
-        CXX=${CMAKE_CXX_COMPILER}
-        LD=${CMAKE_CXX_COMPILER}
-        cmake_info
-  WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
-  OUTPUT_VARIABLE MAKE_OUTPUT
+# ----------------------------------------------------------------------------
+# Installation rules
+# ----------------------------------------------------------------------------
+# Layout (with the default CMAKE_INSTALL_PREFIX on each platform):
+#   <prefix>/bin/abc[.exe]                               -- driver executable
+#   <prefix>/lib/libabc.a   or  <prefix>/lib/libabc.lib  -- static library
+#   <prefix>/include/abc/<...>                           -- full src/ header tree
+#   <prefix>/lib/cmake/abc/abcConfig.cmake               -- find_package(abc) entry
+#   <prefix>/lib/cmake/abc/abcConfigVersion.cmake
+#   <prefix>/lib/cmake/abc/abcTargets*.cmake
+#
+# Downstream usage:
+#   project(my_tool LANGUAGES C CXX)    # CXX required even for pure-C consumers:
+#                                       # libabc carries C++ TUs (cadical, eslim, ...)
+#                                       # so the link line needs the C++ runtime.
+#   find_package(abc CONFIG REQUIRED)
+#   target_link_libraries(my_tool PRIVATE abc::abc)
+#
+# ABC's headers cross-reference each other with paths like "misc/vec/vec.h",
+# so the public include root is exposed as <prefix>/include/abc; consumers
+# spell includes the same way the ABC sources do, e.g. <base/main/main.h>
+# (no leading abc/ prefix).
+
+include(CMakePackageConfigHelpers)
+
+add_library(abc::abc ALIAS libabc)
+set_target_properties(libabc PROPERTIES EXPORT_NAME abc)
+
+target_include_directories(libabc INTERFACE
+    $<BUILD_INTERFACE:${CMAKE_CURRENT_SOURCE_DIR}/src>
+    $<INSTALL_INTERFACE:${CMAKE_INSTALL_INCLUDEDIR}/abc>
 )
 
-# extract options from make output
-function(extract_var SEPARATOR DEST_VARIABLE MAKE_OUTPUT)
-  string(REGEX MATCH "${SEPARATOR} .* ${SEPARATOR}" TMP "${MAKE_OUTPUT}")
-  string(REGEX REPLACE "${SEPARATOR} (.*) ${SEPARATOR}" "\\1" TMP "${TMP}")
+target_compile_definitions(libabc INTERFACE WIN32_NO_DLL)
 
-  separate_arguments(TMP)
+install(TARGETS abc RUNTIME DESTINATION ${CMAKE_INSTALL_BINDIR})
 
-  set(${DEST_VARIABLE} ${TMP} PARENT_SCOPE)
-endfunction()
+install(TARGETS libabc
+    EXPORT abcTargets
+    ARCHIVE DESTINATION ${CMAKE_INSTALL_LIBDIR}
+    LIBRARY DESTINATION ${CMAKE_INSTALL_LIBDIR}
+)
 
-extract_var(SEPARATOR_SRC ABC_SRC ${MAKE_OUTPUT})
-extract_var(SEPARATOR_LIBS ABC_LIBS ${MAKE_OUTPUT})
-extract_var(SEPARATOR_CFLAGS ABC_CFLAGS ${MAKE_OUTPUT})
-extract_var(SEPARATOR_CXXFLAGS ABC_CXXFLAGS ${MAKE_OUTPUT})
+install(DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}/src/
+    DESTINATION ${CMAKE_INSTALL_INCLUDEDIR}/abc
+    FILES_MATCHING
+        PATTERN "*.h"
+        PATTERN "*.hpp"
+)
 
-if(ABC_USE_NAMESPACE)
-    set_source_files_properties(${ABC_SRC} PROPERTIES LANGUAGE CXX)
-endif()
+install(EXPORT abcTargets
+    FILE abcTargets.cmake
+    NAMESPACE abc::
+    DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/abc
+)
 
-function(abc_properties target visibility)
-    target_include_directories(${target} ${visibility} ${CMAKE_CURRENT_SOURCE_DIR}/src )
-    target_compile_options_filtered(${target} ${visibility} ${ABC_CFLAGS} ${ABC_CXXFLAGS} -Wno-unused-but-set-variable )
-    target_link_libraries(${target} ${visibility} ${ABC_LIBS})
-endfunction()
-
-set(ABC_MAIN_SRC src/base/main/main.c)
-list(REMOVE_ITEM ABC_SRC ${ABC_MAIN_SRC})
-
-add_library(libabc EXCLUDE_FROM_ALL ${ABC_SRC})
-abc_properties(libabc PUBLIC)
-set_property(TARGET libabc PROPERTY OUTPUT_NAME abc)
-
-add_executable(abc ${ABC_MAIN_SRC})
-target_link_libraries(abc PRIVATE libabc)
-abc_properties(abc PRIVATE)
-
-add_library(libabc-pic EXCLUDE_FROM_ALL ${ABC_SRC})
-abc_properties(libabc-pic PUBLIC)
-set_property(TARGET libabc-pic PROPERTY POSITION_INDEPENDENT_CODE ON)
-set_property(TARGET libabc-pic PROPERTY OUTPUT_NAME abc-pic)
-
-if(NOT DEFINED ABC_SKIP_TESTS)
-    enable_testing()
-    include(FetchContent)
-    FetchContent_Declare(
-    googletest
-    DOWNLOAD_EXTRACT_TIMESTAMP TRUE
-    # Specify the commit you depend on and update it regularly.
-    URL "https://github.com/google/googletest/archive/refs/tags/v1.14.0.zip"
-    )
-    FetchContent_MakeAvailable(googletest)
-    include(GoogleTest)
-    add_subdirectory(test)
-endif()
\ No newline at end of file
+configure_package_config_file(
+    "${CMAKE_CURRENT_SOURCE_DIR}/cmake/abcConfig.cmake.in"
+    "${CMAKE_CURRENT_BINARY_DIR}/abcConfig.cmake"
+    INSTALL_DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/abc
+)
+
+write_basic_package_version_file(
+    "${CMAKE_CURRENT_BINARY_DIR}/abcConfigVersion.cmake"
+    VERSION ${PROJECT_VERSION}
+    COMPATIBILITY SameMajorVersion
+)
+
+install(FILES
+    "${CMAKE_CURRENT_BINARY_DIR}/abcConfig.cmake"
+    "${CMAKE_CURRENT_BINARY_DIR}/abcConfigVersion.cmake"
+    DESTINATION ${CMAKE_INSTALL_LIBDIR}/cmake/abc
+)
diff --git a/cmake/abcConfig.cmake.in b/cmake/abcConfig.cmake.in
new file mode 100644
index 0000000000..43dde4fc4e
--- /dev/null
+++ b/cmake/abcConfig.cmake.in
@@ -0,0 +1,7 @@
+@PACKAGE_INIT@
+
+include(CMakeFindDependencyMacro)
+
+include("${CMAKE_CURRENT_LIST_DIR}/abcTargets.cmake")
+
+check_required_components(abc)
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index c5a0327e04..c72f61c4cc 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -83,8 +83,11 @@
 #include <string.h>
 
 // catch memory leaks in Visual Studio
+// Note: _CRTDBG_MAP_ALLOC remaps malloc/free/etc. as macros, which collides with
+// C++ class members named the same (e.g. cadical's DeferDeleteArray::free), so
+// only enable it in C TUs.
 #ifdef WIN32
-  #ifdef _DEBUG
+  #if defined(_DEBUG) && !defined(__cplusplus)
     #define _CRTDBG_MAP_ALLOC
     #include <crtdbg.h>
   #endif
diff --git a/src/opt/eslim/utils.hpp b/src/opt/eslim/utils.hpp
index b4beb33f07..24fd83c5ce 100644
--- a/src/opt/eslim/utils.hpp
+++ b/src/opt/eslim/utils.hpp
@@ -74,9 +74,9 @@ namespace eSLIM {
       if (tt == 0) {
         return -1;
       }
-      int x = 0;
-      bool status = _BitScanForward64(x, tt);
-      return x;
+      unsigned long x = 0;
+      _BitScanForward64(&x, tt);
+      return (int)x;
     #else
       if (tt == 0) {
         return -1;
diff --git a/src/opt/eslim/windowMan.tpp b/src/opt/eslim/windowMan.tpp
index d09b264abe..c540988a38 100644
--- a/src/opt/eslim/windowMan.tpp
+++ b/src/opt/eslim/windowMan.tpp
@@ -126,7 +126,7 @@ namespace eSLIM {
       std::cout << "PThreads not available, minimize random window.\n";
       std::uniform_int_distribution<> udist(0, windows.size() - 1);
       int wid = udist(rng);
-      eSLIM_Man<SynthesisEngine, SelectionStrategy>::applyeSLIM(windows[wid], cfg, wlogs[wid])
+      eSLIM_Man<SynthesisEngine, SelectionStrategy>::applyeSLIM(windows[wid], cfg, wlogs[wid]);
     #endif
   }
 
diff --git a/src/opt/ufar/UfarPthStub.c b/src/opt/ufar/UfarPthStub.c
new file mode 100644
index 0000000000..702c3c17f0
--- /dev/null
+++ b/src/opt/ufar/UfarPthStub.c
@@ -0,0 +1,33 @@
+// No-op stubs for the subset of pthread functions referenced by UfarPth.cpp.
+// Linked into libabc only when no real pthread implementation is available
+// (currently: MSVC builds, where ABC_USE_PTHREADS is not set).
+// RunConcurrentSolver simply won't do real parallel work in this build.
+
+#include "../../../lib/pthread.h"
+
+int pthread_create(pthread_t * thread, const pthread_attr_t * attr,
+                   void * (*start_routine)(void *), void * arg)
+{
+    (void)thread; (void)attr; (void)start_routine; (void)arg;
+    return -1;
+}
+
+void pthread_exit(void * retval) { (void)retval; }
+
+int pthread_join(pthread_t thread, void ** retval)
+{
+    (void)thread; (void)retval;
+    return 0;
+}
+
+int pthread_mutex_lock(pthread_mutex_t * mutex) { (void)mutex; return 0; }
+int pthread_mutex_unlock(pthread_mutex_t * mutex) { (void)mutex; return 0; }
+
+int pthread_cond_timedwait(pthread_cond_t * cond, pthread_mutex_t * mutex,
+                           const struct timespec * abstime)
+{
+    (void)cond; (void)mutex; (void)abstime;
+    return 0;
+}
+
+int pthread_cond_signal(pthread_cond_t * cond) { (void)cond; return 0; }
diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c
index f9a6de09bd..94eafa479e 100644
--- a/src/proof/cec/cecProve.c
+++ b/src/proof/cec/cecProve.c
@@ -61,8 +61,10 @@ struct Cec_SproveTrace_t_;
 static int Cec_SProveCallback( void * pUser, int fSolved, unsigned Result );
 static Gia_Man_t * Cec_GiaScorrOld( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
 static Gia_Man_t * Cec_GiaScorrNew( Gia_Man_t * p, int nTimeOut, Par_Share_t * pShare, struct Cec_ScorrStop_t_ * pStopOut );
+#ifdef ABC_USE_PTHREADS
 static void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int nTimeOut, int nTimeOutU, Wlc_Ntk_t * pWlc, const char * pUfarArgs, int fVerbose, pthread_t * WorkerThread, Par_Share_t * pShare, int * pEngines, int StageId, int NetId, struct Cec_SproveTrace_t_ * pTrace );
 static void Cec_GiaStopThreads( Par_ThData_t * ThData, pthread_t * WorkerThread, int nWorkers );
+#endif
 static int Cec_GiaWaitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int RetValue, int * pRetEngine );
 
 extern int Ufar_ProveWithTimeout( Wlc_Ntk_t * pNtk, int nTimeOut, int fVerbose, int (*pFuncStop)(int), int RunId, const char * pArgs );