Add a regression test based on the original code cited in #6168.

This also demonstrates the issue being fixed.

Author: NlightNFotis

regression/goto-instrument/github_6168_infinite_unwinding_bug/main.c

@@ -0,0 +1,21 @@
+#include <assert.h>
+#include <stdlib.h>
+
+static int adder(const int *a, const int *b)
+{
+  return (*a + *b);
+}
+
+int main()
+{
+  int x = 1024;
+
+  int (*local_adder)(const int *, const int *) = adder;
+
+  while(x > 0)
+  __CPROVER_loop_invariant(1 == 1)
+  {
+    x += local_adder(&x, &x); // loop detection fails
+    //x += adder(&x, &x);       // works fine
+  }
+}

regression/goto-instrument/github_6168_infinite_unwinding_bug/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--enforce-all-contracts
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+^\[main.1\] line \d+ Check loop invariant before entry: SUCCESS$
+^\[main.2\] line \d+ Check that loop invariant is preserved: SUCCESS$
+--
+--
+This is guarding against an issue described in https://github.com/diffblue/cbmc/issues/6168.