From c9dfa023ddcc6ea1ff3b8f7598f87bd200ab6c9e Mon Sep 17 00:00:00 2001
From: rustanleino <unknown>
Date: Tue, 2 Nov 2010 23:40:03 +0000
Subject: ModelViewer: * map back values introduced by bool_2_U and int_2_U *
 map back internal names for select/store to [n] and [n:=], where n is the
 arity of the map * added /break switch to ModelViewer * display more things
 (including sequences) in Dafny provider

---
 Test/test15/Answer | 10 +++++-----
 1 file changed, 5 insertions(+), 5 deletions(-)

(limited to 'Test/test15')

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 8f2fbaf3..4d0b3bad 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -234,7 +234,7 @@ type -> {
   *8 -> *18
   *9 -> *6
   *10 -> *7
-  *20 -> *4
+  -2 -> *4
 }
 MapType0Type -> {
   *6 *7 *4 -> *18
@@ -254,14 +254,14 @@ MapType0TypeInv0 -> {
   2 -> true
   5 -> true
 }
-MapType0Select -> {
-  *8 *9 *10 -> *20
+[3] -> {
+  *8 *9 *10 -> -2
 }
 U_2_int -> {
-  *20 -> -2
+  -2 -> -2
 }
 int_2_U -> {
-  -2 -> *20
+  -2 -> -2
 }
 *** STATE <initial>
   Heap -> *8
-- 
cgit v1.2.3