diff options
| author |  Rustan Leino <leino@microsoft.com> | 2012-06-08 18:22:08 -0700 |
|---|---|---|
| committer | Rustan Leino <leino@microsoft.com> | 2012-06-08 18:22:08 -0700 |
| commit | b663406e442285d3774342cf5a8f1dd8b84f2755 (patch) | |
| tree | 91eede7be63ae1bfdf8a9e04d7f3cdf9f88fafa8 /Test/test15 | |
| parent | 13d31d4e91c4d15506069e73d62573cb566abbaf (diff) | |
Dafny/Boogie/BVD: made Dafny plug-in for BVD work again
Diffstat (limited to 'Test/test15')
| -rw-r--r-- | Test/test15/Answer | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/Test/test15/Answer b/Test/test15/Answer index 56c247c2..04a94759 100644 --- a/Test/test15/Answer +++ b/Test/test15/Answer @@ -144,7 +144,7 @@ type -> { T@U!val!0 -> T@T!val!4
T@U!val!1 -> T@T!val!2
T@U!val!2 -> T@T!val!3
- T@U!val!3 -> T@T!val!0
+ -2 -> T@T!val!0
else -> T@T!val!4
}
Ctor -> {
@@ -162,12 +162,12 @@ Ctor -> { 6 5 -> true
else -> true
}
-MapType0Select -> {
- T@U!val!0 T@U!val!1 T@U!val!2 -> T@U!val!3
- else -> T@U!val!3
+[3] -> {
+ T@U!val!0 T@U!val!1 T@U!val!2 -> -2
+ else -> -2
}
U_2_int -> {
- T@U!val!3 -> -2
+ -2 -> -2
else -> -2
}
MapType0TypeInv1 -> {
@@ -187,8 +187,8 @@ MapType0TypeInv0 -> { else -> T@T!val!2
}
int_2_U -> {
- -2 -> T@U!val!3
- else -> T@U!val!3
+ -2 -> -2
+ else -> -2
}
*** STATE <initial>
Heap -> T@U!val!0
|