summaryrefslogtreecommitdiff
path: root/Test
diff options
context:
space:
mode:
authorGravatar wuestholz <unknown>2012-09-12 10:54:38 +0200
committerGravatar wuestholz <unknown>2012-09-12 10:54:38 +0200
commitf9ee0dff79312c65e78299810590ac040fd0d26b (patch)
treebb514914d2fafea4e081084295640ddca0babfa2 /Test
parentfc76541682ec019b8a2dc08ca9972ff517db9b74 (diff)
Updated test 'test15' that would fail with Z3 4.1 (different ordering of elements in the model output).
Diffstat (limited to 'Test')
-rw-r--r--Test/test15/Answer68
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