Chalice: Use "/smoke" for the test suite by default to ensure test quality. Update all reference outputs accordingly.

35 files changed, 184 insertions, 120 deletions

diff --git a/Chalice/tests/examples/AssociationList.output.txt b/Chalice/tests/examples/AssociationList.output.txt
index 618d878a..ce20ed93 100644
--- a/Chalice/tests/examples/AssociationList.output.txt
+++ b/Chalice/tests/examples/AssociationList.output.txt
@@ -1,6 +1,13 @@
 Verification of AssociationList.chalice using parameters="" 

 

-  19.3: The postcondition at 21.13 might not hold. Insufficient fraction at 21.13 for mu.

-  64.9: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.

-

-Boogie program verifier finished with 10 verified, 2 errors

+  19.3: The postcondition at 21.13 might not hold. Insufficient fraction at 21.13 for mu.
+  64.9: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.
+
+  75.11: The end of the if-branch is unreachable.
+  79.13: The end of the if-branch is unreachable.
+  79.13: The end of the else-branch is unreachable.
+  75.11: The end of the else-branch is unreachable.
+  64.9: The end of the while-body is unreachable.
+  60.7: The end of the else-branch is unreachable.
+
+Boogie program verifier finished with 2 errors and 6 smoke test warnings.

diff --git a/Chalice/tests/examples/BackgroundComputation.output.txt b/Chalice/tests/examples/BackgroundComputation.output.txt
index c139677a..dc1bafc1 100644
--- a/Chalice/tests/examples/BackgroundComputation.output.txt
+++ b/Chalice/tests/examples/BackgroundComputation.output.txt
@@ -1,4 +1,4 @@
 Verification of BackgroundComputation.chalice using parameters="" 

 

-

-Boogie program verifier finished with 7 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt
index 4099f78a..6ea31348 100644
--- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt
+++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack.output.txt
@@ -1,4 +1,11 @@
 Verification of CopyLessMessagePassing-with-ack.chalice using parameters="" 

 

-

-Boogie program verifier finished with 11 verified, 0 errors

+
+  48.22: Assumption might introduce a contradiction.
+  48.7: The end of the if-branch is unreachable.
+  69.22: Assumption might introduce a contradiction.
+  69.7: The end of the if-branch is unreachable.
+  72.21: Assumption might introduce a contradiction.
+  72.5: The end of the if-branch is unreachable.
+
+Boogie program verifier finished with 0 errors and 6 smoke test warnings.

diff --git a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt
index 6ba69de5..7f53cfb3 100644
--- a/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt
+++ b/Chalice/tests/examples/CopyLessMessagePassing-with-ack2.output.txt
@@ -1,4 +1,9 @@
 Verification of CopyLessMessagePassing-with-ack2.chalice using parameters="" 

 

-

-Boogie program verifier finished with 12 verified, 0 errors

+
+  50.23: Assumption might introduce a contradiction.
+  50.7: The end of the if-branch is unreachable.
+  65.27: Assumption might introduce a contradiction.
+  65.7: The end of the if-branch is unreachable.
+
+Boogie program verifier finished with 0 errors and 4 smoke test warnings.

diff --git a/Chalice/tests/examples/CopyLessMessagePassing.output.txt b/Chalice/tests/examples/CopyLessMessagePassing.output.txt
index 859c9998..26784a86 100644
--- a/Chalice/tests/examples/CopyLessMessagePassing.output.txt
+++ b/Chalice/tests/examples/CopyLessMessagePassing.output.txt
@@ -1,4 +1,4 @@
 Verification of CopyLessMessagePassing.chalice using parameters="" 

 

-

-Boogie program verifier finished with 11 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/FictionallyDisjointCells.output.txt b/Chalice/tests/examples/FictionallyDisjointCells.output.txt
index 1dc7a7b1..9bc4fb68 100644
--- a/Chalice/tests/examples/FictionallyDisjointCells.output.txt
+++ b/Chalice/tests/examples/FictionallyDisjointCells.output.txt
@@ -1,4 +1,4 @@
 Verification of FictionallyDisjointCells.chalice using parameters="" 

 

-

-Boogie program verifier finished with 12 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/ForkJoin.output.txt b/Chalice/tests/examples/ForkJoin.output.txt
index ed2abbda..b1371da7 100644
--- a/Chalice/tests/examples/ForkJoin.output.txt
+++ b/Chalice/tests/examples/ForkJoin.output.txt
@@ -1,4 +1,4 @@
 Verification of ForkJoin.chalice using parameters="" 

 

-

-Boogie program verifier finished with 18 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/HandOverHand.output.txt b/Chalice/tests/examples/HandOverHand.output.txt
index de7ab98c..5d32ad2e 100644
--- a/Chalice/tests/examples/HandOverHand.output.txt
+++ b/Chalice/tests/examples/HandOverHand.output.txt
@@ -1,4 +1,4 @@
 Verification of HandOverHand.chalice using parameters="" 

 

-

-Boogie program verifier finished with 10 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/ImplicitLocals.output.txt b/Chalice/tests/examples/ImplicitLocals.output.txt
index 4d7b08b1..db26bba6 100644
--- a/Chalice/tests/examples/ImplicitLocals.output.txt
+++ b/Chalice/tests/examples/ImplicitLocals.output.txt
@@ -1,4 +1,4 @@
 Verification of ImplicitLocals.chalice using parameters="" 

 

-

-Boogie program verifier finished with 8 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/LoopLockChange.output.txt b/Chalice/tests/examples/LoopLockChange.output.txt
index 7a03627f..50b446ec 100644
--- a/Chalice/tests/examples/LoopLockChange.output.txt
+++ b/Chalice/tests/examples/LoopLockChange.output.txt
@@ -1,7 +1,12 @@
 Verification of LoopLockChange.chalice using parameters="" 

 

-  10.5: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.

-  35.5: The loop might lock/unlock more than the lockchange clause allows.

-  65.5: The loop might lock/unlock more than the lockchange clause allows.

-

-Boogie program verifier finished with 14 verified, 3 errors

+  10.5: Method execution before loop might lock/unlock more than allowed by lockchange clause of loop.
+  35.5: The loop might lock/unlock more than the lockchange clause allows.
+  65.5: The loop might lock/unlock more than the lockchange clause allows.
+
+  10.5: The end of the while-body is unreachable.
+  3.3: The end of method Test0 is unreachable.
+  75.5: Assumption might introduce a contradiction.
+  59.3: The end of method Test4 is unreachable.
+
+Boogie program verifier finished with 3 errors and 4 smoke test warnings.

diff --git a/Chalice/tests/examples/OwickiGries.output.txt b/Chalice/tests/examples/OwickiGries.output.txt
index a56e7442..3a9a215b 100644
--- a/Chalice/tests/examples/OwickiGries.output.txt
+++ b/Chalice/tests/examples/OwickiGries.output.txt
@@ -1,4 +1,4 @@
 Verification of OwickiGries.chalice using parameters="" 

 

-

-Boogie program verifier finished with 5 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/PetersonsAlgorithm.output.txt b/Chalice/tests/examples/PetersonsAlgorithm.output.txt
index 5bc49aaa..185dc8e1 100644
--- a/Chalice/tests/examples/PetersonsAlgorithm.output.txt
+++ b/Chalice/tests/examples/PetersonsAlgorithm.output.txt
@@ -1,4 +1,8 @@
 Verification of PetersonsAlgorithm.chalice using parameters="" 

 

-

-Boogie program verifier finished with 7 verified, 0 errors

+
+  15.3: The end of method Main is unreachable.
+  30.3: The end of method Process0 is unreachable.
+  55.3: The end of method Process1 is unreachable.
+
+Boogie program verifier finished with 0 errors and 3 smoke test warnings.

diff --git a/Chalice/tests/examples/ProdConsChannel.output.txt b/Chalice/tests/examples/ProdConsChannel.output.txt
index de5e8467..fc436ea7 100644
--- a/Chalice/tests/examples/ProdConsChannel.output.txt
+++ b/Chalice/tests/examples/ProdConsChannel.output.txt
@@ -1,8 +1,10 @@
 Verification of ProdConsChannel.chalice using parameters="" 

 

-  47.3: Method body is not allowed to leave any debt.

-  61.3: Method body is not allowed to leave any debt.

-  85.20: Location might not be readable.

-  123.7: Assertion might not hold. The expression at 123.14 might not evaluate to true.

-

-Boogie program verifier finished with 19 verified, 4 errors

+  47.3: Method body is not allowed to leave any debt.
+  61.3: Method body is not allowed to leave any debt.
+  85.20: Location might not be readable.
+  123.7: Assertion might not hold. The expression at 123.14 might not evaluate to true.
+
+  80.5: The end of the while-body is unreachable.
+
+Boogie program verifier finished with 4 errors and 1 smoke test warnings.

diff --git a/Chalice/tests/examples/RockBand-automagic.output.txt b/Chalice/tests/examples/RockBand-automagic.output.txt
index efff95e2..2e62b457 100644
--- a/Chalice/tests/examples/RockBand-automagic.output.txt
+++ b/Chalice/tests/examples/RockBand-automagic.output.txt
@@ -1,4 +1,4 @@
 Verification of RockBand-automagic.chalice using parameters="-checkLeaks -defaults -autoFold -autoMagic" 

 

-

-Boogie program verifier finished with 35 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/RockBand.output.txt b/Chalice/tests/examples/RockBand.output.txt
index a52b021b..94f92a6e 100644
--- a/Chalice/tests/examples/RockBand.output.txt
+++ b/Chalice/tests/examples/RockBand.output.txt
@@ -1,4 +1,4 @@
 Verification of RockBand.chalice using parameters="-checkLeaks -defaults -autoFold" 

 

-

-Boogie program verifier finished with 35 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/Sieve.output.txt b/Chalice/tests/examples/Sieve.output.txt
index 93271d87..3e5117d3 100644
--- a/Chalice/tests/examples/Sieve.output.txt
+++ b/Chalice/tests/examples/Sieve.output.txt
@@ -1,4 +1,4 @@
 Verification of Sieve.chalice using parameters="" 

 

-

-Boogie program verifier finished with 11 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/SmokeTestTest.chalice b/Chalice/tests/examples/SmokeTestTest.chalice
index a9bbf197..e5384955 100644
--- a/Chalice/tests/examples/SmokeTestTest.chalice
+++ b/Chalice/tests/examples/SmokeTestTest.chalice
@@ -4,11 +4,11 @@ class Cell {
   var f: int;

   

   method a1()

-    requires false

+    requires false // SMOKE: precondition is false

   {}

   

   method a2()

-    requires acc(this.f,-2)

+    requires acc(this.f,-2) // SMOKE: precondition is equivalent to false

   {}

   

   method a3()

@@ -23,7 +23,7 @@ class Cell {
     requires acc(this.f)

   {

     if (false) {

-      this.f := 0;

+      this.f := 0; // SMOKE: unreachable

     }

   }

   

@@ -39,7 +39,7 @@ class Cell {
     requires acc(this.f)

   {

     if (false) {

-      this.f := 0;

+      this.f := 0; // SMOKE: unreachable

     } else {

       this.f := 1;

     }

@@ -48,18 +48,22 @@ class Cell {
   method a7(i: int, j: int)

     requires i != j;

   {

-    assume i == j;

+    assume i == j; // SMOKE: introduces contradiction

   }

   

   method a8()

     requires acc(this.f)

   {

-    while (true) {

+    while (true)

+      invariant acc(this.f)

+    {

       this.f := this.f + 1

     }

+    // SMOKE: unreachable, loop does not terminate

   }

   

   method a9()

+    requires acc(this.f)

   {

     call a8()

   }

@@ -70,7 +74,7 @@ class Cell {
     if (true) {

       this.f := 0;

     } else {

-      this.f := 1;

+      this.f := 1; // SMOKE: unreachable

     }

   }

 }

diff --git a/Chalice/tests/examples/SmokeTestTest.output.txt b/Chalice/tests/examples/SmokeTestTest.output.txt
index 1fe23f64..2bfce65f 100644
--- a/Chalice/tests/examples/SmokeTestTest.output.txt
+++ b/Chalice/tests/examples/SmokeTestTest.output.txt
@@ -1,5 +1,6 @@
 Verification of SmokeTestTest.chalice using parameters="-smoke" 

 

+
   6.3: Precondition of method a1 is equivalent to false.
   6.3: The end of method a1 is unreachable.
   10.3: Precondition of method a2 is equivalent to false.
@@ -9,7 +10,6 @@ Verification of SmokeTestTest.chalice using parameters="-smoke"
   51.5: Assumption might introduce a contradiction.
   48.3: The end of method a7 is unreachable.
   54.3: The end of method a8 is unreachable.
-  70.5: The end of the else-branch is unreachable.
+  74.5: The end of the else-branch is unreachable.
 
-Smoke testing finished with 3 verified, 10 warnings
-

+Boogie program verifier finished with 0 errors and 10 smoke test warnings.

diff --git a/Chalice/tests/examples/Solver.output.txt b/Chalice/tests/examples/Solver.output.txt
index e88f63d9..1ec04d27 100644
--- a/Chalice/tests/examples/Solver.output.txt
+++ b/Chalice/tests/examples/Solver.output.txt
@@ -1,4 +1,4 @@
 Verification of Solver.chalice using parameters="" 

 

-

-Boogie program verifier finished with 10 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/TreeOfWorker.output.txt b/Chalice/tests/examples/TreeOfWorker.output.txt
index 4dc67e3c..13932da9 100644
--- a/Chalice/tests/examples/TreeOfWorker.output.txt
+++ b/Chalice/tests/examples/TreeOfWorker.output.txt
@@ -1,4 +1,4 @@
 Verification of TreeOfWorker.chalice using parameters="" 

 

-

-Boogie program verifier finished with 5 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/UnboundedThreads.output.txt b/Chalice/tests/examples/UnboundedThreads.output.txt
index efd70a6d..ccb4e93c 100644
--- a/Chalice/tests/examples/UnboundedThreads.output.txt
+++ b/Chalice/tests/examples/UnboundedThreads.output.txt
@@ -1,5 +1,5 @@
 Verification of UnboundedThreads.chalice using parameters="" 

 

-  40.17: The loop invariant at 40.17 might not be preserved by the loop. Insufficient epsilons at 40.27  for C.f.

-

-Boogie program verifier finished with 6 verified, 1 error

+  40.17: The loop invariant at 40.17 might not be preserved by the loop. Insufficient epsilons at 40.27  for C.f.
+
+Boogie program verifier finished with 1 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/cell-defaults.output.txt b/Chalice/tests/examples/cell-defaults.output.txt
index 0f7a3b80..31b4223f 100644
--- a/Chalice/tests/examples/cell-defaults.output.txt
+++ b/Chalice/tests/examples/cell-defaults.output.txt
@@ -1,7 +1,9 @@
 Verification of cell-defaults.chalice using parameters="-defaults -autoFold -autoMagic" 

 

-  97.5: The heap of the callee might not be strictly smaller than the heap of the caller.

-  103.5: The heap of the callee might not be strictly smaller than the heap of the caller.

-  132.5: Assertion might not hold. Insufficient fraction at 132.12 for Cell.valid.

-

-Boogie program verifier finished with 29 verified, 3 errors

+  97.5: The heap of the callee might not be strictly smaller than the heap of the caller.
+  103.5: The heap of the callee might not be strictly smaller than the heap of the caller.
+  132.5: Assertion might not hold. Insufficient fraction at 132.12 for Cell.valid.
+
+  125.3: The end of method main2 is unreachable.
+
+Boogie program verifier finished with 3 errors and 1 smoke test warnings.

diff --git a/Chalice/tests/examples/cell.output.txt b/Chalice/tests/examples/cell.output.txt
index 2c6c617d..075cbcf5 100644
--- a/Chalice/tests/examples/cell.output.txt
+++ b/Chalice/tests/examples/cell.output.txt
@@ -1,5 +1,7 @@
 Verification of cell.chalice using parameters="" 

 

-  142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.

-

-Boogie program verifier finished with 31 verified, 1 error

+  142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.
+
+  135.3: The end of method main2 is unreachable.
+
+Boogie program verifier finished with 1 errors and 1 smoke test warnings.

diff --git a/Chalice/tests/examples/counter.output.txt b/Chalice/tests/examples/counter.output.txt
index 961b1413..69f93f12 100644
--- a/Chalice/tests/examples/counter.output.txt
+++ b/Chalice/tests/examples/counter.output.txt
@@ -1,10 +1,16 @@
 Verification of counter.chalice using parameters="" 

 

-  69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.

-  80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true.

-  119.5: The target of the release statement might not be locked by the current thread.

-  128.7: The mu field of the target of the acquire statement might not be above waitlevel.

-  136.7: The mu field of the target of the acquire statement might not be above waitlevel.

-  145.5: The target of the release statement might not be locked by the current thread.

-

-Boogie program verifier finished with 24 verified, 6 errors

+  69.5: Monitor invariant might hot hold. The expression at 4.27 might not evaluate to true.
+  80.5: Assertion might not hold. The expression at 80.12 might not evaluate to true.
+  119.5: The target of the release statement might not be locked by the current thread.
+  128.7: The mu field of the target of the acquire statement might not be above waitlevel.
+  136.7: The mu field of the target of the acquire statement might not be above waitlevel.
+  145.5: The target of the release statement might not be locked by the current thread.
+
+  62.3: The end of method main4 is unreachable.
+  116.3: The end of method nestedBad0 is unreachable.
+  124.3: The end of method nestedBad1 is unreachable.
+  132.3: The end of method nestedBad2 is unreachable.
+  141.3: The end of method nestedBad3 is unreachable.
+
+Boogie program verifier finished with 6 errors and 5 smoke test warnings.

diff --git a/Chalice/tests/examples/dining-philosophers.output.txt b/Chalice/tests/examples/dining-philosophers.output.txt
index 651bd638..9d17fd1f 100644
--- a/Chalice/tests/examples/dining-philosophers.output.txt
+++ b/Chalice/tests/examples/dining-philosophers.output.txt
@@ -1,4 +1,6 @@
 Verification of dining-philosophers.chalice using parameters="" 

 

-

-Boogie program verifier finished with 12 verified, 0 errors

+
+  16.3: The end of method run is unreachable.
+
+Boogie program verifier finished with 0 errors and 1 smoke test warnings.

diff --git a/Chalice/tests/examples/iterator.output.txt b/Chalice/tests/examples/iterator.output.txt
index de361b94..a33f44db 100644
--- a/Chalice/tests/examples/iterator.output.txt
+++ b/Chalice/tests/examples/iterator.output.txt
@@ -1,4 +1,4 @@
 Verification of iterator.chalice using parameters="" 

 

-

-Boogie program verifier finished with 22 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/iterator2.output.txt b/Chalice/tests/examples/iterator2.output.txt
index af837e6f..02a7f02d 100644
--- a/Chalice/tests/examples/iterator2.output.txt
+++ b/Chalice/tests/examples/iterator2.output.txt
@@ -1,4 +1,4 @@
 Verification of iterator2.chalice using parameters="" 

 

-

-Boogie program verifier finished with 21 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/linkedlist.output.txt b/Chalice/tests/examples/linkedlist.output.txt
index 65f03446..ce5b5844 100644
--- a/Chalice/tests/examples/linkedlist.output.txt
+++ b/Chalice/tests/examples/linkedlist.output.txt
@@ -1,5 +1,5 @@
 Verification of linkedlist.chalice using parameters="" 

 

-  49.39: Precondition at 47.14 might not hold. The expression at 47.31 might not evaluate to true.

-

-Boogie program verifier finished with 9 verified, 1 error

+  49.39: Precondition at 47.14 might not hold. The expression at 47.31 might not evaluate to true.
+
+Boogie program verifier finished with 1 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/producer-consumer.output.txt b/Chalice/tests/examples/producer-consumer.output.txt
index b21044bb..9d408b7d 100644
--- a/Chalice/tests/examples/producer-consumer.output.txt
+++ b/Chalice/tests/examples/producer-consumer.output.txt
@@ -1,4 +1,7 @@
 Verification of producer-consumer.chalice using parameters="" 

 

-

-Boogie program verifier finished with 36 verified, 0 errors

+
+  36.3: The end of method run is unreachable.
+  77.3: The end of method run is unreachable.
+
+Boogie program verifier finished with 0 errors and 2 smoke test warnings.

diff --git a/Chalice/tests/examples/prog1.output.txt b/Chalice/tests/examples/prog1.output.txt
index 61938bf7..3b80f8a8 100644
--- a/Chalice/tests/examples/prog1.output.txt
+++ b/Chalice/tests/examples/prog1.output.txt
@@ -1,11 +1,18 @@
 Verification of prog1.chalice using parameters="" 

 

-  9.10: Location might not be readable.

-  25.5: Location might not be writable

-  33.14: Location might not be readable.

-  42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true.

-  60.5: Location might not be writable

-  76.5: The target of the unshare statement might not be shared.

-  84.5: The target of the unshare statement might not be shared.

-

-Boogie program verifier finished with 16 verified, 7 errors

+  9.10: Location might not be readable.
+  25.5: Location might not be writable
+  33.14: Location might not be readable.
+  42.5: Monitor invariant might hot hold. The expression at 5.23 might not evaluate to true.
+  60.5: Location might not be writable
+  76.5: The target of the unshare statement might not be shared.
+  84.5: The target of the unshare statement might not be shared.
+
+  7.3: The end of method seq0 is unreachable.
+  21.3: The end of method seq3 is unreachable.
+  28.3: The end of method main0 is unreachable.
+  53.3: The end of method main3 is unreachable.
+  73.3: The end of method main5 is unreachable.
+  78.3: The end of method main6 is unreachable.
+
+Boogie program verifier finished with 7 errors and 6 smoke test warnings.

diff --git a/Chalice/tests/examples/prog2.output.txt b/Chalice/tests/examples/prog2.output.txt
index b3ea3e93..3d08e54c 100644
--- a/Chalice/tests/examples/prog2.output.txt
+++ b/Chalice/tests/examples/prog2.output.txt
@@ -1,8 +1,12 @@
 Verification of prog2.chalice using parameters="" 

 

-  24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true.

-  31.13: Location might not be readable.

-  73.5: Const variable can be assigned to only once.

-  78.5: Assertion might not hold. The expression at 78.12 might not evaluate to true.

-

-Boogie program verifier finished with 24 verified, 4 errors

+  24.5: Assertion might not hold. The expression at 24.12 might not evaluate to true.
+  31.13: Location might not be readable.
+  73.5: Const variable can be assigned to only once.
+  78.5: Assertion might not hold. The expression at 78.12 might not evaluate to true.
+
+  20.3: The end of method Caller1 is unreachable.
+  35.3: The end of method Caller2 is unreachable.
+  70.3: The end of method M2 is unreachable.
+
+Boogie program verifier finished with 4 errors and 3 smoke test warnings.

diff --git a/Chalice/tests/examples/prog3.output.txt b/Chalice/tests/examples/prog3.output.txt
index 82eeab18..729d78fe 100644
--- a/Chalice/tests/examples/prog3.output.txt
+++ b/Chalice/tests/examples/prog3.output.txt
@@ -1,8 +1,10 @@
 Verification of prog3.chalice using parameters="" 

 

-  76.3: The postcondition at 77.13 might not hold. The expression at 77.13 might not evaluate to true.

-  76.3: Method might lock/unlock more than allowed.

-  191.5: The precondition at 182.14 might not hold. Insufficient epsilons at 182.14  for ReadSharing.x.

-  202.3: The postcondition at 204.13 might not hold. Insufficient epsilons at 204.13  for ReadSharing.x.

-

-Boogie program verifier finished with 51 verified, 4 errors

+  76.3: The postcondition at 77.13 might not hold. The expression at 77.13 might not evaluate to true.
+  76.3: Method might lock/unlock more than allowed.
+  191.5: The precondition at 182.14 might not hold. Insufficient epsilons at 182.14  for ReadSharing.x.
+  202.3: The postcondition at 204.13 might not hold. Insufficient epsilons at 204.13  for ReadSharing.x.
+
+  187.3: The end of method Divulge is unreachable.
+
+Boogie program verifier finished with 4 errors and 1 smoke test warnings.

diff --git a/Chalice/tests/examples/prog4.output.txt b/Chalice/tests/examples/prog4.output.txt
index 62197afb..db9af8c2 100644
--- a/Chalice/tests/examples/prog4.output.txt
+++ b/Chalice/tests/examples/prog4.output.txt
@@ -1,11 +1,13 @@
 Verification of prog4.chalice using parameters="" 

 

-  5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.

-  17.7: The target of the release statement might not be locked by the current thread.

-  17.7: Release might fail because the current thread might hold the read lock.

-  30.7: The target of the release statement might not be locked by the current thread.

-  30.7: Release might fail because the current thread might hold the read lock.

-  34.5: The target of the release statement might not be locked by the current thread.

-  34.5: Release might fail because the current thread might hold the read lock.

-

-Boogie program verifier finished with 6 verified, 7 errors

+  5.5: Assertion might not hold. The expression at 5.12 might not evaluate to true.
+  17.7: The target of the release statement might not be locked by the current thread.
+  17.7: Release might fail because the current thread might hold the read lock.
+  30.7: The target of the release statement might not be locked by the current thread.
+  30.7: Release might fail because the current thread might hold the read lock.
+  34.5: The target of the release statement might not be locked by the current thread.
+  34.5: Release might fail because the current thread might hold the read lock.
+
+  2.3: The end of method M is unreachable.
+
+Boogie program verifier finished with 7 errors and 1 smoke test warnings.

diff --git a/Chalice/tests/examples/quantifiers.output.txt b/Chalice/tests/examples/quantifiers.output.txt
index efae2ed6..2f325c42 100644
--- a/Chalice/tests/examples/quantifiers.output.txt
+++ b/Chalice/tests/examples/quantifiers.output.txt
@@ -1,5 +1,5 @@
 Verification of quantifiers.chalice using parameters="" 

 

-  57.29: The heap of the callee might not be strictly smaller than the heap of the caller.

-

-Boogie program verifier finished with 11 verified, 1 error

+  57.29: The heap of the callee might not be strictly smaller than the heap of the caller.
+
+Boogie program verifier finished with 1 errors and 0 smoke test warnings.

diff --git a/Chalice/tests/examples/swap.output.txt b/Chalice/tests/examples/swap.output.txt
index 70bac3a2..8cd3bb7c 100644
--- a/Chalice/tests/examples/swap.output.txt
+++ b/Chalice/tests/examples/swap.output.txt
@@ -1,4 +1,4 @@
 Verification of swap.chalice using parameters="" 

 

-

-Boogie program verifier finished with 5 verified, 0 errors

+
+Boogie program verifier finished with 0 errors and 0 smoke test warnings.