Make tests pass with single-path symbolic execution

Each run of symbolic execution reports the number of properties that failed *in
this run*, and it isn't always possible to violate multiple properties along a
single path. All paths together, however, show the same property violations as
path-merging symbolic execution.

Author: tautschnig

regression/cbmc/gcc_switch_case_range1/test.desc

@@ -4,6 +4,9 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\*\* 4 of 4 failed
+^\[main.assertion.1\] line 12 0 works: FAILURE$
+^\[main.assertion.2\] line 19 \.\.\. works: FAILURE$
+^\[main.assertion.3\] line 22 13 works: FAILURE$
+^\[main.assertion.4\] line 25 default works: FAILURE$
 --
 ^warning: ignoring

regression/cbmc/gcc_switch_case_range2/test.desc

@@ -4,6 +4,8 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\*\* 3 of 3 failed
+^\[main.assertion.1\] line 15 0 works: FAILURE$
+^\[main.assertion.2\] line 24 \.\.\. works: FAILURE$
+^\[main.assertion.3\] line 27 default works: FAILURE$
 --
 ^warning: ignoring

regression/cbmc/havoc_object1/test.desc

@@ -4,5 +4,12 @@ main.c
 ^EXIT=10$
 ^SIGNAL=0$
 ^VERIFICATION FAILED$
-^\*\* 6 of 8 failed.*$
+^\[main.assertion.1\] line 5 i==0: FAILURE$
+^\[main.assertion.2\] line 11 array\[3\]: FAILURE$
+^\[main.assertion.3\] line 15 struct i: FAILURE$
+^\[main.assertion.4\] line 16 struct j: FAILURE$
+^\[main.assertion.5\] line 26 i==20 \(A\): FAILURE$
+^\[main.assertion.6\] line 27 some_struct.i==30 \(A\): SUCCESS$
+^\[main.assertion.7\] line 31 i==20 \(B\): SUCCESS$
+^\[main.assertion.8\] line 32 some_struct\.i==30 \(B\): FAILURE$
 --