Incorrectly labeled termination benchmarks in seq-mthreaded/

[mchalupa]

These benchmarks from seq-mthreaded directory seem to be incorrectly labeled w.r.t the no-termination property:

pals_floodmax.3.3.ufo.UNBOUNDED.pals.c
pals_lcr.3_overflow.ufo.UNBOUNDED.pals.c
pals_lcr.5_overflow.ufo.UNBOUNDED.pals.c
pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c
pals_floodmax.3_overflow.ufo.UNBOUNDED.pals.c
pals_lcr.4_overflow.ufo.UNBOUNDED.pals.c
pals_opt-floodmax.3.2.ufo.UNBOUNDED.pals.c
pals_opt-floodmax.3_overflow.ufo.UNBOUNDED.pals.c

Although they have a while(1) loop, this loop contains an assertion that eventually fails on every path. You can check that the loop is in fact bounded by instrumenting the programs with an explicit counter of the iterations and asserting that this counter has an upper bound, e.g.,:

diff --git a/c/seq-mthreaded/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c b/c/seq-mthreaded/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c
index c80275cd00..37f69eb350 100644
--- a/c/seq-mthreaded/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c
+++ b/c/seq-mthreaded/pals_floodmax.3.3.ufo.UNBOUNDED.pals.c
@@ -534,7 +534,9 @@ int main(void)
   p32_old = nomsg;
   p32_new = nomsg;
   i2 = 0;
+  unsigned counter = 0;
   while (1) {
+    assert(counter++ < 4);
     {
     node1();
     node2();
@@ -552,7 +554,9 @@ int main(void)
     p32_old = p32_new;
     p32_new = nomsg;
     c1 = check();
-    assert(c1);
+    //assert(c1);
+    if (!c1)
+        abort();
     }
   }
 }

The upper bounds (not all of them are tight) for the benchmarks are as follows:

benchmark	upper bound
pals_floodmax.3.3.ufo.UNBOUNDED.pals.c	4
pals_lcr.3_overflow.ufo.UNBOUNDED.pals.c	515
pals_lcr.5_overflow.ufo.UNBOUNDED.pals.c	512
pals_opt-floodmax.3.3.ufo.UNBOUNDED.pals.c	4
pals_floodmax.3_overflow.ufo.UNBOUNDED.pals.c	950
pals_lcr.4_overflow.ufo.UNBOUNDED.pals.c	512
pals_opt-floodmax.3.2.ufo.UNBOUNDED.pals.c	2
pals_opt-floodmax.3_overflow.ufo.UNBOUNDED.pals.c	600

I checked that the assertions for upper bound hold with Symbiotic and CPAchecker (and some of the benchmarks also with other tools, e.g., CBMC with --unwinding-assertions or KLEE).