From: Hamed Gorjiara Date: Tue, 19 Nov 2019 17:05:01 +0000 (-0800) Subject: Timeout for running benchmarks X-Git-Url: http://plrg.eecs.uci.edu/git/?p=satune.git;a=commitdiff_plain;h=03cc8e971bf25ef6966ade49b9ada99d200739e7 Timeout for running benchmarks --- diff --git a/src/Scripts/runbench.sh b/src/Scripts/runbench.sh index db570df..0d536c7 100755 --- a/src/Scripts/runbench.sh +++ b/src/Scripts/runbench.sh @@ -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 ....