Test for printing multiple goto traces from one counterexample

The traces need to be correctly truncated so that
the failing property comes last.
The traces are printed in the same order as the properties
are listed in the result report.

Author: peterschrammel

regression/cbmc/multiple-goto-traces/main.c

@@ -0,0 +1,14 @@
+#include <assert.h>
+
+int main(int argc, char** argv)
+{
+  assert(4 != argc);
+  argc++;
+  argc--;
+  assert(argc >= 1);
+  assert(argc != 4);
+  argc++;
+  argc--;
+  assert(argc + 1 != 5);
+  return 0;
+}

regression/cbmc/multiple-goto-traces/test.desc

@@ -0,0 +1,14 @@
+CORE
+main.c
+--trace
+activate-multi-line-match
+EXIT=10
+SIGNAL=0
+VERIFICATION FAILED
+Trace for main\.assertion\.1:(\n.*){16}  assertion 4 \!= argc(\n.*){5}Trace for main\.assertion\.3:(\n.*){30}  assertion argc != 4(\n.*){5}Trace for main\.assertion\.4:(\n.*){44}  assertion argc \+ 1 != 5
+\*\* 3 of 4 failed
+--
+^warning: ignoring
+--
+We have one counterexample violating multiple properties.
+Make sure the traces are correctly truncated.