-------------------- NullInModel --------------------
*** MODEL
%lbl%@47 -> false
%lbl%+24 -> true
%lbl%+37 -> true
null -> T@ref!val!0
s -> T@ref!val!0
tickleBool -> {
  true -> true
  false -> true
  else -> true
}
*** END_MODEL
NullInModel.bpl(4,3): Error BP5001: This assertion might not hold.
Execution trace:
    NullInModel.bpl(4,3): anon0

Boogie program verifier finished with 0 verified, 1 error

-------------------- IntInModel --------------------
*** MODEL
%lbl%@39 -> false
%lbl%+23 -> true
%lbl%+29 -> true
i -> 0
tickleBool -> {
  true -> true
  false -> true
  else -> true
}
*** END_MODEL
IntInModel.bpl(4,3): Error BP5001: This assertion might not hold.
Execution trace:
    IntInModel.bpl(4,3): anon0

Boogie program verifier finished with 0 verified, 1 error

-------------------- ModelTest --------------------
*** MODEL
%lbl%@147 -> false
%lbl%+64 -> true
%lbl%+84 -> true
i@0 -> 1
j@0 -> 2
j@1 -> 3
j@2 -> 4
tickleBool -> {
  true -> true
  false -> true
  else -> true
}
*** END_MODEL
ModelTest.bpl(9,3): Error BP5001: This assertion might not hold.
Execution trace:
    ModelTest.bpl(5,5): anon0

Boogie program verifier finished with 0 verified, 1 error

-------------------- InterpretedFunctionTests --------------------
InterpretedFunctionTests.bpl(6,3): Error BP5001: This assertion might not hold.
Execution trace:
    InterpretedFunctionTests.bpl(4,3): anon0
InterpretedFunctionTests.bpl(12,3): Error BP5001: This assertion might not hold.
Execution trace:
    InterpretedFunctionTests.bpl(10,3): anon0
InterpretedFunctionTests.bpl(18,3): Error BP5001: This assertion might not hold.
Execution trace:
    InterpretedFunctionTests.bpl(16,3): anon0

Boogie program verifier finished with 0 verified, 3 errors

-------------------- CaptureState --------------------
CaptureState.bpl(29,1): Error BP5003: A postcondition might not hold on this return path.
CaptureState.bpl(10,3): Related location: This is the postcondition that might not hold.
Execution trace:
    CaptureState.bpl(14,3): anon0
    CaptureState.bpl(18,5): anon4_Then
    CaptureState.bpl(26,5): anon3
*** MODEL
$mv_state_const -> 3
%lbl%@293 -> false
%lbl%+112 -> true
%lbl%+114 -> true
%lbl%+118 -> true
%lbl%+148 -> true
F -> T@FieldName!val!0
Heap -> T@[Ref,FieldName]Int!val!0
m -> **m
m@0 -> -276
m@1 -> -275
m@3 -> -275
r -> **r
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
}
$mv_state -> {
  3 0 -> true
  3 1 -> true
  3 2 -> true
  3 5 -> true
  else -> true
}
*** STATE <initial>
  Heap -> T@[Ref,FieldName]Int!val!0
  this -> T@Ref!val!0
  x -> 719
  y -> **y
  r -> **r
  m -> **m
*** END_STATE
*** STATE top
*** END_STATE
*** STATE then
  m -> -276
*** END_STATE
*** STATE postUpdate0
  m -> -275
*** END_STATE
*** STATE end
  r -> -550
  m -> 7
*** END_STATE
*** END_MODEL

Boogie program verifier finished with 0 verified, 1 error