diff --git a/regression/cbmc/gcc_switch_case_range1/test.desc b/regression/cbmc/gcc_switch_case_range1/test.desc
index 50c1f3315fb..1c486bc871a 100644
--- a/regression/cbmc/gcc_switch_case_range1/test.desc
+++ b/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
diff --git a/regression/cbmc/gcc_switch_case_range2/test.desc b/regression/cbmc/gcc_switch_case_range2/test.desc
index cfa6e0b1e20..de6a3e88b0b 100644
--- a/regression/cbmc/gcc_switch_case_range2/test.desc
+++ b/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
diff --git a/regression/cbmc/havoc_object1/test.desc b/regression/cbmc/havoc_object1/test.desc
index abe30d88695..b70cee38dab 100644
--- a/regression/cbmc/havoc_object1/test.desc
+++ b/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$
 --