Updated test 'test15' that would fail with Z3 4.1 (different ordering of elements in the model output).

1 files changed, 34 insertions, 34 deletions

diff --git a/Test/test15/Answer b/Test/test15/Answer
index 24ed0446..3361b320 100644
--- a/Test/test15/Answer
+++ b/Test/test15/Answer
@@ -9,11 +9,6 @@ intType -> T@T!val!0
 null -> T@U!val!0

 refType -> T@T!val!2

 s -> T@U!val!0

-tickleBool -> {

-  true -> true

-  false -> true

-  else -> true

-}

 type -> {

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

   else -> T@T!val!2

@@ -24,6 +19,11 @@ Ctor -> {
   T@T!val!2 -> 2

   else -> 0

 }

+tickleBool -> {

+  true -> true

+  false -> true

+  else -> true

+}

 *** END_MODEL

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

 Execution trace:

@@ -39,16 +39,16 @@ Boogie program verifier finished with 0 verified, 1 error
 boolType -> T@T!val!1

 i -> 0

 intType -> T@T!val!0

-tickleBool -> {

-  true -> true

-  false -> true

-  else -> true

-}

 Ctor -> {

   T@T!val!0 -> 0

   T@T!val!1 -> 1

   else -> 0

 }

+tickleBool -> {

+  true -> true

+  false -> true

+  else -> true

+}

 *** END_MODEL

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

 Execution trace:

@@ -70,11 +70,6 @@ j@2 -> 4
 r -> T@U!val!1

 refType -> T@T!val!2

 s -> T@U!val!0

-tickleBool -> {

-  true -> true

-  false -> true

-  else -> true

-}

 type -> {

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

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

@@ -86,6 +81,11 @@ Ctor -> {
   T@T!val!2 -> 2

   else -> 0

 }

+tickleBool -> {

+  true -> true

+  false -> true

+  else -> true

+}

 *** END_MODEL

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

 Execution trace:

@@ -135,10 +135,9 @@ RefType -> T@T!val!2
 this -> T@U!val!1

 x@@4 -> 797

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

-tickleBool -> {

-  true -> true

-  false -> true

-  else -> true

+int_2_U -> {

+  -2 -> -2

+  else -> -2

 }

 type -> {

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

@@ -147,6 +146,13 @@ type -> {
   -2 -> T@T!val!0

   else -> T@T!val!4

 }

+@MV_state -> {

+  6 0 -> true

+  6 3 -> true

+  6 4 -> true

+  6 5 -> true

+  else -> true

+}

 Ctor -> {

   T@T!val!0 -> 0

   T@T!val!1 -> 1

@@ -155,13 +161,6 @@ Ctor -> {
   T@T!val!4 -> 2

   else -> 0

 }

-@MV_state -> {

-  6 0 -> true

-  6 3 -> true

-  6 4 -> true

-  6 5 -> true

-  else -> true

-}

 [3] -> {

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

   else -> -2

@@ -174,6 +173,15 @@ MapType0TypeInv1 -> {
   T@T!val!4 -> T@T!val!3

   else -> T@T!val!3

 }

+MapType0TypeInv0 -> {

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

+  else -> T@T!val!2

+}

+tickleBool -> {

+  true -> true

+  false -> true

+  else -> true

+}

 MapType0Type -> {

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

   else -> T@T!val!4

@@ -182,14 +190,6 @@ MapType0TypeInv2 -> {
   T@T!val!4 -> T@T!val!0

   else -> T@T!val!0

 }

-MapType0TypeInv0 -> {

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

-  else -> T@T!val!2

-}

-int_2_U -> {

-  -2 -> -2

-  else -> -2

-}

 *** STATE <initial>

   Heap -> T@U!val!0

   this -> T@U!val!1