Tests for incremental status with multiple properties

The incremental status should report failure from the first unwinding
for which one property is falsified.

Author: Thomas Kiley

regression/cbmc-incr-oneloop/multiple-asserts/test-no-cp.desc

@@ -0,0 +1,19 @@
+CORE
+test.c
+--incremental-loop main.0 --no-propagation
+activate-multi-line-match
+Current unwinding: 1\nUnwinding .*\nIncremental status: INCONCLUSIVE
+Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE
+Current unwinding: 7\nUnwinding .*\nIncremental status: FAILURE
+Current unwinding: 9\nUnwinding .*\nIncremental status: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Ensure that with multiple properites, the incremental stauts
+switches to failure as soon as one property has been falsified
+but keeps unwinding till it has resolved them all
+
+Use `--no-propagation` to ensure that even the output is the same regardless of whether the asserts are checked via the solver or the constant propogator

regression/cbmc-incr-oneloop/multiple-asserts/test.c

@@ -0,0 +1,7 @@
+int main() {
+	for(int i = 0; i < 10; ++i) {
+		assert(i != 5);
+		assert(i != 8);
+	}
+	return 0;
+}

regression/cbmc-incr-oneloop/multiple-asserts/test.desc

@@ -0,0 +1,17 @@
+CORE
+test.c
+--incremental-loop main.0
+activate-multi-line-match
+Current unwinding: 1\nUnwinding .*\nIncremental status: INCONCLUSIVE
+Current unwinding: 6\nUnwinding .*\nIncremental status: INCONCLUSIVE
+Current unwinding: 7\nUnwinding .*\nIncremental status: FAILURE
+Current unwinding: 9\nUnwinding .*\nIncremental status: FAILURE
+^EXIT=10$
+^SIGNAL=0$
+^VERIFICATION FAILED$
+--
+^warning: ignoring
+--
+Ensure that with multiple properites, the incremental stauts
+switches to failure as soon as one property has been falsified
+but keeps unwinding till it has resolved them all