diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy
index 71e24a19203..7b12a4452d7 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy
@@ -1,5 +1,4 @@
-// RUN: %exits-with 4 %verify --cores 1 --progress "%s" > "%t".raw
-// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
+// RUN: %exits-with 4 %verify --isolate-assertions --cores 1 "%s" > "%t"
 // RUN: %diff "%s.expect" "%t"
 
 // These tests make sure that the built-in arrow types are taken into account when
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect
index 0090517f563..a7d4037754a 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/hofs/ArrowTypeOptimizations.dfy.expect
@@ -1,19 +1,5 @@
-Verified 0/7 symbols. Waiting for CheckReads to verify.
-Verification part 1/1 of CheckReads, on line 8, could not prove all assertions, redacted and consuming 1.1E+004 resources
-ArrowTypeOptimizations.dfy(11,2): Error: function precondition could not be proved
-ArrowTypeOptimizations.dfy(11,2): Error: insufficient reads clause to invoke function
-Verified 1/7 symbols. Waiting for CheckPre to verify.
-Verification part 1/1 of CheckPre, on line 14, could not prove all assertions, redacted and consuming 1.0E+004 resources
-ArrowTypeOptimizations.dfy(17,2): Error: function precondition could not be proved
-Verified 2/7 symbols. Waiting for CheckReadsTot to verify.
-Verification part 1/1 of CheckReadsTot, on line 20, verified successfully, redacted and consuming 1.0E+004 resources
-Verified 3/7 symbols. Waiting for CheckReadsParens to verify.
-Verification part 1/1 of CheckReadsParens, on line 26, verified successfully, redacted and consuming 1.0E+004 resources
-Verified 4/7 symbols. Waiting for CheckReadsLambdaGeneral to verify.
-Verification part 1/1 of CheckReadsLambdaGeneral, on line 32, verified successfully, redacted and consuming 1.9E+004 resources
-Verified 5/7 symbols. Waiting for CheckReadsLambdaPartial to verify.
-Verification part 1/1 of CheckReadsLambdaPartial, on line 38, verified successfully, redacted and consuming 1.7E+004 resources
-Verified 6/7 symbols. Waiting for CheckReadsLambdaTotal to verify.
-Verification part 1/1 of CheckReadsLambdaTotal, on line 44, verified successfully, redacted and consuming 1.5E+004 resources
+ArrowTypeOptimizations.dfy(10,2): Error: function precondition could not be proved
+ArrowTypeOptimizations.dfy(10,2): Error: insufficient reads clause to invoke function
+ArrowTypeOptimizations.dfy(16,2): Error: function precondition could not be proved
 
-Dafny program verifier finished with 5 verified, 3 errors
+Dafny program verifier finished with 17 verified, 3 errors
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressFirstSequence.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressFirstSequence.check
new file mode 100644
index 00000000000..d16ba0812c5
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressFirstSequence.check
@@ -0,0 +1,5 @@
+// CHECK-L:Verified 0/5 symbols. Waiting for Foo to verify.
+// CHECK-L:Verified 1/5 symbols. Waiting for Faz to verify.
+// CHECK-L:Verified 2/5 symbols. Waiting for Fopple to verify.
+// CHECK-L:Verified 3/5 symbols. Waiting for Burp to verify.
+// CHECK-L:Verified 4/5 symbols. Waiting for Blanc to verify.
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check
new file mode 100644
index 00000000000..2884ac1aaa9
--- /dev/null
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check
@@ -0,0 +1,12 @@
+// CHECK-L:Verification part 1/3 of Foo, on line 6, verified successfully, redacted and consuming 8.7E+002 resources
+// CHECK-L:Verification part 2/3 of Foo, on line 8, verified successfully, redacted and consuming 3.1E+003 resources
+// CHECK-L:Verification part 3/3 of Foo, on line 9, verified successfully, redacted and consuming 2.8E+003 resources
+// CHECK-L:Verification part 1/2 of Faz, on line 12, verified successfully, redacted and consuming 8.7E+002 resources
+// CHECK-L:Verification part 2/2 of Faz, on line 12, verified successfully, redacted and consuming 3.1E+003 resources
+// CHECK-L:Verification part 1/2 of Fopple, on line 14, verified successfully, redacted and consuming 8.7E+002 resources
+// CHECK-L:Verification part 2/2 of Fopple, on line 14, verified successfully, redacted and consuming 3.1E+003 resources
+// CHECK-L:Verification part 1/3 of Burp, on line 16, verified successfully, redacted and consuming 8.7E+002 resources
+// CHECK-L:Verification part 2/3 of Burp, on line 18, verified successfully, redacted and consuming 3.1E+003 resources
+// CHECK-L:Verification part 3/3 of Burp, on line 19, verified successfully, redacted and consuming 2.8E+003 resources
+// CHECK-L:Verification part 1/2 of Blanc, on line 22, verified successfully, redacted and consuming 8.7E+002 resources
+// CHECK-L:Verification part 2/2 of Blanc, on line 22, verified successfully, redacted and consuming 3.1E+003 resources
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy
index c992fcd4c28..ac8fab24ac5 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy
@@ -1,6 +1,11 @@
 // RUN: %verify --progress --cores=1 %s &> %t.raw
 // RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
-// RUN: %diff "%s.expect" "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%s"
+// CHECK-L:Verification part 1/3 of Foo, on line 10, verified successfully, redacted and consuming 8.7E+002 resources
+// CHECK-L:Verification part 2/3 of Foo, on line 11, verified successfully, redacted and consuming 3.1E+003 resources
+// CHECK-L:Verification part 3/3 of Foo, on line 12, verified successfully, redacted and consuming 2.8E+003 resources
+// CHECK-L:Verified 1/2 symbols. Waiting for Bar to verify.
+// CHECK-L:Verification part 1/1 of Bar, on line 15, verified successfully, redacted and consuming 3.1E+003 resources
 
 method {:isolate_assertions} Foo() {
   assert true;
diff --git a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy
index 90626b23cbd..2e84fdaed13 100644
--- a/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy
+++ b/Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy
@@ -1,6 +1,7 @@
 // RUN: %verify --progress --isolate-assertions --cores=1 %s > %t.raw
 // RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
-// RUN: %diff "%s.expect" "%t"
+// RUN: %OutputCheck --file-to-check %t "%S/Inputs/progressFirstSequence.check"
+// RUN: %OutputCheck --file-to-check %t "%S/Inputs/progressSecondSequence.check"
 
 method Foo() 
 {