diff options
Diffstat (limited to 'test/regress/run_regression')
| -rwxr-xr-x | test/regress/run_regression | 12 |
1 files changed, 11 insertions, 1 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index 65ab6c31a..439c8e6c9 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -77,7 +77,17 @@ else echo "$expected_error" >"$experrfile" fi -("$cvc4" --segv-nospin "$benchmark"; echo $? >"$exitstatusfile") > "$outfile" 2> "$errfile" +cvc4dir=`dirname "$cvc4"` +cvc4dirfull=`cd "$cvc4dir" && pwd` +if [ -z "$cvc4dirfull" ]; then + error "getting directory of \`$cvc4 !?" +fi +cvc4base=`basename "$cvc4"` +cvc4full="$cvc4dirfull/$cvc4base" +( cd `dirname "$benchmark"`; + "$cvc4full" --segv-nospin `basename "$benchmark"`; + echo $? >"$exitstatusfile" +) > "$outfile" 2> "$errfile" diffs=`diff -u "$expoutfile" "$outfile"` diffexit=$? |