A test case which demonstrates the problem

martin-cs · Feb 2, 2024 · 6b830fd · 6b830fd
1 parent 5bdff46
commit 6b830fd
Show file tree

Hide file tree

Showing 2 changed files with 25 additions and 0 deletions.
diff --git a/regression/goto-analyzer/recursion-01/main.c 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
@@ -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