diff options
Diffstat (limited to 'Test/test15')
| -rw-r--r-- | Test/test15/Answer | 28 |
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
|