summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rwxr-xr-xtest/regress/run_regression2
1 files changed, 1 insertions, 1 deletions
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
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback