From 6b830fd5e43b05437119fd39c6d8f651f31298b6 Mon Sep 17 00:00:00 2001
From: martin <martin@michael>
Date: Fri, 29 Apr 2022 16:49:48 +0100
Subject: [PATCH] A test case which demonstrates the problem

---
 regression/goto-analyzer/recursion-01/main.c    | 15 +++++++++++++++
 regression/goto-analyzer/recursion-01/test.desc | 10 ++++++++++
 2 files changed, 25 insertions(+)
 create mode 100644 regression/goto-analyzer/recursion-01/main.c
 create mode 100644 regression/goto-analyzer/recursion-01/test.desc

diff --git a/regression/goto-analyzer/recursion-01/main.c b/regression/goto-analyzer/recursion-01/main.c
new file mode 100644
index 00000000000..679379d720c
--- /dev/null
+++ b/regression/goto-analyzer/recursion-01/main.c
@@ -0,0 +1,15 @@
+int nondet_int(void);
+
+void rec ( void ) {
+  if (nondet_int()) {
+    rec();
+    __CPROVER_assert(0, "Clearly reachable");
+  }
+  return;
+}
+
+int main()
+{
+  rec();
+  return 0;
+}
diff --git a/regression/goto-analyzer/recursion-01/test.desc b/regression/goto-analyzer/recursion-01/test.desc
new file mode 100644
index 00000000000..95dcbfe6ec2
--- /dev/null
+++ b/regression/goto-analyzer/recursion-01/test.desc
@@ -0,0 +1,10 @@
+CORE
+main.c
+--verify --vsd
+^EXIT=0$
+^SIGNAL=0$
+^\[main\.assertion\.1\] .* assertion y != 0: SUCCESS$
+^\[main\.assertion\.2\] .* assertion y == 0: SUCCESS \(unreachable\)$
+^\[main\.assertion\.3\] .* assertion z == 1: SUCCESS$
+--
+^warning: ignoring