From cece05cadf6a624afd188e81720ae7701736a703 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 14 Jan 2016 12:21:48 +0000 Subject: 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... :( --- tools/kleaver/Makefile | 12 +----------- 1 file changed, 1 insertion(+), 11 deletions(-) (limited to 'tools/kleaver') 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 -- cgit 1.4.1