Update to match the new model printing format

1 files changed, 94 insertions, 158 deletions

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 4e3886aa..56c247c2 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -1,51 +1,30 @@
 

 -------------------- NullInModel --------------------

-Z3 error model: 

-partitions:

-*0 {%lbl%+24 %lbl%+37} -> true

-*1 {%lbl%@47} -> false

-*2 {s null} 

-*3 {refType} 

-*4 {intType} 

-*5 {boolType} 

-*6 -> 0:int

-*7 -> 1:int

-*8 -> 2:int

-*9 

-function interpretations:

+*** MODEL

+s -> T@U!val!0

+%lbl%+24 -> true

+%lbl%@47 -> false

+refType -> T@T!val!2

+intType -> T@T!val!0

+%lbl%+37 -> true

+boolType -> T@T!val!1

+null -> T@U!val!0

 tickleBool -> {

-  *0 -> *0

-  *1 -> *0

-  else -> #unspecified

+  true -> true

+  false -> true

+  else -> true

 }

 type -> {

-  *2 -> *3

-  else -> #unspecified

+  T@U!val!0 -> T@T!val!2

+  else -> T@T!val!2

 }

 Ctor -> {

-  *4 -> *6

-  *5 -> *7

-  *3 -> *8

-  else -> #unspecified

+  T@T!val!0 -> 0

+  T@T!val!1 -> 1

+  T@T!val!2 -> 2

+  else -> 0

 }

-END_OF_MODEL

-.

-identifierToPartition:

-%lbl%+24 : *0

-%lbl%+37 : *0

-%lbl%@47 : *1

-s : *2

-null : *2

-refType : *3

-intType : *4

-boolType : *5

-valueToPartition:

-True : *0

-False : *1

-0 : *6

-1 : *7

-2 : *8

-End of model.

+*** END_MODEL

 NullInModel.bpl(2,3): Error BP5001: This assertion might not hold.

 Execution trace:

     NullInModel.bpl(2,3): anon0

@@ -53,41 +32,24 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- IntInModel --------------------

-Z3 error model: 

-partitions:

-*0 {%lbl%+29 %lbl%+23} -> true

-*1 {%lbl%@39} -> false

-*2 {intType} 

-*3 {boolType} 

-*4 {i} -> 0:int

-*5 -> 1:int

-*6 

-function interpretations:

+*** MODEL

+intType -> T@T!val!0

+boolType -> T@T!val!1

+%lbl%+29 -> true

+%lbl%+23 -> true

+i -> 0

+%lbl%@39 -> false

 tickleBool -> {

-  *0 -> *0

-  *1 -> *0

-  else -> #unspecified

+  true -> true

+  false -> true

+  else -> true

 }

 Ctor -> {

-  *2 -> *4

-  *3 -> *5

-  else -> #unspecified

+  T@T!val!0 -> 0

+  T@T!val!1 -> 1

+  else -> 0

 }

-END_OF_MODEL

-.

-identifierToPartition:

-%lbl%+29 : *0

-%lbl%+23 : *0

-%lbl%@39 : *1

-intType : *2

-boolType : *3

-i : *4

-valueToPartition:

-True : *0

-False : *1

-0 : *4

-1 : *5

-End of model.

+*** END_MODEL

 IntInModel.bpl(2,3): Error BP5001: This assertion might not hold.

 Execution trace:

     IntInModel.bpl(2,3): anon0

@@ -95,62 +57,36 @@ Execution trace:
 Boogie program verifier finished with 0 verified, 1 error

 

 -------------------- ModelTest --------------------

-Z3 error model: 

-partitions:

-*0 {%lbl%+64 %lbl%+119} -> true

-*1 {%lbl%@182} -> false

-*2 {s} 

-*3 {j@2} -> 4:int

-*4 {boolType} 

-*5 {intType} 

-*6 {refType} 

-*7 {i@0} -> 1:int

-*8 {j@0} -> 2:int

-*9 {j@1} -> 3:int

-*10 {r} 

-*11 -> 0:int

-*12 

-function interpretations:

+*** MODEL

+%lbl%+64 -> true

+s -> T@U!val!0

+j@2 -> 4

+%lbl%+119 -> true

+boolType -> T@T!val!1

+intType -> T@T!val!0

+refType -> T@T!val!2

+%lbl%@182 -> false

+i@0 -> 1

+j@0 -> 2

+j@1 -> 3

+r -> T@U!val!1

 tickleBool -> {

-  *0 -> *0

-  *1 -> *0

-  else -> #unspecified

+  true -> true

+  false -> true

+  else -> true

 }

 type -> {

-  *2 -> *6

-  *10 -> *6

-  else -> #unspecified

+  T@U!val!0 -> T@T!val!2

+  T@U!val!1 -> T@T!val!2

+  else -> T@T!val!2

 }

 Ctor -> {

-  *5 -> *11

-  *4 -> *7

-  *6 -> *8

-  else -> #unspecified

+  T@T!val!0 -> 0

+  T@T!val!1 -> 1

+  T@T!val!2 -> 2

+  else -> 0

 }

-END_OF_MODEL

-.

-identifierToPartition:

-%lbl%+64 : *0

-%lbl%+119 : *0

-%lbl%@182 : *1

-s : *2

-j@2 : *3

-boolType : *4

-intType : *5

-refType : *6

-i@0 : *7

-j@0 : *8

-j@1 : *9

-r : *10

-valueToPartition:

-True : *0

-False : *1

-4 : *3

-1 : *7

-2 : *8

-3 : *9

-0 : *11

-End of model.

+*** END_MODEL

 ModelTest.bpl(7,3): Error BP5001: This assertion might not hold.

 Execution trace:

     ModelTest.bpl(3,5): anon0

@@ -178,22 +114,22 @@ Execution trace:
     CaptureState.bpl(16,5): anon4_Then

     CaptureState.bpl(24,5): anon3

 *** MODEL

+m@3 -> -1

+this -> T@U!val!1

+intType -> T@T!val!0

 %lbl%+112 -> true

+Heap -> T@U!val!0

 %lbl%+116 -> true

 %lbl%+110 -> true

-%lbl%+189 -> true

-%lbl%@334 -> false

-m@3 -> -1

-m@2 -> -1

-this -> *3

-intType -> *4

-Heap -> *5

-FieldNameType -> *6

+FieldNameType -> T@T!val!3

 m@0 -> -2

+m@2 -> -1

 r@0 -> -2

-boolType -> *8

-RefType -> *9

-F -> *10

+boolType -> T@T!val!1

+%lbl%@334 -> false

+%lbl%+189 -> true

+RefType -> T@T!val!2

+F -> T@U!val!2

 @MV_state_const -> 6

 x@@4 -> 797

 y@@1 -> **y@@1

@@ -205,18 +141,18 @@ tickleBool -> {
   else -> true

 }

 type -> {

-  *5 -> *13

-  *3 -> *9

-  *10 -> *6

-  -2 -> *4

-  else -> *13

+  T@U!val!0 -> T@T!val!4

+  T@U!val!1 -> T@T!val!2

+  T@U!val!2 -> T@T!val!3

+  T@U!val!3 -> T@T!val!0

+  else -> T@T!val!4

 }

 Ctor -> {

-  *4 -> 0

-  *8 -> 1

-  *9 -> 3

-  *6 -> 4

-  *13 -> 2

+  T@T!val!0 -> 0

+  T@T!val!1 -> 1

+  T@T!val!2 -> 3

+  T@T!val!3 -> 4

+  T@T!val!4 -> 2

   else -> 0

 }

 @MV_state -> {

@@ -226,37 +162,37 @@ Ctor -> {
   6 5 -> true

   else -> true

 }

-[3] -> {

-  *5 *3 *10 -> -2

-  else -> -2

+MapType0Select -> {

+  T@U!val!0 T@U!val!1 T@U!val!2 -> T@U!val!3

+  else -> T@U!val!3

 }

 U_2_int -> {

-  -2 -> -2

+  T@U!val!3 -> -2

   else -> -2

 }

 MapType0TypeInv1 -> {

-  *13 -> *6

-  else -> *6

+  T@T!val!4 -> T@T!val!3

+  else -> T@T!val!3

 }

 MapType0Type -> {

-  *9 *6 *4 -> *13

-  else -> *13

+  T@T!val!2 T@T!val!3 T@T!val!0 -> T@T!val!4

+  else -> T@T!val!4

 }

 MapType0TypeInv2 -> {

-  *13 -> *4

-  else -> *4

+  T@T!val!4 -> T@T!val!0

+  else -> T@T!val!0

 }

 MapType0TypeInv0 -> {

-  *13 -> *9

-  else -> *9

+  T@T!val!4 -> T@T!val!2

+  else -> T@T!val!2

 }

 int_2_U -> {

-  -2 -> -2

-  else -> -2

+  -2 -> T@U!val!3

+  else -> T@U!val!3

 }

 *** STATE <initial>

-  Heap -> *5

-  this -> *3

+  Heap -> T@U!val!0

+  this -> T@U!val!1

   x -> 797

   y -> **y@@1

   r -> **r