From 05e2dd4fd5e65ff9cfdcad537b2fa5f694f2851f Mon Sep 17 00:00:00 2001
From: thk123 <thomas@diffblue.com>
Date: Wed, 29 Mar 2017 16:18:08 +0100
Subject: [PATCH] Test to demonstate assert bug on alpine

The user added assert in this test does not get coverage under alpine
linux.
---
 regression/cbmc/simple_assert/main.c    |  9 +++++++++
 regression/cbmc/simple_assert/test.desc | 14 ++++++++++++++
 2 files changed, 23 insertions(+)
 create mode 100644 regression/cbmc/simple_assert/main.c
 create mode 100644 regression/cbmc/simple_assert/test.desc

diff --git a/regression/cbmc/simple_assert/main.c b/regression/cbmc/simple_assert/main.c
new file mode 100644
index 00000000000..e9ff60b7a83
--- /dev/null
+++ b/regression/cbmc/simple_assert/main.c
@@ -0,0 +1,9 @@
+#include <assert.h>
+
+int main(int argc, char* argv[])
+{
+  int x = 5;
+  assert(x==5);
+
+  return 0;
+}
diff --git a/regression/cbmc/simple_assert/test.desc b/regression/cbmc/simple_assert/test.desc
new file mode 100644
index 00000000000..c38a891e8d3
--- /dev/null
+++ b/regression/cbmc/simple_assert/test.desc
@@ -0,0 +1,14 @@
+CORE
+main.c
+--cover location
+
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.coverage\.1\] .* function main block 1: SATISFIED$
+^\[main\.coverage\.2\] .* function main block 2: SATISFIED$
+^\[main\.coverage\.3\] .* function main block 3: SATISFIED$
+^\[main\.coverage\.4\] .* function main block 4: SATISFIED$
+4 of 4 covered \(100.0%\)$
+--
+^warning: ignoring
+^CONVERSION ERROR$