diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-10-11 19:20:16 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2015-10-11 19:20:16 -0400 |
| commit | c79677bdfc6342d4f669b7343a35511334503fdb (patch) | |
| tree | 0ae71f14d13493844dad858f393c9ab870536c45 /test | |
| parent | 4fd18dee3156a6dd1903b95662034d6e996ff88b (diff) | |
fix regression tests, support fallback mode for proofs
Diffstat (limited to 'test')
| -rwxr-xr-x | test/regress/run_regression | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/test/regress/run_regression b/test/regress/run_regression index b6fb735fe..9204fe33c 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -239,6 +239,7 @@ if [ "$proof" = yes ]; then ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null && ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--unconstrained-simp' &>/dev/null && ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null && + ! expr "$BINARY" : '.*pcvc4' &>/dev/null && ! expr "$benchmark" : '.*\.sy$' &>/dev/null; then # later on, we'll run another test with --check-proofs on check_proofs=true @@ -248,6 +249,7 @@ if [ "$proof" = yes ]; then ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null && ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--unconstrained-simp' &>/dev/null && ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null && + ! expr "$BINARY" : '.*pcvc4' &>/dev/null && ! expr "$benchmark" : '.*\.sy$' &>/dev/null; then # later on, we'll run another test with --check-unsat-cores on check_unsat_cores=true |