summaryrefslogtreecommitdiff
path: root/Test/test15
diff options
context:
space:
mode:
authorGravatar Rustan Leino <leino@microsoft.com>2012-08-21 00:24:08 -0700
committerGravatar Rustan Leino <leino@microsoft.com>2012-08-21 00:24:08 -0700
commit1ac82df441e621fce2f38d53b5d17c69650d7358 (patch)
treea882d519a00f2d7cef05756598257867f7523e41 /Test/test15
parent61ca25219a71a22430b3f7a5071f8655cbf75cb1 (diff)
Dafny and Boogie: get rid of 'static' fields in parser
Diffstat (limited to 'Test/test15')
-rw-r--r--Test/test15/Answer28
1 files changed, 14 insertions, 14 deletions
diff --git a/Test/test15/Answer b/Test/test15/Answer
index ae010dc9..24ed0446 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -1,9 +1,9 @@
-------------------- NullInModel --------------------
*** MODEL
-%lbl%@47 -> false
-%lbl%+24 -> true
-%lbl%+37 -> true
+%lbl%@46 -> false
+%lbl%+23 -> true
+%lbl%+36 -> true
boolType -> T@T!val!1
intType -> T@T!val!0
null -> T@U!val!0
@@ -33,9 +33,9 @@ Boogie program verifier finished with 0 verified, 1 error
-------------------- IntInModel --------------------
*** MODEL
-%lbl%@39 -> false
-%lbl%+23 -> true
-%lbl%+29 -> true
+%lbl%@38 -> false
+%lbl%+22 -> true
+%lbl%+28 -> true
boolType -> T@T!val!1
i -> 0
intType -> T@T!val!0
@@ -58,9 +58,9 @@ Boogie program verifier finished with 0 verified, 1 error
-------------------- ModelTest --------------------
*** MODEL
-%lbl%@182 -> false
-%lbl%+119 -> true
-%lbl%+64 -> true
+%lbl%@181 -> false
+%lbl%+118 -> true
+%lbl%+63 -> true
boolType -> T@T!val!1
i@0 -> 1
intType -> T@T!val!0
@@ -114,11 +114,11 @@ Execution trace:
CaptureState.bpl(16,5): anon4_Then
CaptureState.bpl(24,5): anon3
*** MODEL
-%lbl%@336 -> false
-%lbl%+112 -> true
-%lbl%+114 -> true
-%lbl%+118 -> true
-%lbl%+191 -> true
+%lbl%@335 -> false
+%lbl%+111 -> true
+%lbl%+113 -> true
+%lbl%+117 -> true
+%lbl%+190 -> true
@MV_state_const -> 6
boolType -> T@T!val!1
F -> T@U!val!2