diff options
author | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:01:52 -0400 |
---|---|---|
committer | Benjamin Barenblat <bbaren@mit.edu> | 2016-06-05 15:01:52 -0400 |
commit | 41082463d783d6f8d8a5aaf69bf459b57bca6000 (patch) | |
tree | 8b9dca4b583b9cb1ea7ed220fe34d611217eb6cc /Test/test15/CaptureState.bpl.expect | |
parent | 64e8b33656140b87137d0662d9e6835e004d13c2 (diff) | |
parent | 8ed5dab22d8377924ee6282b83c1b1f8aa8f3573 (diff) |
Merge branch 'upstream' into dfsg_free
Diffstat (limited to 'Test/test15/CaptureState.bpl.expect')
-rw-r--r-- | Test/test15/CaptureState.bpl.expect | 18 |
1 files changed, 9 insertions, 9 deletions
diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect index 5d9d41c5..6939fee4 100644 --- a/Test/test15/CaptureState.bpl.expect +++ b/Test/test15/CaptureState.bpl.expect @@ -14,17 +14,17 @@ $mv_state_const -> 3 F -> T@FieldName!val!0 Heap -> |T@[Ref,FieldName]Int!val!0| m -> **m -m@0 -> (- 276) -m@1 -> (- 275) -m@3 -> (- 275) +m@0 -> (- 2) +m@1 -> (- 1) +m@3 -> (- 1) r -> **r -r@0 -> (- 550) +r@0 -> (- 2) this -> T@Ref!val!0 x -> 719 y -> **y Select_[Ref,FieldName]$int -> { - |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 276) - else -> (- 276) + |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 2) + else -> (- 2) } $mv_state -> { 3 0 -> true @@ -49,13 +49,13 @@ tickleBool -> { *** STATE top *** END_STATE *** STATE then - m -> (- 276) + m -> (- 2) *** END_STATE *** STATE postUpdate0 - m -> (- 275) + m -> (- 1) *** END_STATE *** STATE end - r -> (- 550) + r -> (- 2) m -> 7 *** END_STATE *** END_MODEL |