From 97e9314c918064c408643e1a5f38feb649f762ac Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 3 Jul 2018 10:45:17 +0000
Subject: [PATCH 1/2] Do not hardcode tests.log as option -s <suffix> may be in
 use

With -s <suffix> the output log file is actually tests-<suffix>.log.
---
 regression/test.pl | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/regression/test.pl b/regression/test.pl
index 1a87c2a24a4..9f9e630b394 100755
--- a/regression/test.pl
+++ b/regression/test.pl
@@ -421,7 +421,7 @@ ($)
 close LOG;
 
 if($opt_p && $failures != 0) {
-  open LOG,"<tests.log" or die "Failed to open tests.log\n";
+  open LOG,"<$logfile_name" or die "Failed to open $logfile_name\n";
 
   my $printed_this_test = 1;
   my $current_test = "";

From 2be11f37c461c3ef1258a61da27bfdfb89faa270 Mon Sep 17 00:00:00 2001
From: Michael Tautschnig <tautschn@amazon.com>
Date: Tue, 3 Jul 2018 10:53:24 +0000
Subject: [PATCH 2/2] Make "clean" target in regression tests do full cleanup

---
 jbmc/regression/jbmc-strings/Makefile | 2 +-
 jbmc/regression/jbmc/Makefile         | 2 +-
 regression/cbmc/Makefile              | 2 +-
 regression/goto-gcc/Makefile          | 1 +
 regression/invariants/Makefile        | 5 +++++
 5 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/jbmc/regression/jbmc-strings/Makefile b/jbmc/regression/jbmc-strings/Makefile
index 4ff4e5ba834..6a87a176e59 100644
--- a/jbmc/regression/jbmc-strings/Makefile
+++ b/jbmc/regression/jbmc-strings/Makefile
@@ -28,4 +28,4 @@ show:
 clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	find -name '*.gb' -execdir $(RM) '{}' \;
-	$(RM) tests.log
+	$(RM) tests.log tests-symex-driven-loading.log
diff --git a/jbmc/regression/jbmc/Makefile b/jbmc/regression/jbmc/Makefile
index 81024778e07..1639d08dea4 100644
--- a/jbmc/regression/jbmc/Makefile
+++ b/jbmc/regression/jbmc/Makefile
@@ -20,7 +20,7 @@ show:
 clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	find -name '*.gb' -execdir $(RM) '{}' \;
-	$(RM) tests.log
+	$(RM) tests.log tests-symex-driven-loading.log
 
 %.class: %.java ../../src/org.cprover.jar
 	javac -g -cp ../../src/org.cprover.jar:. $<
diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
index 8096fc27cb3..e376acf4a28 100644
--- a/regression/cbmc/Makefile
+++ b/regression/cbmc/Makefile
@@ -15,5 +15,5 @@ show:
 
 clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
-	find -name '*.gb' -execdir $(RM) '{}' \;
+	find -name '*.smt2' -execdir $(RM) '{}' \;
 	$(RM) tests.log
diff --git a/regression/goto-gcc/Makefile b/regression/goto-gcc/Makefile
index e7838b58131..8c6ebfa9738 100644
--- a/regression/goto-gcc/Makefile
+++ b/regression/goto-gcc/Makefile
@@ -18,4 +18,5 @@ show:
 clean:
 	find -name '*.out' -execdir $(RM) '{}' \;
 	find -name '*.gb' -execdir $(RM) '{}' \;
+	find -name '*.goto-cc-saved' -execdir $(RM) '{}' \;
 	$(RM) tests.log
diff --git a/regression/invariants/Makefile b/regression/invariants/Makefile
index 4fbc8a60aee..758be254a65 100644
--- a/regression/invariants/Makefile
+++ b/regression/invariants/Makefile
@@ -25,3 +25,8 @@ show:
 
 driver$(EXEEXT): $(OBJ)
 	$(LINKBIN)
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	$(RM) driver$(EXEEXT) driver$(DEPEXT) driver$(OBJEXT)
+	$(RM) tests.log