diff options
| author |  rustanleino <unknown> | 2009-08-07 17:21:13 +0000 |
|---|---|---|
| committer | rustanleino <unknown> | 2009-08-07 17:21:13 +0000 |
| commit | faf1c46b1e67ab4c3d8a1c82974b0499015a83d3 (patch) | |
| tree | 923bae2639dd557a9fed921135cca78911cef619 /Test/test15 | |
| parent | 46b654cd5c5a0dc3df37d9a593fa5c81c59ab83f (diff) | |
Removed Output files. These are created on a local machine when the tests are run.
Diffstat (limited to 'Test/test15')
| -rw-r--r-- | Test/test15/Output | 177 |
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
|