diff --git a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i index 6dacd120f08fff7d2f0b954015295c7a650ca023..b00b49020602e59a42e532d69d609ffd12549dfd 100644 --- a/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i +++ b/src/plugins/wp/tests/wp_plugin/bitmask0x8000.i @@ -3,7 +3,7 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script,alt-ergo @USING_WP_SESSION@ */ diff --git a/src/plugins/wp/tests/wp_plugin/unroll.i b/src/plugins/wp/tests/wp_plugin/unroll.i index ff39035772624cd144ee6f3989a91ff352a85555..d42bda0c3d540694900bdde8c5017002b0eac26e 100644 --- a/src/plugins/wp/tests/wp_plugin/unroll.i +++ b/src/plugins/wp/tests/wp_plugin/unroll.i @@ -3,7 +3,7 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/unrolled_loop_*.json OPT: -ulevel=1 -wp-prop=@ensures -wp-prover script @USING_WP_SESSION@ */ diff --git a/src/plugins/wp/tests/wp_plugin/unsigned.i b/src/plugins/wp/tests/wp_plugin/unsigned.i index 3fcc134f879363367be687a49e514517ed975419..bdc84346f2afb07c499bbaf9706efb018fe2b163 100644 --- a/src/plugins/wp/tests/wp_plugin/unsigned.i +++ b/src/plugins/wp/tests/wp_plugin/unsigned.i @@ -3,7 +3,7 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script @USING_WP_SESSION@ */ diff --git a/src/plugins/wp/tests/wp_tip/clear.i b/src/plugins/wp/tests/wp_tip/clear.i index b86a92e0c332fdae71206a780c9591330f1e7dcb..cc1ba10ac8a54f6dfe5e85b611bda12bb0c194f0 100644 --- a/src/plugins/wp/tests/wp_tip/clear.i +++ b/src/plugins/wp/tests/wp_tip/clear.i @@ -1,5 +1,5 @@ /* run.config - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/clear_*.json OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@ */ /* run.config_qualif diff --git a/src/plugins/wp/tests/wp_tip/induction.i b/src/plugins/wp/tests/wp_tip/induction.i index 332d18f30565cbdef2880f50cdbcdcda69fb7c84..3e74960fa48709f83fefc88479d3681a106b3a92 100644 --- a/src/plugins/wp/tests/wp_tip/induction.i +++ b/src/plugins/wp/tests/wp_tip/induction.i @@ -3,11 +3,11 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@ - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@ - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@ */ diff --git a/src/plugins/wp/tests/wp_tip/induction_typing.i b/src/plugins/wp/tests/wp_tip/induction_typing.i index 6837f329d7c1c9dc889f1e7f84e9537e779dba1f..2a2771df273fb410150907a3c5168e0e0db9d9f7 100644 --- a/src/plugins/wp/tests/wp_tip/induction_typing.i +++ b/src/plugins/wp/tests/wp_tip/induction_typing.i @@ -1,5 +1,5 @@ /* run.config - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/function_*.json OPT: -wp-par 1 -wp-prop X -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@ */ /* run.config_qualif diff --git a/src/plugins/wp/tests/wp_tip/modmask.i b/src/plugins/wp/tests/wp_tip/modmask.i index 7234784f8de24f29006b3002d7720bc87d8f59ac..9437a5a3e8529f3d4fb5eaee89e6c7349a16a3a1 100644 --- a/src/plugins/wp/tests/wp_tip/modmask.i +++ b/src/plugins/wp/tests/wp_tip/modmask.i @@ -1,7 +1,7 @@ /* run.config - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/check_lemma_*.json OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@ - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/check_lemma_*.json OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@ */ /* run.config_qualif diff --git a/src/plugins/wp/tests/wp_tip/overflow.i b/src/plugins/wp/tests/wp_tip/overflow.i index 66552f291f95180cb17061d3db8bb63f4f32ea6f..d9d14829442cbd3c0ee6ae9a54f77df7059914e4 100644 --- a/src/plugins/wp/tests/wp_tip/overflow.i +++ b/src/plugins/wp/tests/wp_tip/overflow.i @@ -3,7 +3,7 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script,alt-ergo -wp-timeout 1 @USING_WP_SESSION@ */ diff --git a/src/plugins/wp/tests/wp_tip/split.i b/src/plugins/wp/tests/wp_tip/split.i index 0738e2bcd8cb0f42f4f31104855dbdfb28b7efde..f7d03a503c3723bf03e74775aa2eeaefd214ac94 100644 --- a/src/plugins/wp/tests/wp_tip/split.i +++ b/src/plugins/wp/tests/wp_tip/split.i @@ -1,5 +1,5 @@ /* run.config - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/test_*.json OPT: -wp-par 1 -wp-no-print -wp-prover qed,script -wp-msg-key script @USING_WP_SESSION@ */ /* run.config_qualif diff --git a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i index e67c1eca52fb62e9e320481912621b84934372fb..994571f3059ca385cc52505ce4f8c61aaae7bdc2 100644 --- a/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i +++ b/src/plugins/wp/tests/wp_tip/tac_split_quantifiers.i @@ -4,7 +4,7 @@ /* run.config_qualif SCRIPT: TacNOP - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/split_*.json OPT: -wp -wp-par 1 -wp-prover script @USING_WP_SESSION@ */ diff --git a/src/plugins/wp/tests/wp_tip/unroll.i b/src/plugins/wp/tests/wp_tip/unroll.i index a8c6e6defc3eb08a92035e063c87550d6920989b..7b09c6963fcd67163de0cf8fd37c18b60bf84b3e 100644 --- a/src/plugins/wp/tests/wp_tip/unroll.i +++ b/src/plugins/wp/tests/wp_tip/unroll.i @@ -3,7 +3,7 @@ */ /* run.config_qualif - DEPS: @WP_SESSION@/script/* + DEPS: @WP_SESSION@/script/lemma_*.json OPT: -wp-prover script,none @USING_WP_SESSION@ */