diff --git a/Makefile.build b/Makefile.build
index f1b700e9c..99a8fe43c 100644
--- a/Makefile.build
+++ b/Makefile.build
@@ -309,14 +309,14 @@ regress: build_subdirs version
 	@ echo "=== Building binaries ==="
 	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) bin
 	@ echo "=== Running regressions ==="
-	@ $(regressdir)/check.sh $(regressdir) $(build_dir)/bin
+	+@ $(regressdir)/check.sh $(regressdir) $(build_dir)/bin
 
 
 static-regress: static_build_subdirs version
 	@ echo "=== Building binaries ==="
 	@ $(MAKE) -C $(srcdir) BUILD=../$(build_dir) static-bin
 	@ echo "=== Running regressions ==="
-	@ $(regressdir)/check.sh $(regressdir) $(build_dir)/static_bin
+	@ $(regressdir)/check.sh -j $(regressdir) $(build_dir)/static_bin
 
 
 .PHONY: all obj static-obj lib static-lib bin static-bin test static-test \
diff --git a/configure.ac b/configure.ac
index 15b4a97b6..b9448ef30 100644
--- a/configure.ac
+++ b/configure.ac
@@ -578,7 +578,7 @@ if test -z "$1"; then
        if test -f $ldir/libgmp.a; then
           AC_MSG_RESULT(found)
           testlib=$ldir/libgmp.a
-	  CSL_CHECK_GMP($testlib,$testincludedir)
+          CSL_CHECK_GMP($testlib,$testincludedir)
           if test $run_ok = yes; then
             STATIC_GMP=$testlib
             STATIC_GMP_INCLUDE_DIR=$testincludedir
diff --git a/tests/regress/check.sh b/tests/regress/check.sh
index e2870e180..0849f6ea7 100755
--- a/tests/regress/check.sh
+++ b/tests/regress/check.sh
@@ -38,17 +38,25 @@ usage() {
    echo "Usage: $0 <test-directory> <bin-directory> [test1] [test2] ..."
    exit
 }
-    
+
+cleanup() {
+    [[ -n "$logdir" ]] && rm -rf "$logdir"
+}
+
 smt2_options=
+j_option=
 
-while getopts "s:" o; do
+while getopts "js:" o; do
     case "$o" in
-	s)
-	    smt2_options=${OPTARG}
-	    ;;
-	*)
-	    usage
-	    ;;
+    s)
+      smt2_options=${OPTARG}
+      ;;
+    j)
+      j_option=yes
+      ;;
+    *)
+      usage
+      ;;
     esac
 done
 shift $((OPTIND-1))
@@ -62,13 +70,10 @@ bin_dir=$2
 shift 2
 all_tests="$@"
 
-# Make sure fatal errors go to stderr
-export LIBC_FATAL_STDERR_=1
-
 #
 # System-dependent configuration
 #
-os_name=`uname 2>/dev/null` || os_name=unknown
+os_name=$(uname 2>/dev/null) || os_name=unknown
 
 case "$os_name" in
   *Darwin* )
@@ -81,50 +86,30 @@ case "$os_name" in
 
 esac
 
-#
-# We try bash's builtin time command
-#
-TIMEFORMAT="%U"
-
-
-#
-# Output colors
-#
-red=
-green=
-black=
-if test -t 1 ; then
-  red=`tput setaf 1`
-  green=`tput setaf 2`
-  black=`tput sgr0`
+parallel_tool=
+if command -v parallel &> /dev/null ; then
+    if parallel --version 2>&1 | grep GNU > /dev/null 2>&1 ; then
+        parallel_tool="gnu"
+    else
+        parallel_tool="more"
+    fi
 fi
 
 #
 # The temp file for output
 #
-outfile=`$mktemp_cmd` || { echo "Can't create temp file" ; exit 1 ; }
-timefile=`$mktemp_cmd` || { echo "Can't create temp file" ; exit 1 ; }
-
-fail=0
-pass=0
-
-failed_tests=()
+trap cleanup EXIT
+logdir=$($mktemp_cmd -d) || { echo "Can't create temp folder" ; exit 1 ; }
 
 if [[ -z "$REGRESS_FILTER" ]];
 then
-	REGRESS_FILTER="."
+    REGRESS_FILTER="."
 fi
 
-if [[ -z "$TIME_LIMIT" ]];
-then
-  TIME_LIMIT=60
-fi
-
-
 #
 # Check if MCSAT is supported
 #
-./$bin_dir/yices_smt2 --mcsat >& /dev/null < /dev/null
+./"$bin_dir"/yices_smt2 --mcsat >& /dev/null < /dev/null
 if [ $? -ne 0 ]
 then
     MCSAT_FILTER="-v mcsat"
@@ -132,114 +117,90 @@ else
     MCSAT_FILTER="."
 fi
 
-if test -z "$all_tests"; then
+if [ -z "$all_tests" ] ; then
     all_tests=$(
-	find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' |
-	    grep $REGRESS_FILTER | grep $MCSAT_FILTER |
-	    sort
+    find "$regress_dir" -name '*.smt' -or -name '*.smt2' -or -name '*.ys' |
+      grep $REGRESS_FILTER | grep $MCSAT_FILTER |
+      sort
     )
 fi
 
-for file in $all_tests; do
-
-    echo -n $file
-
-    # Get the binary based on the filename
-    filename=`basename "$file"`
-
-    options=
-    
-    case $filename in
-        *.smt2)
-            binary=yices_smt2
-	    options=$smt2_options
-            ;;
-        *.smt)
-            binary=yices_smtcomp
-            ;;
-        *.ys)
-            binary=yices
-            ;;
-        *)
-            echo FAIL: unknown extension for $filename
-            fail=`expr $fail + 1`
-            continue
-    esac
+if [ -t 1 ] ; then
+  color_flag="-c"
+fi
 
-    # Get the options
-    if [ -e "$file.options" ]
-    then
-        options="$options `cat $file.options`"
-        echo " [ $options ]"
-    	test_string="$file [ $options ]"
-    else
-        test_string="$file"
-        echo
-    fi
+# job_count 1: serial execution, 0: unrestricted parallel, n>1: n processes
+job_count=1
+
+#check if we are in a make run with -j N
+if [[ -n "$j_option" ]]; then
+    job_count=0
+elif [[ "$MAKEFLAGS" =~ --jobserver-(fds|auth)=([0-9]+),([0-9]+) ]]; then
+    # greedy get as many tokens as possible
+    fdR=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\2|")
+    fdW=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-(fds\|auth)=([0-9]+),([0-9]+).*|\3|")
+    while IFS= read -r -d '' -t 1 -n 1 <&"$fdR"; do
+      job_count=$((job_count+1))
+    done
+elif [[ "$MAKEFLAGS" =~ --jobserver-auth=fifo:([^ ]+) ]]; then
+    fifo=$(echo "$MAKEFLAGS" | sed -E "s|.*--jobserver-auth=fifo:([^ ]+).*|\1|")
+    while IFS= read -r -d '' -t 1 -n 1 <"$fifo"; do
+      job_count=$((job_count+1))
+    done
+elif [[ "$MAKEFLAGS" =~ (^|[ ])-?j($|[ ]) ]]; then
+    job_count=0
+fi
 
-    # Get the expected result
-    if [ -e "$file.gold" ]
-    then
-        gold=$file.gold
-    else
-        echo -n $red
-        echo FAIL: missing file: $file.gold
-        echo -n $black
-        fail=`expr $fail + 1`
-        failed_tests+=("$test_string")
-        continue
-    fi
+if [[ $job_count != 1 ]] && [[ -z "$parallel_tool" ]]; then
+    echo "**********************************************************"
+    echo "Install moreutils or GNU parallel to run tests in parallel"
+    echo "**********************************************************"
+else
+    case $job_count in
+        0) echo "Running in parallel";;
+        1) echo "Running sequentially";;
+        *) echo "Running with $job_count parallel jobs";;
+    esac
+fi
 
-    # Run the binary
-    (
-      ulimit -S -t $TIME_LIMIT &> /dev/null
-      ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null
-      (time ./$bin_dir/$binary $options ./$file >& $outfile ) >& $timefile
-    )
-    status=$?
-    thetime=`cat $timefile`
-
-    # Do the diff
-    DIFF=`diff -w $outfile $gold`
-
-    if [ $? -eq 0 ] && [ $status -eq 0 ]
-    then
-        echo -n $green
-    	echo PASS [${thetime} s]
-        echo -n $black
-        pass=`expr $pass + 1`
-    else
-        echo -n $red
-        echo FAIL
-        echo -n $black
-        fail=`expr $fail + 1`
-        failed_tests+=("$test_string"$'\n'"$DIFF")
-    fi
+j_param="-j$job_count"
+if [[ $job_count == 0 ]]; then j_param=""; fi
+
+case "$parallel_tool" in
+    more)
+        parallel -i $j_param bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" -- $all_tests
+        ;;
+    gnu)
+        parallel -q $j_param bash "${BASH_SOURCE%/*}/run_test.sh" $color_flag -s "$smt2_options" {} "$bin_dir" "$logdir" ::: $all_tests
+        ;;
+    *)
+        for file in $all_tests; do
+            bash "${BASH_SOURCE%/*}"/run_test.sh $color_flag -s "$smt2_options" "$file" "$bin_dir" "$logdir"
+        done
+        ;;
+esac
 
+# give back tokens
+while [[ $job_count -gt 1 ]]; do
+    [[ -n $fdW ]] && echo -n '+' >&"$fdW"
+    [[ -n $fifo ]] && echo -n '+' >"$fifo"
+    job_count=$((job_count-1))
 done
 
-rm $outfile
-rm $timefile
+pass=$(find "$logdir" -type f -name "*.pass" | wc -l)
+fail=$(find "$logdir" -type f -name "*.error" | wc -l)
 
-if [ $fail -eq 0 ]
-then
-    echo -n $green
-    echo Pass: $pass
-    echo Fail: $fail
-    echo -n $black
-else
-    echo -n $red
-    echo Pass: $pass
-    echo Fail: $fail
-    echo -n $black
-fi
+echo "Pass: $pass"
+echo "Fail: $fail"
 
-if [ $fail -eq 0 ]
-then
-    exit 0
+if [ "$fail" -eq 0 ] ; then
+    code=0
 else
-    for i in "${!failed_tests[@]}"; do echo "$((i+1)). ${failed_tests[$i]}"; done
-    exit 1
+    for f in "$logdir"/*.error ; do
+      cat "$f"
+      echo
+    done
+    code=1
 fi
 
-echo -n $black
+exit $code
diff --git a/tests/regress/run_test.sh b/tests/regress/run_test.sh
new file mode 100755
index 000000000..2ef34be9d
--- /dev/null
+++ b/tests/regress/run_test.sh
@@ -0,0 +1,195 @@
+#!/bin/bash
+
+#
+#  This file is part of the Yices SMT Solver.
+#  Copyright (C) 2017 SRI International.
+#
+#  Yices is free software: you can redistribute it and/or modify
+#  it under the terms of the GNU General Public License as published by
+#  the Free Software Foundation, either version 3 of the License, or
+#  (at your option) any later version.
+#
+#  Yices is distributed in the hope that it will be useful,
+#  but WITHOUT ANY WARRANTY; without even the implied warranty of
+#  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+#  GNU General Public License for more details.
+#
+#  You should have received a copy of the GNU General Public License
+#  along with Yices.  If not, see <http://www.gnu.org/licenses/>.
+#
+
+#
+# Run one single regression tests
+#
+# Usage: run_test.sh <test-file> <bin-dir> [<out-dir>]
+#
+# test-file is the test file the SMT1, SMT2, or Yices input language
+# bin-dir contains the Yices binaries for each of these languages
+# tmp-dir (optional) and specifies the location to put the results
+#
+# For each test file, the expected results are stored in file.gold
+# and command-line options are stored in file.options.
+#
+# This scripts calls the appropriate binary on each test file, passing it
+# the command-line options if any, then check whether the output matches
+# what's expected.
+#
+
+usage() {
+  echo "Usage: $0 <test-file> <bin-dir> [out-dir]"
+  exit 4
+}
+
+smt2_options=
+color=
+
+while getopts "cs:" o; do
+    case "$o" in
+    s)
+      smt2_options=${OPTARG}
+      ;;
+    c)
+      color="on"
+      ;;
+    *)
+      usage
+      ;;
+    esac
+done
+shift $((OPTIND-1))
+
+if [ $# -lt 2 ] ; then
+  usage
+fi
+
+test_file=$1
+bin_dir=$2
+
+if [ $# -ge 3 ] ; then
+  out_dir=$3
+fi
+
+export LIBC_FATAL_STDERR_=1
+
+#
+# System-dependent configuration
+#
+os_name=$(uname 2>/dev/null) || os_name=unknown
+
+case "$os_name" in
+  *Darwin* )
+     mktemp_cmd="/usr/bin/mktemp -t out"
+  ;;
+
+  * )
+     mktemp_cmd=mktemp
+  ;;
+
+esac
+
+#
+# We try bash's builtin time command
+#
+TIMEFORMAT="%U"
+
+
+#
+# Output colors
+#
+red=
+green=
+black=
+if [ -t 1 ] || [ -n "$color" ]; then
+    red=$(tput setaf 1)
+    green=$(tput setaf 2)
+    black=$(tput sgr0)
+fi
+
+#
+# The temp file for output
+#
+outfile=$($mktemp_cmd) || { echo "Can't create temp file" ; exit 3 ; }
+timefile=$($mktemp_cmd) || { echo "Can't create temp file" ; exit 3 ; }
+
+if [[ -z "$TIME_LIMIT" ]];
+then
+    TIME_LIMIT=60
+fi
+
+# Get the binary based on the filename
+filename=$(basename "$test_file")
+
+options=
+
+case $filename in
+    *.smt2)
+        binary=yices_smt2
+        options=$smt2_options
+        ;;
+    *.smt)
+        binary=yices_smtcomp
+        ;;
+    *.ys)
+        binary=yices
+        ;;
+    *)
+        echo "FAIL: unknown extension for $filename"
+        exit 2
+esac
+
+# Get the options
+if [ -e "$test_file.options" ]
+then
+    options="$options $(cat "$test_file.options")"
+    test_string="$test_file [ $options ]"
+else
+    test_string="$test_file"
+fi
+
+# Get the expected result
+if [ -e "$test_file.gold" ]
+then
+    gold=$test_file.gold
+else
+    echo "$red FAIL: missing file: $test_file.gold $black"
+    exit 2
+fi
+
+if [ -d "$out_dir" ] ; then
+    # replace _ with __ and / with _
+    log_file="$out_dir/_$(echo "${test_file//_/__}" | tr '/' '_')}"
+fi
+
+# Run the binary
+(
+  ulimit -S -t $TIME_LIMIT &> /dev/null
+  ulimit -H -t $((1+$TIME_LIMIT)) &> /dev/null
+  (time "./$bin_dir/$binary" $options "./$test_file" >& "$outfile" ) >& "$timefile"
+)
+status=$?
+runtime=$(cat "$timefile")
+
+# Do the diff
+DIFF=$(diff -w "$outfile" "$gold")
+
+if [ $? -eq 0 ] && [ $status -eq 0 ]
+then
+    echo -e "$green PASS [${runtime} s] $black $test_string"
+    if [ -n "$log_file" ] ; then
+        log_file="$log_file.pass"
+        echo "$test_string" > "$log_file"
+    fi
+    code=0
+else
+    echo -e "$red FAIL $black $test_string"
+    if [ -n "$log_file" ] ; then
+        log_file="$log_file.error"
+        echo "$test_string" > "$log_file"
+        echo "$DIFF" >> "$log_file"
+    fi
+    code=1
+fi
+
+rm "$timefile"
+rm "$outfile"
+exit $code