From d169b18bf17693f0997a87e8d5d37a567da6ec85 Mon Sep 17 00:00:00 2001
From: Thomas Given-Wilson <thomas.givenwilson@diffblue.com>
Date: Thu, 1 Apr 2021 17:01:30 +0100
Subject: [PATCH 1/3] Unify make and cmake behaviours

This fixes the inconsistencies between cmake and make
behaviours.
---
 regression/Makefile      | 2 +-
 regression/cbmc/Makefile | 4 ++++
 2 files changed, 5 insertions(+), 1 deletion(-)

diff --git a/regression/Makefile b/regression/Makefile
index 496ecf34283..d697d41fbd2 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -85,7 +85,7 @@ test:
 .PHONY: $(DIRS)
 $(DIRS):
 	@echo "Running $@..." ;
-	$(MAKE) -C "$@" test || exit 1;
+	$(MAKE) -C "$@" || exit 1;
 
 # Run all test directories using GNU Parallel
 .PHONY: test-parallel
diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
index d4b3dbe7220..25065f755fd 100644
--- a/regression/cbmc/Makefile
+++ b/regression/cbmc/Makefile
@@ -1,3 +1,5 @@
+THIS_FILE := $(lastword $(MAKEFILE_LIST))
+
 default: test
 
 include ../../src/config.inc
@@ -11,6 +13,8 @@ endif
 
 test:
 	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" -X smt-backend $(GCC_ONLY)
+	@$(MAKE) -f $(THIS_FILE) test-paths-lifo
+	@$(MAKE) -f $(THIS_FILE) test-cprover-smt2
 
 test-cprover-smt2:
 	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \

From d88e3d7c4905691f49c90c03488b31a41922758c Mon Sep 17 00:00:00 2001
From: Thomas Given-Wilson <thomas.givenwilson@diffblue.com>
Date: Tue, 6 Apr 2021 09:41:53 +0100
Subject: [PATCH 2/3] Use dependency style make

Change from calling the separate make targets inside a default
to instead using make dependency style.
---
 regression/cbmc/Makefile | 6 +-----
 1 file changed, 1 insertion(+), 5 deletions(-)

diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
index 25065f755fd..3a31f84a87b 100644
--- a/regression/cbmc/Makefile
+++ b/regression/cbmc/Makefile
@@ -1,5 +1,3 @@
-THIS_FILE := $(lastword $(MAKEFILE_LIST))
-
 default: test
 
 include ../../src/config.inc
@@ -11,10 +9,8 @@ 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)
-	@$(MAKE) -f $(THIS_FILE) test-paths-lifo
-	@$(MAKE) -f $(THIS_FILE) test-cprover-smt2
 
 test-cprover-smt2:
 	@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" \

From bc541389eed06d792e78794834f58e34c5922928 Mon Sep 17 00:00:00 2001
From: Thomas Given-Wilson <thomas.givenwilson@diffblue.com>
Date: Fri, 9 Apr 2021 09:37:38 +0100
Subject: [PATCH 3/3] Unify the other way

---
 regression/Makefile | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/regression/Makefile b/regression/Makefile
index d697d41fbd2..6434bdc167c 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -78,14 +78,14 @@ 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
 .PHONY: $(DIRS)
 $(DIRS):
 	@echo "Running $@..." ;
-	$(MAKE) -C "$@" || exit 1;
+	$(MAKE) -C "$@" test || exit 1;
 
 # Run all test directories using GNU Parallel
 .PHONY: test-parallel