From c9e0af1f12d606120b5f6d60a54f1b79cfc01f7c Mon Sep 17 00:00:00 2001
From: "Hoang M. Le" <hle@informatik.uni-bremen.de>
Date: Thu, 5 Oct 2017 11:37:56 +0200
Subject: [travis] update scripts to additionally test CVC4 and Yices2

---
 .travis/klee.sh    |  2 +-
 .travis/metaSMT.sh | 12 +++++++++---
 2 files changed, 10 insertions(+), 4 deletions(-)

(limited to '.travis')

diff --git a/.travis/klee.sh b/.travis/klee.sh
index 33299780..2de6b57c 100755
--- a/.travis/klee.sh
+++ b/.travis/klee.sh
@@ -147,7 +147,7 @@ make systemtests
 # If metaSMT is the only solver, then rerun lit tests with non-default metaSMT backends
 if [ "X${SOLVERS}" == "XmetaSMT" ]; then
   metasmt_default=`echo "${METASMT_DEFAULT,,}"` # klee_opts and kleaver_opts use lowercase
-  available_metasmt_backends="btor stp z3"
+  available_metasmt_backends="btor stp z3 yices2 cvc4"
   for backend in $available_metasmt_backends; do
     if [ "X${metasmt_default}" != "X$backend" ]; then
       lit -v --param klee_opts=-metasmt-backend=$backend --param kleaver_opts=-metasmt-backend=$backend test/
diff --git a/.travis/metaSMT.sh b/.travis/metaSMT.sh
index f0748919..dbdd2643 100755
--- a/.travis/metaSMT.sh
+++ b/.travis/metaSMT.sh
@@ -4,8 +4,8 @@ set -e
 
 : ${METASMT_VERSION?"METASMT_VERSION not specified"}
 
-# Get Z3, libgmp
-sudo apt-get -y install libz3 libz3-dev libgmp-dev
+# Get Z3, libgmp, gperf (required by yices2)
+sudo apt-get -y install libz3 libz3-dev libgmp-dev gperf
 
 # Get Boost
 if [ "X${METASMT_BOOST_VERSION}" != "X" ]; then
@@ -19,6 +19,11 @@ else
   sudo apt-get -y install libboost1.55-dev
 fi
 
+# Get CVC4
+wget http://www.informatik.uni-bremen.de/agra/systemc-verification/media/snapshots/cvc4-594301e.tar.gz
+tar -xf cvc4-594301e.tar.gz
+sudo mv cvc4 /usr
+
 # Clone
 git clone -b ${METASMT_VERSION} --single-branch --depth 1 https://github.com/hoangmle/metaSMT.git
 cd metaSMT
@@ -33,11 +38,12 @@ fi
 # 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 -DmetaSMT_REQUIRE_CXX11=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 -DZ3_DIR=/usr
+./bootstrap.sh -d deps -m RELEASE build -DmetaSMT_ENABLE_TESTS=off -DmetaSMT_REQUIRE_CXX11=off --build stp-git-basic --build boolector-2.2.0 --build minisat-git --build lingeling-ayv-86bf266-140429 --build yices-2.5.1 -DZ3_DIR=/usr -DCVC4_DIR=/usr/cvc4
 sudo cp deps/boolector-2.2.0/lib/* /usr/lib/              #
 sudo cp deps/lingeling-ayv-86bf266-140429/lib/* /usr/lib/ #
 sudo cp deps/minisat-git/lib/* /usr/lib/                  # hack
 sudo cp -r deps/stp-git-basic/lib/lib* /usr/lib/          #
+sudo cp deps/yices-2.5.1/lib/* /usr/lib/                  #
 
 # Build
 make -C build install
-- 
cgit 1.4.1