diff options
| author |  leino <unknown> | 2015-09-20 21:51:42 -0700 |
|---|---|---|
| committer | leino <unknown> | 2015-09-20 21:51:42 -0700 |
| commit | 800885b4d7d0164803c0c2f117b78c65479283f9 (patch) | |
| tree | d5ffd8318ffeed8fa300a9e872461f38455c28ed /Test/dafny0/AssumptionVariables0.dfy.expect | |
| parent | b9319e38746bc6a2043cb7c979c4ccd4b175b86c (diff) | |
Preliminary refactoring of ghost-statement computations to after type checking
Diffstat (limited to 'Test/dafny0/AssumptionVariables0.dfy.expect')
| -rw-r--r-- | Test/dafny0/AssumptionVariables0.dfy.expect | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/Test/dafny0/AssumptionVariables0.dfy.expect b/Test/dafny0/AssumptionVariables0.dfy.expect index f2d43fe1..16572961 100644 --- a/Test/dafny0/AssumptionVariables0.dfy.expect +++ b/Test/dafny0/AssumptionVariables0.dfy.expect @@ -1,14 +1,13 @@ AssumptionVariables0.dfy(6,29): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(7,33): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a2 && <boolean expression>"
-AssumptionVariables0.dfy(9,20): Error: assumption variable must be ghost
AssumptionVariables0.dfy(9,2): Error: assumption variable must be of type 'bool'
AssumptionVariables0.dfy(15,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"
AssumptionVariables0.dfy(17,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a3 && <boolean expression>"
AssumptionVariables0.dfy(27,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(31,5): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(53,9): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
-AssumptionVariables0.dfy(57,26): Error: assumption variable must be ghost
AssumptionVariables0.dfy(61,37): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
AssumptionVariables0.dfy(61,10): Error: assumption variable must be of type 'bool'
AssumptionVariables0.dfy(69,15): Error: there may be at most one assignment to an assumption variable, the RHS of which must match the expression "a0 && <boolean expression>"
-13 resolution/type errors detected in AssumptionVariables0.dfy
+AssumptionVariables0.dfy(78,20): Error: assumption variable must be ghost
+12 resolution/type errors detected in AssumptionVariables0.dfy
|