Fix tests

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/outOfResourceAndIsolateAssertions.check

@@ -0,0 +1,26 @@
+CHECK: Verified 0/2 symbols. Waiting for f to verify.
+CHECK: Verification part 1/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 2/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 3/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 4/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 5/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 6/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 7/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 8/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 9/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 10/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 11/11 of f, on line 5, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verified 1/2 symbols. Waiting for L to verify.
+CHECK: Verification part 1/9 of L, on line 7, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 2/9 of L, on line 9, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 3/9 of L, on line 10, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 4/9 of L, on line 10, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 5/9 of L, on line 10, ran out of resources \(time: .*, resource count: .*\)
+CHECK: Verification part 6/9 of L, on line 11, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 7/9 of L, on line 12, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 8/9 of L, on line 12, verified successfully \(time: .*, resource count: .*\)
+CHECK: Verification part 9/9 of L, on line 12, ran out of resources
+outOfResourceAndIsolateAssertions.dfy\(10,18\): Error: Verification out of resource \(L\)
+outOfResourceAndIsolateAssertions.dfy\(12,18\): Error: Verification out of resource \(L\)
+
+Dafny program verifier finished with 18 verified, 0 errors, 2 out of resource

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/Inputs/progressSecondSequence.check

@@ -1,12 +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
+// CHECK:Verification part 1/3 of Foo, on line 6, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/3 of Foo, on line 8, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 3/3 of Foo, on line 9, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/2 of Faz, on line 12, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/2 of Faz, on line 12, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/2 of Fopple, on line 14, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/2 of Fopple, on line 14, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/3 of Burp, on line 16, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/3 of Burp, on line 18, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 3/3 of Burp, on line 19, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 1/2 of Blanc, on line 22, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/2 of Blanc, on line 22, verified successfully \(time: .*, resource count: .*\)

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/isolate-assertions.dfy

@@ -1,11 +1,11 @@
-// RUN: %verify --progress --cores=1 %s &> %t.raw
-// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
+// RUN: %verify --progress --cores=1 %s &> %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
+// CHECK:Verification part 1/3 of Foo, on line 10, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 2/3 of Foo, on line 11, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verification part 3/3 of Foo, on line 12, verified successfully \(time: .*, resource count: .*\)
+// CHECK:Verified 1/2 symbols. Waiting for Bar to verify.
+// CHECK:Verification part 1/1 of Bar, on line 15, verified successfully \(time: .*, resource count: .*\)
+
 
 method {:isolate_assertions} Foo() {
  assert true;
@@ -15,4 +15,4 @@ method {:isolate_assertions} Foo() {
 method Bar() {
  assert true;
  assert true;
-}
+}

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/outOfResourceAndIsolateAssertions.dfy

@@ -1,6 +1,6 @@
-// RUN: ! %verify --isolate-assertions --cores=1 --progress "%s" &> %t.raw
-// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
-// RUN: %diff "%s.expect" %t
+// RUN: ! %verify --isolate-assertions --cores=1 --progress "%s" &> "%t"
+// RUN: %OutputCheck --file-to-check "%t" "%S/Inputs/outOfResourceAndIsolateAssertions.check"
+
 
 ghost function f(i:nat, j:nat):int {if i == 0 then 0 else f(i - 1, i * j + 1) + f(i - 1, 2 * i * j)}
 

Source/IntegrationTests/TestFiles/LitTests/LitTest/verification/progress.dfy

@@ -1,8 +1,8 @@
-// RUN: %verify --progress --isolate-assertions --cores=1 %s > %t.raw
-// RUN: %sed 's/taking \d*ms/redacted/g' %t.raw > %t
+// RUN: %verify --progress --isolate-assertions --cores=1 %s > %t
 // RUN: %OutputCheck --file-to-check %t "%S/Inputs/progressFirstSequence.check"
 // RUN: %OutputCheck --file-to-check %t "%S/Inputs/progressSecondSequence.check"
 
+
 method Foo() 
 {
  assert true;
@@ -19,4 +19,4 @@ method Burp()
  assert true;
 }
 
-method Blanc() ensures true { }
+method Blanc() ensures true { }