diff --git a/regression/Makefile b/regression/Makefile index 496ecf34283..6434bdc167c 100644 --- a/regression/Makefile +++ b/regression/Makefile @@ -78,7 +78,7 @@ endif .PHONY: test test: @for dir in $(DIRS); do \ - $(MAKE) "$$dir" || exit 1; \ + $(MAKE) "$$dir" test || exit 1; \ done; # Pattern to execute a single test suite directory diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile index d4b3dbe7220..3a31f84a87b 100644 --- a/regression/cbmc/Makefile +++ b/regression/cbmc/Makefile @@ -9,7 +9,7 @@ else GCC_ONLY = endif -test: +test: test-cprover-smt2 test-paths-lifo @../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY) test-cprover-smt2: