about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
-rw-r--r--MetaSMT.mk17
-rw-r--r--tools/kleaver/Makefile12
-rw-r--r--tools/klee/Makefile12
-rw-r--r--unittests/Solver/Makefile2
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