start 
------ Running regression test cell.chalice 
  142.5: Assertion might not hold. Insufficient fraction at 142.12 for Cell.valid.

Boogie program verifier finished with 31 verified, 1 error
------ Running regression test counter.chalice 
  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
------ Running regression test dining-philosophers.chalice 

Boogie program verifier finished with 12 verified, 0 errors
------ Running regression test ForkJoin.chalice 

Boogie program verifier finished with 18 verified, 0 errors
------ Running regression test HandOverHand.chalice 

Boogie program verifier finished with 10 verified, 0 errors
------ Running regression test iterator.chalice 

Boogie program verifier finished with 22 verified, 0 errors
------ Running regression test iterator2.chalice 

Boogie program verifier finished with 21 verified, 0 errors
------ Running regression test producer-consumer.chalice 

Boogie program verifier finished with 36 verified, 0 errors
------ Running regression test prog0.chalice 
The program did not typecheck.
3.17: undeclared member a in class C
3.37: undeclared member a in class C
3.41: undeclared member a in class C
3.12: assert statement requires a boolean expression (found int)
4.5: undeclared member a in class C
4.10: undeclared member a in class C
5.5: undeclared member b in class C
5.10: undeclared member a in class C
5.14: undeclared member b in class C
5.18: undeclared member c in class C
5.26: undeclared member d in class C
6.5: undeclared member b in class C
6.14: undeclared member a in class C
6.18: undeclared member b in class C
6.23: undeclared member c in class C
6.32: undeclared member d in class C
7.5: undeclared member c in class C
7.10: undeclared member a in class C
7.15: undeclared member b in class C
7.20: undeclared member c in class C
7.29: undeclared member d in class C
8.13: undeclared member X in class C
8.19: undeclared member Y in class C
8.13: incorrect type of ==> LHS (expected bool, found int)
8.19: incorrect type of ==> RHS (expected bool, found int)
8.26: undeclared member Z in class C
8.26: incorrect type of ==> RHS (expected bool, found int)
8.33: undeclared member A in class C
8.39: undeclared member B in class C
8.45: undeclared member C in class C
8.39: incorrect type of ==> LHS (expected bool, found int)
8.45: incorrect type of ==> RHS (expected bool, found int)
8.33: incorrect type of ==> LHS (expected bool, found int)
9.12: undeclared member A in class C
9.17: undeclared member B in class C
9.12: incorrect type of && LHS (expected bool, found int)
9.17: incorrect type of && RHS (expected bool, found int)
9.23: undeclared member C in class C
9.28: undeclared member D in class C
9.23: incorrect type of || LHS (expected bool, found int)
9.28: incorrect type of || RHS (expected bool, found int)
9.33: undeclared member E in class C
9.33: incorrect type of || RHS (expected bool, found int)
9.39: undeclared member F in class C
9.39: incorrect type of && RHS (expected bool, found int)
11.21: undeclared member f in class int
11.21: undeclared member g in class int
11.21: undeclared member h in class int
<undefined position>: not-expression requires boolean operand
<undefined position>: incorrect type of + RHS (expected int, found bool)
11.33: not-expression requires boolean operand
11.33: undeclared member f in class bool
11.43: undeclared member f in class int
11.42: not-expression requires boolean operand
11.42: incorrect type of + RHS (expected int, found bool)
13.5: type mismatch in assignment, lhs=int rhs=D
14.5: undeclared member o in class C
14.5: undeclared member f in class int
15.6: undeclared member a in class C
15.10: undeclared member b in class C
15.5: undeclared member y in class int
15.18: undefined class or channel T used in new expression
16.19: undeclared member O in class C
16.14: == requires operands of the same type, found int and bool
16.31: undeclared member O in class C
16.13: != requires operands of the same type, found bool and int
16.13: object in reorder statement must be of a reference type (found bool)
16.41: undeclared member a in class C
16.41: install bound must be of a reference type or Mu type (found int)
16.43: undeclared member b in class C
16.43: install bound must be of a reference type or Mu type (found int)
16.45: undeclared member c in class C
16.45: install bound must be of a reference type or Mu type (found int)
16.51: install bound must be of a reference type or Mu type (found int)
16.53: install bound must be of a reference type or Mu type (found int)
17.13: undeclared member X in class C
17.19: undeclared member Y in class C
17.13: incorrect type of ==> LHS (expected bool, found int)
17.19: incorrect type of ==> RHS (expected bool, found int)
17.13: object in reorder statement must be of a reference type (found bool)
17.27: install bound must be of a reference type or Mu type (found int)
18.13: undeclared member o in class C
18.13: undeclared member f in class int
18.13: object in reorder statement must be of a reference type (found int)
19.11: undeclared member o in class C
19.11: object in share statement must be of a reference type (found int)
20.13: undeclared member o in class C
20.13: object in unshare statement must be of a reference type (found int)
21.13: undeclared member o in class C
21.13: object in acquire statement must be of a reference type (found int)
22.13: undeclared member o in class C
22.13: object in release statement must be of a reference type (found int)
23.16: undeclared member o in class C
23.16: object in rd acquire statement must be of a reference type (found int)
24.16: undeclared member o in class C
24.16: object in rd release statement must be of a reference type (found int)
25.15: undeclared member o in class C
25.15: object in downgrade statement must be of a reference type (found int)
27.17: undeclared member o in class C
27.5: call of undeclared member m in class int
27.10: wrong token type
29.12: rd expression is allowed only in positive predicate contexts
29.15: undeclared member x in class C
29.20: acc expression is allowed only in positive predicate contexts
29.24: undeclared member y in class C
29.12: incorrect type of + LHS (expected int, found bool)
29.20: incorrect type of + RHS (expected int, found bool)
29.29: acc expression is allowed only in positive predicate contexts
29.33: undeclared member z in class C
29.29: incorrect type of + RHS (expected int, found bool)
29.51: undeclared member k in class C
29.57: undeclared member f in class null
29.12: assert statement requires a boolean expression (found int)
30.10: undeclared member f in class C
31.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)
32.5: wrong number of actual in-parameters in call to C.m (3 instead of 0)
33.19: undeclared member o in class C
33.5: call of undeclared member m in class int
34.5: wrong number of actual in-parameters in call to C.m (1 instead of 0)
34.5: wrong number of actual out-parameters in call to C.m (1 instead of 0)
35.13: undeclared member o in class C
35.13: object in reorder statement must be of a reference type (found int)
58.17: undeclared member sqrt2 in class C
58.25: undeclared member sqrt2 in class C
62.17: undeclared member s in class C
62.5: call of undeclared member M in class int
82.5: call of undeclared member MyMethodX in class ImplicitC
83.12: undefined local variable a
83.16: undefined local variable b
83.16: undeclared member k in class int
88.13: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)
88.13: duplicate actual out-parameter: a
89.16: undeclared member b in class ImplicitC
89.16: undeclared member k in class int
96.21: undeclared member chX in class ImplicitC
96.5: receive expression (which has type int) does not denote a channel
97.12: undefined local variable a
97.16: undefined local variable b
97.16: undeclared member k in class int
104.16: the type of the formal argument is not assignable to the actual parameter (expected: ImplicitC, found: int)
104.16: duplicate actual out-parameter: a
105.16: undeclared member b in class ImplicitC
105.16: undeclared member k in class int
------ Running regression test prog1.chalice 
  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
------ Running regression test prog2.chalice 
  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
------ Running regression test prog3.chalice 
  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
------ Running regression test prog4.chalice 
  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
------ Running regression test ImplicitLocals.chalice 

Boogie program verifier finished with 8 verified, 0 errors
------ Running regression test RockBand.chalice 
  27.3: The postcondition at 29.13 might not hold. Insufficient fraction at 29.13 for RockBand.Valid.
  41.10: Location might not be readable.
  50.5: Location might not be writable
  58.3: The postcondition at 60.13 might not hold. Insufficient fraction at 60.13 for Guitar.Valid.
  77.3: The postcondition at 79.13 might not hold. Insufficient fraction at 79.13 for Vocalist.Valid.
  96.3: The postcondition at 98.13 might not hold. Insufficient fraction at 98.13 for Organ.Valid.

Boogie program verifier finished with 29 verified, 6 errors
------ Running regression test swap.chalice 

Boogie program verifier finished with 5 verified, 0 errors
------ Running regression test OwickiGries.chalice 

Boogie program verifier finished with 5 verified, 0 errors
------ Running regression test ProdConsChannel.chalice 
  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
------ Running regression test LoopLockChange.chalice 
  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
------ Running regression test PetersonsAlgorithm.chalice 

Boogie program verifier finished with 7 verified, 0 errors
------ Running regression test cell-defaults.chalice 
  96.5: The heap of the callee might not be strictly smaller than the heap of the caller.
  102.5: The heap of the callee might not be strictly smaller than the heap of the caller.
  131.5: Assertion might not hold. Automatic fold might fail. Insufficient fraction at 42.5 for Cell.x.

Boogie program verifier finished with 29 verified, 3 errors
------ Running regression test RockBand-automagic.chalice 

Boogie program verifier finished with 35 verified, 0 errors