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

Boogie program verifier finished with 0 verified, 1 error

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

Boogie program verifier finished with 0 verified, 1 error

-------------------- ModelTest --------------------
*** MODEL
%lbl%+64 -> true
s -> T@U!val!0
j@2 -> 4
%lbl%+119 -> true
boolType -> T@T!val!1
intType -> T@T!val!0
refType -> T@T!val!2
%lbl%@182 -> false
i@0 -> 1
j@0 -> 2
j@1 -> 3
r -> T@U!val!1
tickleBool -> {
  true -> true
  false -> true
  else -> true
}
type -> {
  T@U!val!0 -> T@T!val!2
  T@U!val!1 -> T@T!val!2
  else -> T@T!val!2
}
Ctor -> {
  T@T!val!0 -> 0
  T@T!val!1 -> 1
  T@T!val!2 -> 2
  else -> 0
}
*** END_MODEL
ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.
Execution trace:
    ModelTest.bpl(3,5): anon0

Boogie program verifier finished with 0 verified, 1 error

-------------------- InterpretedFunctionTests --------------------
InterpretedFunctionTests.bpl(4,3): Error BP5001: This assertion might not hold.
Execution trace:
    InterpretedFunctionTests.bpl(2,3): anon0
InterpretedFunctionTests.bpl(10,3): Error BP5001: This assertion might not hold.
Execution trace:
    InterpretedFunctionTests.bpl(8,3): anon0
InterpretedFunctionTests.bpl(16,3): Error BP5001: This assertion might not hold.
Execution trace:
    InterpretedFunctionTests.bpl(14,3): anon0

Boogie program verifier finished with 0 verified, 3 errors

-------------------- CaptureState --------------------
CaptureState.bpl(27,1): Error BP5003: A postcondition might not hold on this return path.
CaptureState.bpl(8,3): Related location: This is the postcondition that might not hold.
Execution trace:
    CaptureState.bpl(12,3): anon0
    CaptureState.bpl(16,5): anon4_Then
    CaptureState.bpl(24,5): anon3
*** MODEL
m@3 -> -1
this -> T@U!val!1
intType -> T@T!val!0
%lbl%+112 -> true
Heap -> T@U!val!0
%lbl%+116 -> true
%lbl%+110 -> true
FieldNameType -> T@T!val!3
m@0 -> -2
m@2 -> -1
r@0 -> -2
boolType -> T@T!val!1
%lbl%@334 -> false
%lbl%+189 -> true
RefType -> T@T!val!2
F -> T@U!val!2
@MV_state_const -> 6
x@@4 -> 797
y@@1 -> **y@@1
r -> **r
m -> **m
tickleBool -> {
  true -> true
  false -> true
  else -> true
}
type -> {
  T@U!val!0 -> T@T!val!4
  T@U!val!1 -> T@T!val!2
  T@U!val!2 -> T@T!val!3
  T@U!val!3 -> T@T!val!0
  else -> T@T!val!4
}
Ctor -> {
  T@T!val!0 -> 0
  T@T!val!1 -> 1
  T@T!val!2 -> 3
  T@T!val!3 -> 4
  T@T!val!4 -> 2
  else -> 0
}
@MV_state -> {
  6 0 -> true
  6 3 -> true
  6 4 -> true
  6 5 -> true
  else -> true
}
MapType0Select -> {
  T@U!val!0 T@U!val!1 T@U!val!2 -> T@U!val!3
  else -> T@U!val!3
}
U_2_int -> {
  T@U!val!3 -> -2
  else -> -2
}
MapType0TypeInv1 -> {
  T@T!val!4 -> T@T!val!3
  else -> T@T!val!3
}
MapType0Type -> {
  T@T!val!2 T@T!val!3 T@T!val!0 -> T@T!val!4
  else -> T@T!val!4
}
MapType0TypeInv2 -> {
  T@T!val!4 -> T@T!val!0
  else -> T@T!val!0
}
MapType0TypeInv0 -> {
  T@T!val!4 -> T@T!val!2
  else -> T@T!val!2
}
int_2_U -> {
  -2 -> T@U!val!3
  else -> T@U!val!3
}
*** STATE <initial>
  Heap -> T@U!val!0
  this -> T@U!val!1
  x -> 797
  y -> **y@@1
  r -> **r
  m -> **m
*** END_STATE
*** STATE top
*** END_STATE
*** STATE then
  m -> -2
*** END_STATE
*** STATE postUpdate0
  m -> -1
*** END_STATE
*** STATE end
  r -> -2
  m -> 7
*** END_STATE
*** END_MODEL

Boogie program verifier finished with 0 verified, 1 error