diff options
-rw-r--r-- | MetaSMT.mk | 17 | ||||
-rw-r--r-- | tools/kleaver/Makefile | 12 | ||||
-rw-r--r-- | tools/klee/Makefile | 12 | ||||
-rw-r--r-- | unittests/Solver/Makefile | 2 |
4 files changed, 21 insertions, 22 deletions
diff --git a/MetaSMT.mk b/MetaSMT.mk new file mode 100644 index 00000000..94dd398a --- /dev/null +++ b/MetaSMT.mk @@ -0,0 +1,17 @@ +# This file contains common code for linking against MetaSMT +# +# FIXME: This is a horribly fragile hack. +# Instead the detection of what solvers the build of MetaSMT supports should be +# done by the configure script and then the appropriate compiler flags should +# be emitted to Makefile.config for consumption here. +ifeq ($(ENABLE_METASMT),1) + include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile + LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \ + -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \ + -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \ + -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib \ + -L$(METASMT_ROOT)/../../deps/stp-svn/lib + CXX.Flags += -DBOOST_HAS_GCC_TR1 + CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) + LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lstp -lrt -lboolector -lminisat_core +endif diff --git a/tools/kleaver/Makefile b/tools/kleaver/Makefile index 287aeb38..ece2b799 100644 --- a/tools/kleaver/Makefile +++ b/tools/kleaver/Makefile @@ -23,14 +23,4 @@ ifneq ($(ENABLE_STP),0) LIBS += $(STP_LDFLAGS) endif -ifeq ($(ENABLE_METASMT),1) - include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile - LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \ - -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \ - -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \ - -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib \ - -L$(METASMT_ROOT)/../../deps/stp-svn/lib - CXX.Flags += -DBOOST_HAS_GCC_TR1 - CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) - LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lstp -lrt -lboolector -lminisat_core -endif +include $(PROJ_SRC_ROOT)/MetaSMT.mk diff --git a/tools/klee/Makefile b/tools/klee/Makefile index f8824fe7..d807350d 100644 --- a/tools/klee/Makefile +++ b/tools/klee/Makefile @@ -24,14 +24,4 @@ ifneq ($(ENABLE_STP),0) LIBS += $(STP_LDFLAGS) endif -ifeq ($(ENABLE_METASMT),1) - include $(METASMT_ROOT)/share/metaSMT/metaSMT.makefile - LD.Flags += -L$(METASMT_ROOT)/../../deps/Z3-4.1/lib \ - -L$(METASMT_ROOT)/../../deps/boolector-1.5.118/lib \ - -L$(METASMT_ROOT)/../../deps/minisat-git/lib/ \ - -L$(METASMT_ROOT)/../../deps/boost-1_52_0/lib \ - -L$(METASMT_ROOT)/../../deps/stp-svn/lib - CXX.Flags += -DBOOST_HAS_GCC_TR1 - CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags)) - LIBS += -lgomp -lboost_iostreams -lboost_thread -lboost_system -lmetaSMT -lz3 -lstp -lrt -lboolector -lminisat_core -endif +include $(PROJ_SRC_ROOT)/MetaSMT.mk diff --git a/unittests/Solver/Makefile b/unittests/Solver/Makefile index 65edbe7a..1d3d609e 100644 --- a/unittests/Solver/Makefile +++ b/unittests/Solver/Makefile @@ -12,3 +12,5 @@ include $(LLVM_SRC_ROOT)/unittests/Makefile.unittest ifneq ($(ENABLE_STP),0) LIBS += $(STP_LDFLAGS) endif + +include $(PROJ_SRC_ROOT)/MetaSMT.mk |