From f9ee0dff79312c65e78299810590ac040fd0d26b Mon Sep 17 00:00:00 2001
From: wuestholz <unknown>
Date: Wed, 12 Sep 2012 10:54:38 +0200
Subject: Updated test 'test15' that would fail with Z3 4.1 (different ordering
 of elements in the model output).

---
 Test/test15/Answer | 68 +++++++++++++++++++++++++++---------------------------
 1 file changed, 34 insertions(+), 34 deletions(-)

(limited to 'Test/test15')

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
-- 
cgit v1.2.3