about summary refs log tree commit diff homepage
diff options
context:
space:
mode:
authorHoang M. Le <hle@informatik.uni-bremen.de>2016-06-08 18:14:45 +0200
committerHoang M. Le <hle@informatik.uni-bremen.de>2016-06-10 11:32:34 +0200
commite70147e2c7f6716c4c0313d8e5b4aeba1d3042ed (patch)
tree99d454057324fe824f25f6aa62c0abcc2a5cbd70
parenta0ce2ae13ff2b96befe633742ce5ce0c014666ed (diff)
downloadklee-e70147e2c7f6716c4c0313d8e5b4aeba1d3042ed.tar.gz
add entries for metaSMT with btor/stp/z3 in Travis CI
-rw-r--r--.travis.yml9
-rwxr-xr-x.travis/klee.sh2
2 files changed, 8 insertions, 3 deletions
diff --git a/.travis.yml b/.travis.yml
index 45e93d22..8fc99b98 100644
--- a/.travis.yml
+++ b/.travis.yml
@@ -21,6 +21,7 @@ env:
     #   LLVM  : {2.9, 3.4}
     #   SOLVERS : {Z3, STP, STP:Z3, metaSMT}
     #   STP_VERSION   : {2.1.0, master}
+    #   METASMT_DEFAULT : {btor, stp, z3}
     #   UCLIBC: {0, klee_uclibc_v1.0.0, klee_0_9_29} // Note ``0`` means disabled
     # with Asserts enabled.
 
@@ -28,8 +29,12 @@ env:
 
     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
+    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=btor KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=stp  KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=stp  KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=3.4 SOLVERS=metaSMT METASMT_DEFAULT=z3   KLEE_UCLIBC=klee_uclibc_v1.0.0 DISABLE_ASSERTIONS=0 ENABLE_OPTIMIZED=1 COVERAGE=0
+    - LLVM_VERSION=2.9 SOLVERS=metaSMT METASMT_DEFAULT=z3   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
diff --git a/.travis/klee.sh b/.travis/klee.sh
index 64087b11..bb57f281 100755
--- a/.travis/klee.sh
+++ b/.travis/klee.sh
@@ -66,7 +66,7 @@ for solver in ${SOLVER_LIST}; do
     ;;
   metaSMT)
     echo "metaSMT"
-    KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root"
+    KLEE_METASMT_CONFIGURE_OPTION="--with-metasmt=${BUILD_DIR}/metaSMT/build/root --with-metasmt-default-solver=${METASMT_DEFAULT}"
     ;;
   *)
     echo "Unknown solver ${solver}"