diff --git a/src/plugins/wp/tests/wp_acsl/inductive.i b/src/plugins/wp/tests/wp_acsl/inductive.i
index bf66475a23d0df4798b1a9f6bab124121d664fa2..5f3e2839f7510e61334ea67efb2550442f5a5b64 100644
--- a/src/plugins/wp/tests/wp_acsl/inductive.i
+++ b/src/plugins/wp/tests/wp_acsl/inductive.i
@@ -2,7 +2,7 @@
OPT:-wp-prover=why3 -wp-gen -wp-msg-key print-generated
*/
/* run.config_qualif
- OPT:-wp-prover=why3 -wp-gen -wp-msg-key print-generated
+ DONTRUN:
*/
/*@ inductive is_gcd(integer a, integer b, integer d) {
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/inductive.0.report.json b/src/plugins/wp/tests/wp_acsl/oracle_qualif/inductive.0.report.json
deleted file mode 100644
index 31841a97319b7a9154b21879688568fc29e119d3..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/inductive.0.report.json
+++ /dev/null
@@ -1,9 +0,0 @@
-{ "wp:global": { "wp:main": { "total": 3, "unknown": 3 } },
- "wp:axiomatics": { "": { "lemma_test_one_label": { "wp:main": { "total": 1,
- "unknown": 1 } },
- "lemma_test_no_label": { "wp:main": { "total": 1,
- "unknown": 1 } },
- "lemma_test_multilabel": { "wp:main": { "total": 1,
- "unknown": 1 } },
- "wp:section": { "wp:main": { "total": 3,
- "unknown": 3 } } } } }
diff --git a/src/plugins/wp/tests/wp_acsl/oracle_qualif/inductive.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle_qualif/inductive.res.oracle
deleted file mode 100644
index c40ad64518bbcfad37a78845e2b7e409cd50348c..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_acsl/oracle_qualif/inductive.res.oracle
+++ /dev/null
@@ -1,177 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_acsl/inductive.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] 3 goals scheduled
-[wp:print-generated]
- theory WP
- (* use why3.BuiltIn.BuiltIn *)
-
- (* use bool.Bool *)
-
- (* use int.Int *)
-
- (* use int.ComputerDivision *)
-
- (* use real.RealInfix *)
-
- (* use frama_c_wp.qed.Qed *)
-
- (* use map.Map *)
-
- (* use frama_c_wp.memory.Memory *)
-
- (* use Compound *)
-
- predicate P_reachable (int -> int) (addr -> addr) addr addr
-
- axiom Q_root_reachable :
- forall malloc:int -> int, mptr:addr -> addr, root:addr.
- P_reachable malloc mptr root root
-
- axiom Q_next_reachable :
- forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
- valid_rw malloc root 2 ->
- P_reachable malloc mptr (get mptr (shiftfield_F1__list_next root)) node ->
- P_reachable malloc mptr root node
-
- lemma Q_test_one_label :
- forall malloc:int -> int, mptr:addr -> addr, malloc1:int -> int, mptr1:
- addr -> addr, l1:addr, l2:addr.
- P_reachable malloc1 mptr1 l1 l2 -> not P_reachable malloc mptr l1 l2
-
- predicate P_is_gcd int int int
-
- axiom Q_gcd_zero : forall n:int. P_is_gcd n 0 n
-
- axiom Q_gcd_succ :
- forall a:int, b:int, d:int. P_is_gcd b (mod a b) d -> P_is_gcd a b d
-
- lemma Q_test_no_label :
- forall a:int, b:int, d:int. P_is_gcd a b d -> not P_is_gcd b d a
-
- predicate P_same_array (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:
- addr) (begin:int) (end1:int) =
- forall i:int.
- begin <= i ->
- i < end1 -> get mint1 (shift_sint32 a i) = get mint (shift_sint32 b i)
-
- predicate P_swap (mint:addr -> int) (mint1:addr -> int) (a:addr) (b:addr)
- (begin:int) (i:int) (j:int) (end1:int) =
- ((((get mint1 (shift_sint32 a i) = get mint (shift_sint32 b j) /\
- get mint1 (shift_sint32 a j) = get mint (shift_sint32 b i)) /\
- begin <= i) /\
- i < j) /\
- j < end1) /\
- (forall i1:int.
- not i1 = i ->
- not j = i1 ->
- begin <= i1 ->
- i1 < end1 ->
- get mint1 (shift_sint32 a i1) = get mint (shift_sint32 b i1))
-
- predicate P_same_elements (addr -> int) (addr -> int) addr addr int int
-
- axiom Q_refl :
- forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:int,
- end1:int.
- P_same_array mint mint1 a b begin end1 ->
- P_same_elements mint mint1 a b begin end1
-
- axiom Q_swap :
- forall mint:addr -> int, mint1:addr -> int, a:addr, b:addr, begin:int, i:
- int, j:int, end1:int.
- P_swap mint mint1 a b begin i j end1 ->
- P_same_elements mint mint1 a b begin end1
-
- axiom Q_trans :
- forall mint:addr -> int, mint1:addr -> int, mint2:addr -> int, a:addr, b:
- addr, c:addr, begin:int, end1:int.
- P_same_elements mint mint1 b c begin end1 ->
- P_same_elements mint1 mint2 a b begin end1 ->
- P_same_elements mint mint2 a c begin end1
-
- goal wp_goal :
- forall t:addr -> int, t1:addr -> int, t2:addr -> int, a:addr, a1:addr, i:
- int, i1:int, i2:int, i3:int.
- P_same_elements t1 t2 a a1 i i2 -> not P_same_elements t t1 a1 a i1 i3
- end
-[wp:print-generated]
- theory WP1
- (* use why3.BuiltIn.BuiltIn *)
-
- (* use bool.Bool *)
-
- (* use int.Int *)
-
- (* use int.ComputerDivision *)
-
- (* use real.RealInfix *)
-
- (* use frama_c_wp.qed.Qed *)
-
- (* use map.Map *)
-
- predicate P_is_gcd1 int int int
-
- axiom Q_gcd_zero1 : forall n:int. P_is_gcd1 n 0 n
-
- axiom Q_gcd_succ1 :
- forall a:int, b:int, d:int. P_is_gcd1 b (mod a b) d -> P_is_gcd1 a b d
-
- goal wp_goal :
- forall i:int, i1:int, i2:int. P_is_gcd1 i i1 i2 -> not P_is_gcd1 i1 i2 i
- end
-[wp:print-generated]
- theory WP2
- (* use why3.BuiltIn.BuiltIn *)
-
- (* use bool.Bool *)
-
- (* use int.Int *)
-
- (* use int.ComputerDivision *)
-
- (* use real.RealInfix *)
-
- (* use frama_c_wp.qed.Qed *)
-
- (* use map.Map *)
-
- predicate P_is_gcd2 int int int
-
- axiom Q_gcd_zero2 : forall n:int. P_is_gcd2 n 0 n
-
- axiom Q_gcd_succ2 :
- forall a:int, b:int, d:int. P_is_gcd2 b (mod a b) d -> P_is_gcd2 a b d
-
- lemma Q_test_no_label1 :
- forall a:int, b:int, d:int. P_is_gcd2 a b d -> not P_is_gcd2 b d a
-
- (* use frama_c_wp.memory.Memory *)
-
- (* use Compound *)
-
- predicate P_reachable1 (int -> int) (addr -> addr) addr addr
-
- axiom Q_root_reachable1 :
- forall malloc:int -> int, mptr:addr -> addr, root:addr.
- P_reachable1 malloc mptr root root
-
- axiom Q_next_reachable1 :
- forall malloc:int -> int, mptr:addr -> addr, root:addr, node:addr.
- valid_rw malloc root 2 ->
- P_reachable1 malloc mptr (get mptr (shiftfield_F1__list_next root)) node ->
- P_reachable1 malloc mptr root node
-
- goal wp_goal :
- forall t:int -> int, t1:addr -> addr, t2:int -> int, t3:addr -> addr, a:
- addr, a1:addr. P_reachable1 t2 t3 a a1 -> not P_reachable1 t t1 a a1
- end
-[wp] 3 goals generated
-[wp] Report in: 'tests/wp_acsl/oracle_qualif/inductive.0.report.json'
-[wp] Report out: 'tests/wp_acsl/result_qualif/inductive.0.report.json'
--------------------------------------------------------------
-Axiomatics WP Alt-Ergo Total Success
-Lemma - - 3 0.0%
--------------------------------------------------------------