Bug fix for return value in runbench script

diff --git a/src/Scripts/runbench.sh b/src/Scripts/runbench.sh
index 44e52bfc6c077db49636863f9e5a84e1589e870e..3e498d2645a0c3b4cb60473356f0fdc65e72f688 100755 (executable)
--- a/src/Scripts/runbench.sh
+++ b/src/Scripts/runbench.sh
@@ -19,8 +19,9 @@ for d in $DUMP; do
        if [[ $d = *$1* ]]; then
                echo "Running: ./run.sh tunerrun "."$d $2 $3 out.out"
                ./run.sh tunerrun "."$d $2 $3 out.out
        if [[ $d = *$1* ]]; then
                echo "Running: ./run.sh tunerrun "."$d $2 $3 out.out"
                ./run.sh tunerrun "."$d $2 $3 out.out

-               echo "Return code: $?"
-               if [ $? -eq 141 ]; then #Dump info when SAT Solver gets killed by OS ....
+               RETCODE=$?
+               echo "Return code: $RETCODE"
+               if [ $RETCODE -eq 141 ]; then #Dump info when SAT Solver gets killed by OS ....

                        echo "Satune got out of memory"
                        echo "deserializing $d ..."
                        echo "SAT Solving time: 400000000.0"
                        echo "Satune got out of memory"
                        echo "deserializing $d ..."
                        echo "SAT Solving time: 400000000.0"