diff options
Diffstat (limited to 'cmake')
| -rw-r--r-- | cmake/find_metasmt.cmake | 13 |
1 files changed, 11 insertions, 2 deletions
diff --git a/cmake/find_metasmt.cmake b/cmake/find_metasmt.cmake index 39079e2b..3dc9fe50 100644 --- a/cmake/find_metasmt.cmake +++ b/cmake/find_metasmt.cmake @@ -62,7 +62,13 @@ if (ENABLE_SOLVER_METASMT) klee_component_add_cxx_flag(${f} REQUIRED) endforeach() - set(available_metasmt_backends "BTOR" "STP" "Z3") + # Check if metaSMT provides an useable backend + if (NOT metaSMT_AVAILABLE_QF_ABV_SOLVERS) + message(FATAL_ERROR "metaSMT does not provide an useable backend.") + endif() + + message(STATUS "metaSMT has the following backend(s): ${metaSMT_AVAILABLE_QF_ABV_SOLVERS}.") + set(available_metasmt_backends ${metaSMT_AVAILABLE_QF_ABV_SOLVERS}) set(METASMT_DEFAULT_BACKEND "STP" CACHE STRING @@ -79,9 +85,12 @@ if (ENABLE_SOLVER_METASMT) "Valid values are ${available_metasmt_backends}") endif() - # Set appropriate define + # Set appropriate defines list(APPEND KLEE_COMPONENT_CXX_DEFINES -DMETASMT_DEFAULT_BACKEND_IS_${METASMT_DEFAULT_BACKEND}) + foreach(backend ${available_metasmt_backends}) + list(APPEND KLEE_COMPONENT_CXX_DEFINES -DMETASMT_HAVE_${backend}) + endforeach() else() message(STATUS "metaSMT solver support disabled") set(ENABLE_METASMT 0) # For config.h |