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