-------------------- NullInModel --------------------
Z3 error model: 
partitions:
*0 -> true
*1 -> false
*2 {@true} -> 3:int
*3 {@false} -> 4:int
*4 {intType} 
*5 {boolType} 
*6 {refType} 
*7 {s null} 
*8 -> 0:int
*9 -> 1:int
*10 -> 2:int
*11 
function interpretations:
$pow2 -> {
  *8 -> *9
  else -> #unspecified
}
tickleBool -> {
  *1 -> *0
  *0 -> *0
  else -> #unspecified
}
Ctor -> {
  *4 -> *8
  *5 -> *9
  *6 -> *10
  else -> #unspecified
}
type -> {
  *7 -> *6
  else -> #unspecified
}
END_OF_MODEL
.
identifierToPartition:
@true : *2
@false : *3
intType : *4
boolType : *5
refType : *6
s : *7
null : *7
valueToPartition:
True : *0
False : *1
3 : *2
4 : *3
0 : *8
1 : *9
2 : *10
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 -> true
*1 -> false
*2 {@true} -> 2:int
*3 {@false} -> 3:int
*4 {intType} 
*5 {boolType} 
*6 {i} -> 0:int
*7 -> 1:int
*8 
function interpretations:
$pow2 -> {
  *6 -> *7
  else -> #unspecified
}
tickleBool -> {
  *1 -> *0
  *0 -> *0
  else -> #unspecified
}
Ctor -> {
  *4 -> *6
  *5 -> *7
  else -> #unspecified
}
END_OF_MODEL
.
identifierToPartition:
@true : *2
@false : *3
intType : *4
boolType : *5
i : *6
valueToPartition:
True : *0
False : *1
2 : *2
3 : *3
0 : *6
1 : *7
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 -> true
*1 -> false
*2 {@true} -> 5:int
*3 {@false} -> 6:int
*4 {intType} 
*5 {boolType} 
*6 {refType} 
*7 {s} 
*8 {r} 
*9 {i@0} -> 1:int
*10 {j@0} -> 2:int
*11 {j@1} -> 3:int
*12 {j@2} -> 4:int
*13 -> 0:int
*14 
function interpretations:
$pow2 -> {
  *13 -> *9
  else -> #unspecified
}
tickleBool -> {
  *1 -> *0
  *0 -> *0
  else -> #unspecified
}
Ctor -> {
  *4 -> *13
  *5 -> *9
  *6 -> *10
  else -> #unspecified
}
type -> {
  *7 -> *6
  *8 -> *6
  else -> #unspecified
}
END_OF_MODEL
.
identifierToPartition:
@true : *2
@false : *3
intType : *4
boolType : *5
refType : *6
s : *7
r : *8
i@0 : *9
j@0 : *10
j@1 : *11
j@2 : *12
valueToPartition:
True : *0
False : *1
5 : *2
6 : *3
1 : *9
2 : *10
3 : *11
4 : *12
0 : *13
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
@true -> 6
@false -> 7
intType -> *4
boolType -> *5
RefType -> *6
FieldNameType -> *7
Heap -> *8
this -> *9
F -> *10
m@0 -> -2
r@0 -> -2
x@@4 -> 797
m@2 -> -1
m@3 -> -1
y@@1 -> **y@@1
r -> **r
m -> **m
$pow2 -> {
  0 -> 1
  else -> *22
}
tickleBool -> {
  false -> true
  true -> true
  else -> *22
}
Ctor -> {
  *4 -> 0
  *5 -> 1
  *6 -> 3
  *7 -> 4
  *18 -> 2
  else -> *22
}
type -> {
  *8 -> *18
  *9 -> *6
  *10 -> *7
  -2 -> *4
  else -> *22
}
MapType0Type -> {
  *6 *7 *4 -> *18
  else -> *22
}
MapType0TypeInv2 -> {
  *18 -> *4
  else -> *22
}
MapType0TypeInv1 -> {
  *18 -> *7
  else -> *22
}
MapType0TypeInv0 -> {
  *18 -> *6
  else -> *22
}
@MV_state -> {
  0 -> true
  3 -> true
  4 -> true
  5 -> true
  else -> *22
}
[3] -> {
  *8 *9 *10 -> -2
  else -> *22
}
U_2_int -> {
  -2 -> -2
  else -> *22
}
int_2_U -> {
  -2 -> -2
  else -> *22
}
*** STATE <initial>
  Heap -> *8
  this -> *9
  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