about summary refs log tree commit diff homepage
path: root/tools
diff options
context:
space:
mode:
authorDan Liew <daniel.liew@imperial.ac.uk>2016-01-14 12:21:48 +0000
committerDan Liew <daniel.liew@imperial.ac.uk>2016-01-14 12:30:31 +0000
commitcece05cadf6a624afd188e81720ae7701736a703 (patch)
treedab3e0f57477f584dfa65f0c166bceb118c4551c /tools
parent68fa7490713ecf6672684c4398f9c19a101f822a (diff)
downloadklee-cece05cadf6a624afd188e81720ae7701736a703.tar.gz
Refactor the MetaSMT makefile commands into its own file which can
be included by tools that needs to link against MetaSMT. Apart from
making the Makefile code cleaner this allowed the Solver unit test
linking to succeed when not building with STP support.

Unfortunately when using MetaSMT as the core solver the Solver unit
tests do not pass. Clearly no one tried this before... :(
Diffstat (limited to 'tools')
-rw-r--r--tools/kleaver/Makefile12
-rw-r--r--tools/klee/Makefile12
2 files changed, 2 insertions, 22 deletions
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