diff options
| author | Andres Noetzli <noetzli@stanford.edu> | 2018-03-08 23:27:31 -0800 |
|---|---|---|
| committer | Andres Noetzli <noetzli@stanford.edu> | 2018-03-08 23:27:31 -0800 |
| commit | 4d4e1bdce951bb73767894f22dc885500d9d4bc5 (patch) | |
| tree | 75534226dee696bd63ecb337644eb3080dba7df1 | |
| parent | c6b2e085d4eb2c232a528a96e13fc7b65fd98fea (diff) | |
Skip (get-unsat-assumptions) tests not supported
(get-unsat-assumptions) requires the proof infrastructure,so we can't
run the regression tests if CVC4 has not been configured for it. This
commit changes the regression script to skip tests containing
(get-unsat-assumptions) when CVC4 has not been compiled with proof
support.
| -rw-r--r-- | test/regress/regress0/arr1.smt2 | 1 | ||||
| -rwxr-xr-x | test/regress/run_regression | 2 |
2 files changed, 1 insertions, 2 deletions
diff --git a/test/regress/regress0/arr1.smt2 b/test/regress/regress0/arr1.smt2 index 844f7d8e5..1c9747abe 100644 --- a/test/regress/regress0/arr1.smt2 +++ b/test/regress/regress0/arr1.smt2 @@ -7,4 +7,3 @@ (declare-fun i2 () Index) (assert (not (=> (= i1 i2) (= (select a i1) (select a i2))))) (check-sat) - diff --git a/test/regress/run_regression b/test/regress/run_regression index e236234e1..6b2447d8e 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -134,7 +134,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then # If this test case requires unsat cores but CVC4 is not built with proof # support, skip it. Note: checking $CVC4_REGRESSION_ARGS instead of $proof # here because $proof is not set for the second run. - requires_proof=`grep '(get-unsat-core)' "$benchmark"` + requires_proof=`grep '(get-unsat-core)\|(get-unsat-assumptions)' "$benchmark"` if [[ ! "$CVC4_REGRESSION_ARGS" = *"--proof"* ]] && [ -n "$requires_proof" ]; then exit 77 fi |