More unwinding should not yield additional assertion failures

See https://groups.google.com/d/msg/cprover-support/FQHJYskRRuI/mKo7EQq9BAAJ for
discussion and the source of this regression test. The problem is addressed by
the prior commits on this branch/pull request.

regression/cbmc/Malloc24/main.c

@@ -0,0 +1,47 @@
+#include <stdlib.h>
+
+struct node
+{
+    int value;
+    struct node *next;
+};
+
+struct list
+{
+  int size;
+  struct node *head;
+};
+
+void removeLast(struct list * l)
+{
+  int index = l->size - 1;
+  struct node **current;
+  for(current = &(l->head); index && *current; index--)
+    current = &(*current)->next;
+  *current = (*current)->next;
+  l->size--;
+}
+
+int main () {
+  //build a 2-nodes list
+  struct node *n0 = malloc(sizeof(struct node));
+  struct node *n1 = malloc(sizeof(struct node));
+  struct list *l = malloc(sizeof(struct list));
+  l->size = 2;
+  l->head = n0;
+
+  n0->next=n1;
+  n1->next=NULL;
+
+  //remove last node from list
+
+  //this passes
+  // struct node **current = &(l->head);
+  // current = &(*current)->next;
+  // *current = (*current)->next;
+  // l->size--;
+  //this doesn't
+  removeLast(l);
+
+  __CPROVER_assert(n0->next == NULL , "not NULL");
+}

regression/cbmc/Malloc24/test.desc

@@ -0,0 +1,8 @@
+CORE
+main.c
+--unwind 4 --pointer-check --unwinding-assertions
+^EXIT=0$
+^SIGNAL=0$
+^VERIFICATION SUCCESSFUL$
+--
+^warning: ignoring