diff options
| -rw-r--r-- | Test/test15/CaptureState.bpl.expect | 32 |
1 files changed, 16 insertions, 16 deletions
diff --git a/Test/test15/CaptureState.bpl.expect b/Test/test15/CaptureState.bpl.expect index 2c8722d9..5d9d41c5 100644 --- a/Test/test15/CaptureState.bpl.expect +++ b/Test/test15/CaptureState.bpl.expect @@ -12,24 +12,19 @@ $mv_state_const -> 3 %lbl%+118 -> true %lbl%+148 -> true F -> T@FieldName!val!0 -Heap -> T@[Ref,FieldName]Int!val!0 +Heap -> |T@[Ref,FieldName]Int!val!0| m -> **m -m@0 -> -276 -m@1 -> -275 -m@3 -> -275 +m@0 -> (- 276) +m@1 -> (- 275) +m@3 -> (- 275) r -> **r -r@0 -> -550 +r@0 -> (- 550) 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 -} -tickleBool -> { - true -> true - false -> true - else -> true + |T@[Ref,FieldName]Int!val!0| T@Ref!val!0 T@FieldName!val!0 -> (- 276) + else -> (- 276) } $mv_state -> { 3 0 -> true @@ -38,8 +33,13 @@ $mv_state -> { 3 5 -> true else -> true } +tickleBool -> { + true -> true + false -> true + else -> true +} *** STATE <initial> - Heap -> T@[Ref,FieldName]Int!val!0 + Heap -> |T@[Ref,FieldName]Int!val!0| this -> T@Ref!val!0 x -> 719 y -> **y @@ -49,13 +49,13 @@ $mv_state -> { *** STATE top *** END_STATE *** STATE then - m -> -276 + m -> (- 276) *** END_STATE *** STATE postUpdate0 - m -> -275 + m -> (- 275) *** END_STATE *** STATE end - r -> -550 + r -> (- 550) m -> 7 *** END_STATE *** END_MODEL |