Loop counter resetting must not result in unlimited unwinding

Loops with multiple entry points previously resulted in unlimited
unwinding as loop counters were wrongly being reset via edges leaving
one of the loops (and entering the other).

Author: tautschnig

regression/cbmc/unwind_counters4/main.c

@@ -0,0 +1,24 @@
+int main()
+{
+  int x;
+  int y;
+
+  do
+  {
+    y = 10;
+    goto label;
+    x = 1; // dead code, makes sure the above goto is not removed
+  label:
+    _Bool nondet;
+    if(nondet)
+      __CPROVER_assert(y != 10, "violated via first loop");
+    else
+      __CPROVER_assert(y != 20, "violated via second loop");
+
+    if(x % 2)
+      break; // this statement must not cause the loop counter to be reset
+  } while(1);
+
+  y = 20;
+  goto label;
+}

regression/cbmc/unwind_counters4/test.desc

@@ -0,0 +1,11 @@
+CORE
+main.c
+--unwind 2
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+^\** 2 of 2 failed
+--
+--
+Loop unwinding must terminate despite the existence of multiple loop entry
+points.

src/goto-symex/symex_main.cpp

@@ -97,7 +97,7 @@ void symex_transition(
     for(const auto &i_e : instruction.incoming_edges)
     {
       if(
-        i_e->is_goto() && i_e->is_backwards_goto() &&
+        i_e->is_backwards_goto() && i_e->get_target() == to &&
         (!is_backwards_goto ||
          state.source.pc->location_number > i_e->location_number))
       {