add metaSMT to travis

5 files changed, 37 insertions, 1 deletions

diff --git a/.travis.yml b/.travis.yml
index 158f8f76..45e93d22 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -19,7 +19,7 @@ env:
 
     # Check the matrix of:
     #   LLVM  : {2.9, 3.4}
-    #   SOLVERS : {Z3, STP, STP:Z3}
+    #   SOLVERS : {Z3, STP, STP:Z3, metaSMT}
     #   STP_VERSION   : {2.1.0, master}
     #   UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled
     # with Asserts enabled.
@@ -27,6 +27,9 @@ env:
     # COVERAGE set indicated that coverage data should be uplaoded to the server, only ONE job should have COVERAGE set
 
     matrix:
+    # Test experimental metaSMT support
+    - LLVM_VERSION=3.4 SOLVERS=metaSMT KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=2.9 SOLVERS=metaSMT KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
     # Test experimental Z3 support
     - LLVM_VERSION=3.4 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
     - LLVM_VERSION=2.9 SOLVERS=Z3 KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
@@ -65,6 +68,8 @@ before_install:
     # Set up the locations to get various packages from
     # We assume the Travis image uses Ubuntu 12.04 LTS
     ###########################################################################
+    # Needed for Boost
+    - sudo add-apt-repository -y ppa:boost-latest
     # Needed for CMake
     - sudo add-apt-repository -y ppa:kalakris/cmake
     # Needed for LLVM
diff --git a/.travis/klee.sh b/.travis/klee.sh
index 296e1c83..64087b11 100755
--- a/.travis/klee.sh
+++ b/.travis/klee.sh
@@ -51,6 +51,7 @@ fi
 ###############################################################################
 KLEE_Z3_CONFIGURE_OPTION=""
 KLEE_STP_CONFIGURE_OPTION=""
+KLEE_METASMT_CONFIGURE_OPTION=""
 SOLVER_LIST=$(echo "${SOLVERS}" | sed 's/:/ /')
 
 for solver in ${SOLVER_LIST}; do
@@ -63,6 +64,10 @@ for solver in ${SOLVER_LIST}; do
     echo "Z3"
     KLEE_Z3_CONFIGURE_OPTION="--with-z3=/usr"
     ;;
+  metaSMT)
+    echo "metaSMT"
+    KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root"
+    ;;
   *)
     echo "Unknown solver ${solver}"
     exit 1
@@ -87,6 +92,7 @@ ${KLEE_SRC}/configure --with-llvmsrc=/usr/lib/llvm-${LLVM_VERSION}/build \
             --with-llvmcxx=${KLEE_CXX} \
             ${KLEE_STP_CONFIGURE_OPTION} \
             ${KLEE_Z3_CONFIGURE_OPTION} \
+            ${KLEE_METASMT_CONFIGURE_OPTION} \
             ${KLEE_UCLIBC_CONFIGURE_OPTION} \
             ${TCMALLOC_OPTION} \
             CXXFLAGS="${COVERAGE_FLAGS}" \
diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh
new file mode 100755
index 00000000..7a0d1eef
--- /dev/null
+++ b/.travis/metaSMT.sh
@@ -0,0 +1,20 @@
+#!/bin/bash -x
+
+# Get Boost, Z3, libgmp
+sudo apt-get -y install libboost1.55-dev libz3 libz3-dev libgmp-dev
+
+# Clone
+git clone git://github.com/hoangmle/metaSMT.git
+cd metaSMT
+git clone git://github.com/agra-uni-bremen/dependencies.git
+
+# Bootstrap
+export BOOST_ROOT=/usr
+sudo cp dependencies/Z3-2.19/Z3Config.cmake /usr # this is a hack
+./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off --build stp-git-basic --build boolector-1.5.118 --build minisat-git -DZ3_DIR=/usr
+sudo cp deps/boolector-1.5.118/lib/* /usr/lib/ #
+sudo cp deps/minisat-git/lib/* /usr/lib/       # hack
+sudo cp deps/stp-git-basic/lib/* /usr/lib/     #
+
+# Build
+make -C build install
diff --git a/.travis/solvers.sh b/.travis/solvers.sh
index db717f2d..d64c1077 100755
--- a/.travis/solvers.sh
+++ b/.travis/solvers.sh
@@ -20,6 +20,10 @@ for solver in ${SOLVER_LIST}; do
     # Should we install libz3-dbg too?
     sudo apt-get -y install libz3 libz3-dev
     ;;
+  metaSMT)
+    echo "metaSMT"
+    ${KLEE_SRC}/.travis/metaSMT.sh
+    ;;
   *)
     echo "Unknown solver ${solver}"
     exit 1
diff --git a/MetaSMT.mk b/MetaSMT.mk
index 80f28a9b..dd34e5fd 100644
--- a/MetaSMT.mk
+++ b/MetaSMT.mk
@@ -7,5 +7,6 @@ ifeq ($(ENABLE_METASMT),1)
   CXX.Flags += $(metaSMT_CXXFLAGS)
   CXX.Flags += $(metaSMT_INCLUDES)
   CXX.Flags := $(filter-out -fno-exceptions,$(CXX.Flags))
+  CXX.Flags := $(filter-out -fno-rtti,$(CXX.Flags))
   LIBS += $(metaSMT_LDLIBS)
 endif