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