1 files changed, 177 insertions, 0 deletions
diff --git a/Test/test15/Answer b/Test/test15/Answer
new file mode 100644
index 00000000..2054998f
--- /dev/null
+++ b/Test/test15/Answer
@@ -0,0 +1,177 @@
+
+-------------------- 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