From b663406e442285d3774342cf5a8f1dd8b84f2755 Mon Sep 17 00:00:00 2001
From: Rustan Leino <leino@microsoft.com>
Date: Fri, 8 Jun 2012 18:22:08 -0700
Subject: Dafny/Boogie/BVD: made Dafny plug-in for BVD work again

---
 Test/test15/Answer | 14 +++++++-------
 1 file changed, 7 insertions(+), 7 deletions(-)

(limited to 'Test/test15')

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
-- 
cgit v1.2.3