-------------------- NullInModel --------------------
Z3 error model: 
partitions:
*0 {%lbl%+24 %lbl%+37} -> true
*1 {%lbl%@47} -> false
*2 {s null} 
*3 {refType} 
*4 {intType} 
*5 {boolType} 
*6 -> 0:int
*7 -> 1:int
*8 -> 2:int
*9 
function interpretations:
tickleBool -> {
  *0 -> *0
  *1 -> *0
  else -> #unspecified
}
type -> {
  *2 -> *3
  else -> #unspecified
}
Ctor -> {
  *4 -> *6
  *5 -> *7
  *3 -> *8
  else -> #unspecified
}
END_OF_MODEL
.
identifierToPartition:
%lbl%+24 : *0
%lbl%+37 : *0
%lbl%@47 : *1
s : *2
null : *2
refType : *3
intType : *4
boolType : *5
valueToPartition:
True : *0
False : *1
0 : *6
1 : *7
2 : *8
End of 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 --------------------
Z3 error model: 
partitions:
*0 {%lbl%+29 %lbl%+23} -> true
*1 {%lbl%@39} -> false
*2 {intType} 
*3 {boolType} 
*4 {i} -> 0:int
*5 -> 1:int
*6 
function interpretations:
tickleBool -> {
  *0 -> *0
  *1 -> *0
  else -> #unspecified
}
Ctor -> {
  *2 -> *4
  *3 -> *5
  else -> #unspecified
}
END_OF_MODEL
.
identifierToPartition:
%lbl%+29 : *0
%lbl%+23 : *0
%lbl%@39 : *1
intType : *2
boolType : *3
i : *4
valueToPartition:
True : *0
False : *1
0 : *4
1 : *5
End of 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 --------------------
Z3 error model: 
partitions:
*0 {%lbl%+64 %lbl%+119} -> true
*1 {%lbl%@182} -> false
*2 {s} 
*3 {j@2} -> 4:int
*4 {boolType} 
*5 {intType} 
*6 {refType} 
*7 {i@0} -> 1:int
*8 {j@0} -> 2:int
*9 {j@1} -> 3:int
*10 {r} 
*11 -> 0:int
*12 
function interpretations:
tickleBool -> {
  *0 -> *0
  *1 -> *0
  else -> #unspecified
}
type -> {
  *2 -> *6
  *10 -> *6
  else -> #unspecified
}
Ctor -> {
  *5 -> *11
  *4 -> *7
  *6 -> *8
  else -> #unspecified
}
END_OF_MODEL
.
identifierToPartition:
%lbl%+64 : *0
%lbl%+119 : *0
%lbl%@182 : *1
s : *2
j@2 : *3
boolType : *4
intType : *5
refType : *6
i@0 : *7
j@0 : *8
j@1 : *9
r : *10
valueToPartition:
True : *0
False : *1
4 : *3
1 : *7
2 : *8
3 : *9
0 : *11
End of 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
%lbl%+112 -> true
%lbl%+116 -> true
%lbl%+110 -> true
%lbl%+189 -> true
%lbl%@334 -> false
m@3 -> -1
m@2 -> -1
this -> *3
intType -> *4
Heap -> *5
FieldNameType -> *6
m@0 -> -2
r@0 -> -2
boolType -> *8
RefType -> *9
F -> *10
@MV_state_const -> 6
x@@4 -> 797
y@@1 -> **y@@1
r -> **r
m -> **m
tickleBool -> {
  true -> true
  false -> true
  else -> true
}
type -> {
  *5 -> *13
  *3 -> *9
  *10 -> *6
  -2 -> *4
  else -> *13
}
Ctor -> {
  *4 -> 0
  *8 -> 1
  *9 -> 3
  *6 -> 4
  *13 -> 2
  else -> 0
}
@MV_state -> {
  6 0 -> true
  6 3 -> true
  6 4 -> true
  6 5 -> true
  else -> true
}
[3] -> {
  *5 *3 *10 -> -2
  else -> -2
}
U_2_int -> {
  -2 -> -2
  else -> -2
}
MapType0TypeInv1 -> {
  *13 -> *6
  else -> *6
}
MapType0Type -> {
  *9 *6 *4 -> *13
  else -> *13
}
MapType0TypeInv2 -> {
  *13 -> *4
  else -> *4
}
MapType0TypeInv0 -> {
  *13 -> *9
  else -> *9
}
int_2_U -> {
  -2 -> -2
  else -> -2
}
*** STATE <initial>
  Heap -> *5
  this -> *3
  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