diff --git a/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
index a71978a9753a6a8b275f287938aa29c9538c2f86..d0bb2c0c3d43729fff7db41e0cb352f522f471c0 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/vset.res.oracle
@@ -1,18 +1,46 @@
# frama-c -wp [...]
[kernel] Parsing vset.i (no preprocessing)
[wp] Running WP plugin...
+[wp] 21 goals scheduled
+[wp] [Valid] typed_lemma_direct_in (Qed)
+[wp] [Valid] typed_lemma_direct_in_singleton (Qed)
+[wp] [NoResult] typed_lemma_indirect_in_constants (Qed)
+[wp] [Unsuccess] typed_lemma_indirect_equal_logical (Tactic) (Qed)
+[wp] [Unsuccess] typed_lemma_indirect_equal_ghost (Tactic) (Qed)
+[wp] [Unsuccess] typed_lemma_indirect_equal_constants (Tactic) (Qed)
+[wp] [NoResult] typed_lemma_indirect_not_equal_logical (Qed)
+[wp] [NoResult] typed_lemma_indirect_not_equal_constants (Qed)
+[wp] [NoResult] typed_lemma_indirect_in_logical (Qed)
+[wp] [NoResult] typed_lemma_indirect_in_ghost (Qed)
+[wp] [Unsuccess] typed_lemma_iota1_compute_equal_constants (Tactic) (Qed)
+[wp] [NoResult] typed_lemma_iota0_compute_0in_constants (Qed)
+[wp] [NoResult] typed_lemma_indirect_not_in_logical (Qed)
+[wp] [NoResult] typed_lemma_indirect_not_in_constants (Qed)
+[wp] [Unsuccess] typed_lemma_iota_ind0 (Tactic) (Qed)
+[wp] [Unsuccess] typed_lemma_iota3_compute_equal_constants (Tactic) (Qed)
+[wp] [NoResult] typed_lemma_iota3_compute_2in_constants (Qed)
+[wp] [NoResult] typed_lemma_iota3_compute_0in_constants (Qed)
+[wp] [NoResult] typed_lemma_rec_iota_le0 (Qed)
+[wp] [NoResult] typed_lemma_rec_iota_gt0 (Qed)
+[wp] [NoResult] typed_lemma_rec_iota (Qed)
+[wp] Proved goals: 2 / 21
+ Qed: 2
+ Unsuccess: 19
+ Missing: 13
------------------------------------------------------------
Global
------------------------------------------------------------
Goal Lemma 'direct_in':
Prove: true.
+Prover Qed returns Valid
------------------------------------------------------------
Goal Lemma 'direct_in_singleton':
Assume Lemmas: 'direct_in'
Prove: true.
+Prover Qed returns Valid
------------------------------------------------------------
@@ -21,6 +49,7 @@ Assume Lemmas: 'indirect_not_in_constants' 'indirect_in_constants'
'direct_in_singleton' 'direct_in'
Prove: mem(1, L_Set1) /\ mem(2, L_Set1) /\ mem(3, L_Set1) /\
(forall i : Z. (mem(i, L_Set1) -> ((i = 1) \/ (i = 2) \/ (i = 3)))).
+Prover Script returns Unsuccess
------------------------------------------------------------
@@ -30,15 +59,11 @@ Assume Lemmas: 'indirect_in_ghost' 'indirect_not_equal_logical'
'indirect_not_equal_constants' 'indirect_equal_constants'
'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
'direct_in'
-Let a = L_Set2(int3_0, int2_0, int1_0).
-Assume {
- Have: is_sint32(int1_0).
- Have: is_sint32(int2_0).
- Have: is_sint32(int3_0).
-}
-Prove: mem(int1_0, a) /\ mem(int2_0, a) /\ mem(int3_0, a) /\
- (forall i : Z. (mem(i, a) ->
- ((i = int1_0) \/ (i = int2_0) \/ (i = int3_0)))).
+Let a = L_Set2(int2_0, int1_0).
+Assume { Have: is_sint32(int1_0). Have: is_sint32(int2_0). }
+Prove: mem(int1_0, a) /\ mem(int2_0, a) /\
+ (forall i : Z. (mem(i, a) -> ((i = int1_0) \/ (i = int2_0)))).
+Prover Script returns Unsuccess
------------------------------------------------------------
@@ -47,8 +72,9 @@ Assume Lemmas: 'indirect_not_in_logical' 'indirect_in_logical'
'indirect_not_equal_constants' 'indirect_equal_constants'
'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
'direct_in'
-Prove: mem(1, L_Set3) /\ mem(2, L_Set3) /\ mem(3, L_Set3) /\
- (forall i : Z. (mem(i, L_Set3) -> ((i = 1) \/ (i = 2) \/ (i = 3)))).
+Prove: mem(1, L_Set3) /\ mem(2, L_Set3) /\
+ (forall i : Z. (mem(i, L_Set3) -> ((i = 1) \/ (i = 2)))).
+Prover Script returns Unsuccess
------------------------------------------------------------
@@ -65,7 +91,7 @@ Assume Lemmas: 'indirect_not_equal_logical' 'indirect_equal_logical'
'indirect_not_in_constants' 'indirect_in_constants' 'direct_in_singleton'
'direct_in'
Assume { Have: is_sint32(int2_0). }
-Prove: mem(int2_0, L_Set2(int3_0, int2_0, int1_0)).
+Prove: mem(int2_0, L_Set2(int2_0, int1_0)).
------------------------------------------------------------
@@ -90,8 +116,8 @@ Assume Lemmas: 'indirect_equal_logical' 'indirect_not_in_logical'
'indirect_in_logical' 'indirect_not_equal_constants'
'indirect_equal_constants' 'indirect_not_in_constants'
'indirect_in_constants' 'direct_in_singleton' 'direct_in'
-Prove: (!mem(0, L_Set3)) \/ (!mem(1, L_Set3)) \/ (!mem(2, L_Set3)) \/
- (exists i : Z. (i != 0) /\ (i != 1) /\ (i != 2) /\ mem(i, L_Set3)).
+Prove: (!mem(0, L_Set3)) \/ (!mem(1, L_Set3)) \/
+ (exists i : Z. (i != 0) /\ (i != 1) /\ mem(i, L_Set3)).
------------------------------------------------------------
@@ -132,6 +158,7 @@ Assume Lemmas: 'iota3_compute_equal_constants' 'iota3_compute_2in_constants'
Let a = L_iota(1).
Prove: mem(0, a) /\ mem(1, a) /\
(forall i : Z. (mem(i, a) -> ((i = 0) \/ (i = 1)))).
+Prover Script returns Unsuccess
------------------------------------------------------------
@@ -171,6 +198,7 @@ Assume Lemmas: 'iota3_compute_2in_constants' 'iota3_compute_0in_constants'
Let a = L_iota(3).
Prove: mem(0, a) /\ mem(1, a) /\ mem(2, a) /\ mem(3, a) /\
(forall i : Z. (mem(i, a) -> ((i = 0) \/ (i = 1) \/ (i = 2) \/ (i = 3)))).
+Prover Script returns Unsuccess
------------------------------------------------------------
@@ -183,6 +211,7 @@ Assume Lemmas: 'indirect_equal_ghost' 'indirect_in_ghost'
'direct_in'
Let a = L_iota(n). Assume { Have: n <= 0. }
Prove: mem(0, a) /\ (forall i : Z. (mem(i, a) -> (i = 0))).
+Prover Script returns Unsuccess
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle
index f8daf4ebd2ec2fdc6083528998465bef11aa1d12..4321202310536de6175a7c58823447dbec7fc2a5 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle_qualif/vset.res.oracle
@@ -18,16 +18,16 @@
[wp] [Valid] typed_lemma_iota1_compute_equal_constants (Alt-Ergo) (Cached)
[wp] [Valid] typed_lemma_iota3_compute_0in_constants (Alt-Ergo) (Cached)
[wp] [Valid] typed_lemma_iota3_compute_2in_constants (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_lemma_iota3_compute_equal_constants (Alt-Ergo) (Cached)
-[wp] [Unsuccess] typed_lemma_iota_ind0 (Alt-Ergo) (Cached)
+[wp] [Valid] typed_lemma_iota3_compute_equal_constants (Alt-Ergo) (Cached)
+[wp] [Unsuccess] typed_lemma_iota_ind0 (Tactic) (Alt-Ergo) (Cached)
[wp] [Valid] typed_lemma_rec_iota (Alt-Ergo) (Cached)
[wp] [Unsuccess] typed_lemma_rec_iota_gt0 (Alt-Ergo) (Cached)
[wp] [Valid] typed_lemma_rec_iota_le0 (Alt-Ergo) (Cached)
-[wp] Proved goals: 18 / 21
+[wp] Proved goals: 19 / 21
Qed: 2
- Alt-Ergo: 16
- Unsuccess: 3
+ Alt-Ergo: 17
+ Unsuccess: 2
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Lemma 2 16 21 85.7%
+ Lemma 2 17 21 90.5%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_acsl/vset.i b/src/plugins/wp/tests/wp_acsl/vset.i
index 57820e5ace321bd556ef478a1298dc6a5f05f0bb..efe4e4e52c779172ceb0eda13fc51fa916efeeb6 100644
--- a/src/plugins/wp/tests/wp_acsl/vset.i
+++ b/src/plugins/wp/tests/wp_acsl/vset.i
@@ -1,3 +1,9 @@
+/* run.config
+ OPT:-wp-auto wp:split
+*/
+/* run.config_qualif
+ OPT:-wp-auto wp:split
+*/
//@ lemma direct_in: 2 \in {1,2,3};
//@ lemma direct_in_singleton: 2 \in {2};
@@ -11,19 +17,17 @@
//@ logic integer i0 = 0;
//@ logic integer i1 = 1;
//@ logic integer i2 = 2;
-//@ logic integer i3 = 3;
-//@ logic set<integer> Set3 = {i1,i2,i3};
+//@ logic set<integer> Set3 = {i1,i2};
//@ lemma indirect_in_logical: i2 \in Set3;
//@ lemma indirect_not_in_logical: ! (i0 \in Set3);
-//@ lemma indirect_equal_logical: Set3 == {i1,i2,i3};
-//@ lemma indirect_not_equal_logical: Set3 != {i0,i1,i2};
+//@ lemma indirect_equal_logical: Set3 == {i1,i2};
+//@ lemma indirect_not_equal_logical: Set3 != {i0,i1};
//@ ghost int int1 = 1;
//@ ghost int int2 = 2;
-//@ ghost int int3 = 3;
-//@ logic set<int> Set2 = {int1,int2,int3};
+//@ logic set<int> Set2 = {int1,int2};
//@ lemma indirect_in_ghost: int2 \in Set2;
-//@ lemma indirect_equal_ghost: Set2 == {int1,int2,int3};
+//@ lemma indirect_equal_ghost: Set2 == {int1,int2};
/*@
logic set<integer> iota(integer n) =