-------------------- 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
}
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
}
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
}
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