diff options
| author |  rustanleino <unknown> | 2011-03-01 01:08:22 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2011-03-01 01:08:22 +0000 |
| commit | f9cb8c7c79c2c4a6eb921a58b56d7d207bf09b50 (patch) | |
| tree | dcf7f5e5937e952eaff52e490a21afd4ccbb23ef | |
| parent | 299109e6e38ebac40c3372adf48d06d174d92eb1 (diff) | |
Updates to Answer files from recent changes
| -rw-r--r-- | Test/dafny0/Answer | 12 | ||||
| -rw-r--r-- | Test/test15/Answer | 12 |
2 files changed, 18 insertions, 6 deletions
diff --git a/Test/dafny0/Answer b/Test/dafny0/Answer index 173970f6..018a29e2 100644 --- a/Test/dafny0/Answer +++ b/Test/dafny0/Answer @@ -504,15 +504,15 @@ Use.dfy(126,23): Error: assertion violation Execution trace:
(0,0): anon0
Use.dfy(151,12): Error: assertion violation
-Use.dfy(143,5): Related location
+Use.dfy(143,5): Related location: Related location
Execution trace:
(0,0): anon0
Use.dfy(160,12): Error: assertion violation
-Use.dfy(143,5): Related location
+Use.dfy(143,5): Related location: Related location
Execution trace:
(0,0): anon0
Use.dfy(169,12): Error: assertion violation
-Use.dfy(143,5): Related location
+Use.dfy(143,5): Related location: Related location
Execution trace:
(0,0): anon0
Use.dfy(213,19): Error: assertion violation
@@ -541,21 +541,21 @@ Execution trace: (0,0): anon3_Then
(0,0): anon2
TypeParameters.dfy(130,12): Error: assertion violation
-TypeParameters.dfy(130,28): Related location
+TypeParameters.dfy(130,28): Related location: Related location
Execution trace:
(0,0): anon0
(0,0): anon14_Then
TypeParameters.dfy(130,32): anon15_Else
(0,0): anon5
TypeParameters.dfy(132,12): Error: assertion violation
-TypeParameters.dfy(132,33): Related location
+TypeParameters.dfy(132,33): Related location: Related location
Execution trace:
(0,0): anon0
(0,0): anon17_Then
TypeParameters.dfy(132,37): anon18_Else
(0,0): anon11
TypeParameters.dfy(146,15): Error BP5005: This loop invariant might not be maintained by the loop.
-TypeParameters.dfy(146,38): Related location
+TypeParameters.dfy(146,38): Related location: Related location
Execution trace:
(0,0): anon0
TypeParameters.dfy(139,3): anon17_LoopHead
diff --git a/Test/test15/Answer b/Test/test15/Answer index f989c7bd..19f526f5 100644 --- a/Test/test15/Answer +++ b/Test/test15/Answer @@ -218,10 +218,12 @@ r -> **r m -> **m
$pow2 -> {
0 -> 1
+ else -> *22
}
tickleBool -> {
false -> true
true -> true
+ else -> *22
}
Ctor -> {
*4 -> 0
@@ -229,39 +231,49 @@ Ctor -> { *6 -> 3
*7 -> 4
*18 -> 2
+ else -> *22
}
type -> {
*8 -> *18
*9 -> *6
*10 -> *7
-2 -> *4
+ else -> *22
}
MapType0Type -> {
*6 *7 *4 -> *18
+ else -> *22
}
MapType0TypeInv2 -> {
*18 -> *4
+ else -> *22
}
MapType0TypeInv1 -> {
*18 -> *7
+ else -> *22
}
MapType0TypeInv0 -> {
*18 -> *6
+ else -> *22
}
@MV_state -> {
0 -> true
3 -> true
4 -> true
5 -> true
+ else -> *22
}
[3] -> {
*8 *9 *10 -> -2
+ else -> *22
}
U_2_int -> {
-2 -> -2
+ else -> *22
}
int_2_U -> {
-2 -> -2
+ else -> *22
}
*** STATE <initial>
Heap -> *8
|