diff options
author | Andres Noetzli <andres.noetzli@gmail.com> | 2019-11-06 08:40:22 -0800 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2019-11-06 10:40:22 -0600 |
commit | 223d35d897f570aec7599d25c20041bc5306ccb6 (patch) | |
tree | ac8a1c3032888fd7412f360db45b378917d06d07 | |
parent | 52e71b709504ed06ced34962692a329f4c8282ce (diff) |
[Regressions] Remove leading whitespace in output (#3444)
-rwxr-xr-x | test/regress/run_regression.py | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py index d445264fb..8e9261ec2 100755 --- a/test/regress/run_regression.py +++ b/test/regress/run_regression.py @@ -342,6 +342,8 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper, output, error, exit_status = run_benchmark( dump, wrapper, scrubber, error_scrubber, cvc4_binary, command_line_args, benchmark_dir, benchmark_basename, timeout) + output = re.sub(r'^[ \t]*', '', output, flags=re.MULTILINE) + error = re.sub(r'^[ \t]*', '', error, flags=re.MULTILINE) if output != expected_output: exit_code = EXIT_FAILURE print( |