From 1563e30e08f9cbc4d0845360ceea4386e105193b Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 11 Jul 2017 10:38:23 +0100
Subject: [PATCH 1/2] Enable strings test suite

 - Enables regression/strings test suite
 - Updates the regression/strings Makefile to the latest version
---
 regression/Makefile         |  1 +
 regression/strings/Makefile | 36 ++++++++++++++++++++++++++++++++++--
 2 files changed, 35 insertions(+), 2 deletions(-)

diff --git a/regression/Makefile b/regression/Makefile
index cec34c0b37f..1946f6ce614 100644
--- a/regression/Makefile
+++ b/regression/Makefile
@@ -7,6 +7,7 @@ DIRS = ansi-c \
        goto-analyzer \
        goto-instrument \
        goto-instrument-typedef \
+       strings \
        strings-smoke-tests \
        test-script \
        # Empty last line
diff --git a/regression/strings/Makefile b/regression/strings/Makefile
index f9aee8c563e..47653a6bb95 100644
--- a/regression/strings/Makefile
+++ b/regression/strings/Makefile
@@ -1,6 +1,38 @@
+default: tests.log
 
 test:
-	@../test.pl -c ../../../src/cbmc/cbmc
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
 
 testfuture:
-	@../test.pl -c ../../../src/cbmc/cbmc -F
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc -CF ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+testall:
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc -CFTK ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+tests.log: ../test.pl
+	@if ! ../test.pl -c ../../../src/cbmc/cbmc ; then \
+		../failed-tests-printer.pl ; \
+		exit 1 ; \
+	fi
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	find -name '*.out' -execdir $(RM) '{}' \;
+	find -name '*.gb' -execdir $(RM) '{}' \;
+	$(RM) tests.log
+

From 40ac691045f07dbf4294ff8d4690963699d23746 Mon Sep 17 00:00:00 2001
From: "Lukasz A.J. Wrona" <lukasz.andrzej.wrona@gmail.com>
Date: Tue, 11 Jul 2017 10:44:43 +0100
Subject: [PATCH 2/2] Fix a "bug-test-gen-095" test description

---
 regression/strings/bug-test-gen-095/test.desc | 7 ++++---
 1 file changed, 4 insertions(+), 3 deletions(-)

diff --git a/regression/strings/bug-test-gen-095/test.desc b/regression/strings/bug-test-gen-095/test.desc
index a40f9e43402..99d5a8b4bd8 100644
--- a/regression/strings/bug-test-gen-095/test.desc
+++ b/regression/strings/bug-test-gen-095/test.desc
@@ -1,7 +1,8 @@
-KNOWNBUG
+CORE
 test.class
 --refine-strings
-^EXIT=0$
+^EXIT=10$
 ^SIGNAL=0$
-^VERIFICATION SUCCESSFUL$
+[.*assertion\.1] .* line 8 .* FAILURE
+^VERIFICATION FAILED$
 --