Timeout for running benchmarks
authorHamed Gorjiara <hgorjiar@uci.edu>
Tue, 19 Nov 2019 17:05:01 +0000 (09:05 -0800)
committerHamed Gorjiara <hgorjiar@uci.edu>
Tue, 19 Nov 2019 17:05:01 +0000 (09:05 -0800)
src/Scripts/runbench.sh

index db570dfd039b99f92047766ad23ca19b052e19ea..0d536c7f9ef58e6203c2d1e7ffbe82c43c6e155f 100755 (executable)
@@ -18,7 +18,7 @@ cd $BIN
 for d in $DUMP; do
        if [[ $d = *$1* ]] && [[ $d = *learningset* ]]; then
                echo "Running: ./run.sh tunerrun "."$d $2 $3 out.out"
-               ./run.sh tunerrun "."$d $2 $3 out.out
+               ./run.sh timeout $2 tunerrun "."$d $2 $3 out.out
                RETCODE=$?
                echo "Return code: $RETCODE"
                if [ $RETCODE -eq 141 ]; then #Dump info when SAT Solver gets killed by OS ....