diff options
| author | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-01-14 12:21:48 +0000 |
|---|---|---|
| committer | Dan Liew <daniel.liew@imperial.ac.uk> | 2016-01-14 12:30:31 +0000 |
| commit | cece05cadf6a624afd188e81720ae7701736a703 (patch) | |
| tree | dab3e0f57477f584dfa65f0c166bceb118c4551c /MetaSMT.mk | |
| parent | 68fa7490713ecf6672684c4398f9c19a101f822a (diff) | |
| download | klee-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 'MetaSMT.mk')
| -rw-r--r-- | MetaSMT.mk | 17 |
1 files changed, 17 insertions, 0 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 |