From 7cc79726ea246593f4a903ad89b55aa0949fc915 Mon Sep 17 00:00:00 2001
From: Unknown <leino@LEINO6.redmond.corp.microsoft.com>
Date: Thu, 27 Sep 2012 15:18:47 -0700
Subject: Boogie and Dafny: adjustments to the test suite expected output (and
 a temporary hack in FloydCycleDetect.dfy to be corrected shortly)

---
 Test/test15/Answer | 120 ++++++++++++++++++++++++++++-------------------------
 1 file changed, 64 insertions(+), 56 deletions(-)

(limited to 'Test/test15')

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 3361b320..915f63e8 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -1,22 +1,24 @@
 
 -------------------- NullInModel --------------------
 *** MODEL
-%lbl%@46 -> false
-%lbl%+23 -> true
-%lbl%+36 -> true
-boolType -> T@T!val!1
+%lbl%@45 -> false
+%lbl%+24 -> true
+%lbl%+35 -> true
+boolType -> T@T!val!2
 intType -> T@T!val!0
 null -> T@U!val!0
-refType -> T@T!val!2
+realType -> T@T!val!1
+refType -> T@T!val!3
 s -> T@U!val!0
 type -> {
-  T@U!val!0 -> T@T!val!2
-  else -> T@T!val!2
+  T@U!val!0 -> T@T!val!3
+  else -> T@T!val!3
 }
 Ctor -> {
   T@T!val!0 -> 0
   T@T!val!1 -> 1
   T@T!val!2 -> 2
+  T@T!val!3 -> 3
   else -> 0
 }
 tickleBool -> {
@@ -33,15 +35,17 @@ Boogie program verifier finished with 0 verified, 1 error
 
 -------------------- IntInModel --------------------
 *** MODEL
-%lbl%@38 -> false
-%lbl%+22 -> true
-%lbl%+28 -> true
-boolType -> T@T!val!1
+%lbl%@37 -> false
+%lbl%+23 -> true
+%lbl%+27 -> true
+boolType -> T@T!val!2
 i -> 0
 intType -> T@T!val!0
+realType -> T@T!val!1
 Ctor -> {
   T@T!val!0 -> 0
   T@T!val!1 -> 1
+  T@T!val!2 -> 2
   else -> 0
 }
 tickleBool -> {
@@ -58,27 +62,29 @@ Boogie program verifier finished with 0 verified, 1 error
 
 -------------------- ModelTest --------------------
 *** MODEL
-%lbl%@181 -> false
-%lbl%+118 -> true
-%lbl%+63 -> true
-boolType -> T@T!val!1
+%lbl%@145 -> false
+%lbl%+64 -> true
+%lbl%+82 -> true
+boolType -> T@T!val!2
 i@0 -> 1
 intType -> T@T!val!0
 j@0 -> 2
 j@1 -> 3
 j@2 -> 4
 r -> T@U!val!1
-refType -> T@T!val!2
+realType -> T@T!val!1
+refType -> T@T!val!3
 s -> T@U!val!0
 type -> {
-  T@U!val!0 -> T@T!val!2
-  T@U!val!1 -> T@T!val!2
-  else -> T@T!val!2
+  T@U!val!0 -> T@T!val!3
+  T@U!val!1 -> T@T!val!3
+  else -> T@T!val!3
 }
 Ctor -> {
   T@T!val!0 -> 0
   T@T!val!1 -> 1
   T@T!val!2 -> 2
+  T@T!val!3 -> 3
   else -> 0
 }
 tickleBool -> {
@@ -114,37 +120,38 @@ Execution trace:
     CaptureState.bpl(16,5): anon4_Then
     CaptureState.bpl(24,5): anon3
 *** MODEL
-%lbl%@335 -> false
-%lbl%+111 -> true
-%lbl%+113 -> true
-%lbl%+117 -> true
-%lbl%+190 -> true
+%lbl%@291 -> false
+%lbl%+112 -> true
+%lbl%+114 -> true
+%lbl%+118 -> true
+%lbl%+146 -> true
 @MV_state_const -> 6
-boolType -> T@T!val!1
+boolType -> T@T!val!2
 F -> T@U!val!2
-FieldNameType -> T@T!val!3
+FieldNameType -> T@T!val!4
 Heap -> T@U!val!0
 intType -> T@T!val!0
 m -> **m
-m@0 -> -2
-m@2 -> -1
-m@3 -> -1
+m@0 -> -451
+m@2 -> -450
+m@3 -> -450
 r -> **r
-r@0 -> -2
-RefType -> T@T!val!2
+r@0 -> -900
+realType -> T@T!val!1
+RefType -> T@T!val!3
 this -> T@U!val!1
-x@@4 -> 797
+x@@5 -> 0
 y@@1 -> **y@@1
 int_2_U -> {
-  -2 -> -2
-  else -> -2
+  -451 -> -451
+  else -> -451
 }
 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
-  -2 -> T@T!val!0
-  else -> T@T!val!4
+  T@U!val!0 -> T@T!val!5
+  T@U!val!1 -> T@T!val!3
+  T@U!val!2 -> T@T!val!4
+  -451 -> T@T!val!0
+  else -> T@T!val!5
 }
 @MV_state -> {
   6 0 -> true
@@ -156,26 +163,27 @@ type -> {
 Ctor -> {
   T@T!val!0 -> 0
   T@T!val!1 -> 1
-  T@T!val!2 -> 3
+  T@T!val!2 -> 2
   T@T!val!3 -> 4
-  T@T!val!4 -> 2
+  T@T!val!4 -> 5
+  T@T!val!5 -> 3
   else -> 0
 }
 [3] -> {
-  T@U!val!0 T@U!val!1 T@U!val!2 -> -2
-  else -> -2
+  T@U!val!0 T@U!val!1 T@U!val!2 -> -451
+  else -> -451
 }
 U_2_int -> {
-  -2 -> -2
-  else -> -2
+  -451 -> -451
+  else -> -451
 }
 MapType0TypeInv1 -> {
-  T@T!val!4 -> T@T!val!3
-  else -> T@T!val!3
+  T@T!val!5 -> T@T!val!4
+  else -> T@T!val!4
 }
 MapType0TypeInv0 -> {
-  T@T!val!4 -> T@T!val!2
-  else -> T@T!val!2
+  T@T!val!5 -> T@T!val!3
+  else -> T@T!val!3
 }
 tickleBool -> {
   true -> true
@@ -183,17 +191,17 @@ tickleBool -> {
   else -> true
 }
 MapType0Type -> {
-  T@T!val!2 T@T!val!3 T@T!val!0 -> T@T!val!4
-  else -> T@T!val!4
+  T@T!val!3 T@T!val!4 T@T!val!0 -> T@T!val!5
+  else -> T@T!val!5
 }
 MapType0TypeInv2 -> {
-  T@T!val!4 -> T@T!val!0
+  T@T!val!5 -> T@T!val!0
   else -> T@T!val!0
 }
 *** STATE <initial>
   Heap -> T@U!val!0
   this -> T@U!val!1
-  x -> 797
+  x -> 0
   y -> **y@@1
   r -> **r
   m -> **m
@@ -201,13 +209,13 @@ MapType0TypeInv2 -> {
 *** STATE top
 *** END_STATE
 *** STATE then
-  m -> -2
+  m -> -451
 *** END_STATE
 *** STATE postUpdate0
-  m -> -1
+  m -> -450
 *** END_STATE
 *** STATE end
-  r -> -2
+  r -> -900
   m -> 7
 *** END_STATE
 *** END_MODEL
-- 
cgit v1.2.3