Separated regression tests of unsat cores

.gitignore

@@ -22,7 +22,7 @@ m4/ltversion.m4
 m4/lt~obsolete.m4
 opensmt
 src/bin/.dirstamp
-test/regression/base/log-*
+test/regression/*/log-*
 src/PySMT/opensmt.py
 .ycm_extra_conf.py
 .ycm_extra_conf.pyc

ci/run_travis_commands.sh

@@ -23,6 +23,7 @@ make test
 make install
 if [[ ${CMAKE_BUILD_TYPE} == Debug ]]; then
     cd ../test/regression/base && ./run-test-notiming.sh ../../../build/opensmt
+    cd ../unsatcores && ./run-test-notiming.sh ../../../build/opensmt
     cd ../interpolation && ./run-tests.sh ../../../build/opensmt
     if [[ "${PARALLEL}" == "ON" ]]; then
       cd ../splitting && ./bin/run-tests.sh ../../../build/opensmt-splitter

test/regression/unsatcores/run-test-notiming.sh

@@ -0,0 +1,72 @@
+#!/bin/bash
+get_abs_filename() {
+  echo "$(cd "$(dirname "$1")" && pwd)/$(basename "$1")"
+}
+
+usage="Usage: $0 [-h] <path-to-opensmt>"
+
+while [ $# -gt 0 ]; do
+    case $1 in
+        -h|--help)
+            echo "${usage}"
+            exit 1
+            ;;
+        -*)
+            echo "Error: invalid option '$1'"
+            exit 1
+            ;;
+        *)
+            break
+    esac
+    shift; shift
+done
+
+opensmt=$1
+
+if [ -z ${opensmt} ]; then
+    echo "Opensmt binary not specified"
+    exit 1
+fi
+
+echo "This is the script for running regression tests for unsatisfiable cores"
+echo " - date: $(date '+%Y-%m-%d at %H:%M.%S')"
+echo " - host name $(hostname -f)"
+echo " - script path: $(get_abs_filename $0)"
+
+tmpfolder=log-$(date '+%Y-%m-%d-%H-%M-%S')
+mkdir ${tmpfolder}
+
+export outmod=false
+export errmod=false
+export rtmod=false
+tolerance=1.5
+
+for file in $(find . -name '*.smt2' |sort); do
+    name=$(basename $file)
+    dir=$(dirname $file)
+
+    sh -c "ulimit -St 60; ${opensmt} $(echo ${options}) $dir/$name > $tmpfolder/$name.out 2>$tmpfolder/$name.err.tmp" 2>/dev/null
+
+    grep -v '^;' $tmpfolder/$name.err.tmp > $tmpfolder/$name.err
+    diff -q ${tmpfolder}/${name}.out ${dir}/${name}.expected.out
+    if [ $? != 0 ]; then
+        echo "stdout differs for benchmark $file";
+        outmod=true;
+        diff ${tmpfolder}/${name}.out ${dir}/${name}.expected.out
+    fi
+    diff -q ${tmpfolder}/${name}.err ${dir}/${name}.expected.err
+    if [ $? != 0 ]; then
+        echo "stderr differs for benchmark $file";
+        errmod=true;
+        diff ${tmpfolder}/${name}.err ${dir}/${name}.expected.err
+    fi
+
+done
+echo "Stdout differs: ${outmod}, stderr differs: ${errmod}"
+
+if [[ ${outmod} == true || ${errmod} == true ]]; then
+    echo "There were anomalies: check logs in ${tmpfolder}"
+    exit 1
+else
+    rm -rf ${tmpfolder}
+fi