diff --git a/src/libcprover-cpp/CMakeLists.txt b/src/libcprover-cpp/CMakeLists.txt index 278e77f642d..adf1a331f6e 100644 --- a/src/libcprover-cpp/CMakeLists.txt +++ b/src/libcprover-cpp/CMakeLists.txt @@ -61,7 +61,16 @@ target_link_libraries(cprover-api-cpp # Here we prepare a space-separated list of cmake generators that will resolved in absolute paths. set(DEPENDENCY_TARGETS "") foreach(dep ${LIBRARY_DEPENDENCIES}) - list(APPEND DEPENDENCY_TARGETS "$") + if(TARGET ${dep}) + list(APPEND DEPENDENCY_TARGETS "$") + else() + find_library(dep_path ${dep}) + string(REGEX REPLACE "[.]so$" ".a" dep_static_path ${dep_path}) + if (NOT EXISTS "${dep_static_path}") + message(FATAL_ERROR "libcprover-cpp cannot be linked as dependency ${dep_path} does not have a static correspondent file (${dep_static_path})") + endif() + list(APPEND DEPENDENCY_TARGETS ${dep_static_path}) + endif() endforeach(dep LIBRARY_DEPENDENCIES) string(REPLACE ";" " " DEPENDENCY_TARGETS "${DEPENDENCY_TARGETS}") diff --git a/src/solvers/CMakeLists.txt b/src/solvers/CMakeLists.txt index e941c134d69..874f47e6ad5 100644 --- a/src/solvers/CMakeLists.txt +++ b/src/solvers/CMakeLists.txt @@ -87,6 +87,20 @@ foreach(SOLVER ${sat_impl}) target_sources(solvers PRIVATE ${minisat2_source}) target_link_libraries(solvers minisat2-condensed) + elseif("${SOLVER}" STREQUAL "system-minisat2") + include(CheckIncludeFileCXX) + # if/when we move to CMake 3.12 (or later) we could also check for the + # library via CMAKE_REQUIRED_LIBRARIES + find_path(minisat_header_found "minisat/simp/SimpSolver.h") + if(minisat_header_found) + message(STATUS "Building solvers with minisat2 (${minisat_header_found})") + target_compile_definitions(solvers PUBLIC SATCHECK_MINISAT2 HAVE_MINISAT2) + target_sources(solvers PRIVATE ${minisat2_source}) + target_include_directories(solvers PRIVATE ${minisat_header_found}) + target_link_libraries(solvers minisat) + else() + message(FATAL_ERROR "Unable to find header file for preinstalled minisat2") + endif() elseif("${SOLVER}" STREQUAL "glucose") message(STATUS "Building solvers with glucose")