diff options
| author |  rustanleino <unknown> | 2010-11-02 23:40:03 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2010-11-02 23:40:03 +0000 |
| commit | c9dfa023ddcc6ea1ff3b8f7598f87bd200ab6c9e (patch) | |
| tree | b703d03fe15666baa61d0d442f4db8ecabf1a66c /Test/test15 | |
| parent | 2c5f456402ec377ff77bb988bad978837fd372ed (diff) | |
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
Diffstat (limited to 'Test/test15')
| -rw-r--r-- | Test/test15/Answer | 10 |
1 files changed, 5 insertions, 5 deletions
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
|