diff --git a/nix/default.nix b/nix/default.nix
index ed3ac4e26b1a4fb95ece7fce7fd3fed5fcf088df..588b4df87e0e9a7474cfe6f0acb43687fa38274f 100644
--- a/nix/default.nix
+++ b/nix/default.nix
@@ -153,7 +153,7 @@ rec {
wp-qualif = stdenv.mkDerivation {
name = "frama-c-wp-qualif";
buildInputs = mk_buildInputs { opamPackages = [
- { name = "alt-ergo"; constraint = "=2.2.0"; }
+ { name = "alt-ergo"; constraint = "=2.0.0"; }
]; };
build_dir = main.build_dir;
src = main.build_dir + "/dir.tar";
diff --git a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
index fd2db56400cf8cbac895ebd284b904dd7f026ce1..6321440d676cbb0d589ad5932a81008fde0237f8 100644
--- a/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
+++ b/src/plugins/wp/tests/wp_gallery/binary-multiplication.c
@@ -6,7 +6,7 @@
OPT: -wp-rte -wp-prover=alt-ergo,script -wp-prop=-lack
*/
-// The use '-wp-prover=z3,why3:alt-ergo' gives better results.
+// The use '-wp-prover=z3,why3:alt-ergo' or using Alt-Ergo 2.3.0 gives better results.
typedef unsigned uint32_t ;
typedef unsigned long long uint64_t ;
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
index 9bc1b5ea726585551090d6009ad060032f867859..0c30eb6cf12b6ad09707403db775ab3eea05fc4f 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication-without-overflow.res.oracle
@@ -4,7 +4,7 @@
[wp] Loading driver 'share/wp.driver'
[rte] annotating function BinaryMultiplication
[wp] 16 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_ax1_lack : Valid
+[wp] [Alt-Ergo] Goal typed_lemma_ax1_lack : Unsuccess
[wp] [Qed] Goal typed_lemma_sizeof_ok_ok : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_ensures_product : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : Valid
@@ -20,12 +20,12 @@
[wp] [Qed] Goal typed_BinaryMultiplication_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
-[wp] Proved goals: 16 / 16
+[wp] Proved goals: 15 / 16
Qed: 3
- Alt-Ergo: 13
+ Alt-Ergo: 12 (unsuccess: 1)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
- Axiomatic mult 1 1 2 100%
+ Axiomatic mult 1 - 2 50.0%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
BinaryMultiplication 2 12 14 100%
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
index 42846ae5b12ed1ed2faf98b67be590ad269236f3..42a2b002096f5135ea54211277cd6578cc5c70f3 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.res.oracle
@@ -10,7 +10,7 @@
[wp] [Qed] Goal typed_lemma_sizeof_ok_ok : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_ensures_product : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_assert_a1_ok_deductible : Valid
-[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Valid
+[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_preserved : Unsuccess
[wp] [Qed] Goal typed_BinaryMultiplication_loop_invariant_inv1_ok_established : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_preserved : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_invariant_inv2_ok_established : Valid
@@ -21,13 +21,13 @@
[wp] [Qed] Goal typed_BinaryMultiplication_loop_assigns : Valid
[wp] [Alt-Ergo] Goal typed_BinaryMultiplication_loop_variant_decrease : Valid
[wp] [Qed] Goal typed_BinaryMultiplication_loop_variant_positive : Valid
-[wp] Proved goals: 17 / 17
+[wp] Proved goals: 16 / 17
Qed: 4
- Alt-Ergo: 13
+ Alt-Ergo: 12 (unsuccess: 1)
------------------------------------------------------------
Axiomatics WP Alt-Ergo Total Success
Axiomatic mult 1 3 4 100%
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- BinaryMultiplication 3 10 13 100%
+ BinaryMultiplication 3 9 13 92.3%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/nth.i b/src/plugins/wp/tests/wp_plugin/nth.i
index 9c53c9927da577d50605072427990d3238fbbdb0..3e5a1d4e75d247e894c07d6e09395a0d3c7bdf92 100644
--- a/src/plugins/wp/tests/wp_plugin/nth.i
+++ b/src/plugins/wp/tests/wp_plugin/nth.i
@@ -1,6 +1,5 @@
/* run.config_qualif
- OPT: -wp-prover alt-ergo -wp-prop=-lack
- OPT: -wp-prover why3:alt-ergo
+ OPT:
*/
/*@
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
index d915bad48f5005fd78456cd1dffdf1c7dbc68385..c262dc3d274019adb6a1a56a0d2125fef38d489d 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/config.res.oracle
@@ -1,7 +1,7 @@
----------------------------------------------------------
WP Requirements for Qualif Tests (3)
----------------------------------------------------------
-1. The Alt-Ergo theorem prover, version 2.3.0
+1. The Alt-Ergo theorem prover, version 2.0.0
2. The Why3 platform, version 1.3.1
3. The Coq Proof Assistant, version 8.11.1
----------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
index d488804035c965e0eb870fec18654e5612b19332..4b005c11a31b2e9dbfab45e3ecebf574424538f2 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/fallback.res.oracle
@@ -3,7 +3,7 @@
[wp] Running WP plugin...
[wp] Loading driver 'share/wp.driver'
[wp] Warning: Missing RTE guards
-[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.3.0'
+[wp] Warning: Prover 'Alt-Ergo:1.2.0' not found, fallback to 'Alt-Ergo:2.0.0'
[wp] 1 goal scheduled
[wp] [Alt-Ergo] Goal typed_job_ensures : Valid
[wp] Proved goals: 1 / 1
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle
deleted file mode 100644
index f4998e8e664dad8b6f358661e31a7b6cace7e1f6..0000000000000000000000000000000000000000
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle
+++ /dev/null
@@ -1,15 +0,0 @@
-# frama-c -wp [...]
-[kernel] Parsing tests/wp_plugin/nth.i (no preprocessing)
-[wp] Running WP plugin...
-[wp] Loading driver 'share/wp.driver'
-[wp] 3 goals scheduled
-[wp] [Alt-Ergo] Goal typed_lemma_access_16_16_ok : Valid
-[wp] [Alt-Ergo] Goal typed_lemma_access_4_4_ok : Valid
-[wp] [Qed] Goal typed_lemma_eq_repeat_concat_3_ok : Valid
-[wp] Proved goals: 3 / 3
- Qed: 1
- Alt-Ergo: 2
-------------------------------------------------------------
- Axiomatics WP Alt-Ergo Total Success
- Axiomatic Nth 1 2 3 100%
-------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
similarity index 100%
rename from src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.1.res.oracle
rename to src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.res.oracle
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
index 6752a74f6932c0be8c315866cd47a2d167bfa108..a4bc55ce426f46f0f19a9c08a38a529ac8b438f4 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/trig.res.oracle
@@ -6,12 +6,12 @@
[wp] 4 goals scheduled
[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_S : Valid
[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_A : Valid
-[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_B : Valid
+[wp] [Alt-Ergo] Goal typed_foo_assert_qed_ok_B : Unsuccess
[wp] [Qed] Goal typed_foo_call_fconcat_requires_qed_ok : Valid
-[wp] Proved goals: 4 / 4
+[wp] Proved goals: 3 / 4
Qed: 1
- Alt-Ergo: 3
+ Alt-Ergo: 2 (unsuccess: 1)
------------------------------------------------------------
Functions WP Alt-Ergo Total Success
- foo 1 3 4 100%
+ foo 1 2 4 75.0%
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
index ac9e9645d05b5e943c48e0df926808e293879219..5f8c9d742bac2cc5f5d126139c78b5e3cdb02d2d 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_exit_part2.json
@@ -2,37 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.0876,
- "steps": 51 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 9 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "i_102",
- "pattern": "$i" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 9": [ { "prover": "qed",
- "verdict": "valid" } ] } } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.015,
+ "steps": 12 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0156,
+ "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
index ac9e9645d05b5e943c48e0df926808e293879219..db21e16a1115ae542fa59c36e5e5daea1c4c9087 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_assigns_normal_part2.json
@@ -2,37 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_102) /\\ (i_1<=i_103) /\\ (0<=i_0) /\\ (i_102<=i_0) /\\ (i_103<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.0876,
- "steps": 51 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 9 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "i_102",
- "pattern": "$i" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 9": [ { "prover": "qed",
- "verdict": "valid" } ] } } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0148,
+ "steps": 12 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0149,
+ "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
index dae648761762db5157c8fda0543bbf868312682f..d93b3297e1b21a2b9cc8528244b2e10dc57927d4 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part2.json
@@ -2,37 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_9) /\\ (i_1<=i_10) /\\ (0<=i_0) /\\ (i_9<=i_0) /\\ (i_10<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.8178,
- "steps": 88 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 9 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "i_9",
- "pattern": "$i" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 9": [ { "prover": "qed",
- "verdict": "valid" } ] } } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0179,
+ "steps": 22 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0227,
+ "steps": 28 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
index cb2ffdd08270f29cdb22d37e5bf2e132068a710d..827afd22e8c9904b1f3b4541440560d074d9bfe9 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_bis_v2_loop_assigns_part3.json
@@ -2,85 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_1,i_2:int.\n(i_1<=i_0) /\\ (i_2<=i_3) /\\ (0<=i_1) /\\ (i_0<=i_1) /\\ (i_3<=i_2) /\\ (i_1<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 19 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "i_3",
- "pattern": "$i" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 10": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 11": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 12": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 13": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 14": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 15": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 16": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 17": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 18": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 19": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 19": [ { "prover": "qed",
- "verdict": "valid" } ] } } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 9 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "i_0",
- "pattern": "$i" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 9": [ { "prover": "qed",
- "verdict": "valid" } ] } } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0193,
+ "steps": 16 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0184,
+ "steps": 22 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
index 0f29709407bc0b8a2e62bf0006c6883a7684e85c..3f3ed3f304393649f3fc8e17fc9eb9d98a01b77f 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_assigns_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_156) /\\ (i_1<=i_157) /\\ (0<=i_0) /\\ (i_156<=i_0) /\\ (i_157<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.0318,
- "steps": 39 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.562,
- "steps": 414 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0078,
+ "steps": 9 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.008,
+ "steps": 11 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
index 88270611f30de89ca035c371d975b464637ab1bf..a44fae8d4af0fd64e6010c96f9f5984a219f38dc 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part2.json
@@ -2,37 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.6393,
- "steps": 63 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 9 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "i_13",
- "pattern": "$i" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 9": [ { "prover": "qed",
- "verdict": "valid" } ] } } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0148,
+ "steps": 22 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0157,
+ "steps": 24 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
index e2ed0ca2fb06d4355bb996f43ff0769bc9d999ce..b52da31442d64b9e14d8852de77d9f024048b36c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_2_part3.json
@@ -2,85 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_2:int.\n(i_0<=i_1) /\\ (0<=i_0) /\\ (i_1<=i_0) /\\ (j_0<=i_2) /\\ (i_2<=j_0) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i0#1$i#1$j#0" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 19 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "j_0",
- "pattern": "$j" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 10": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 11": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 12": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 13": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 14": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 15": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 16": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 17": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 18": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 19": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 19": [ { "prover": "qed",
- "verdict": "valid" } ] } } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 9 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "i_1",
- "pattern": "$i" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 9": [ { "prover": "qed",
- "verdict": "valid" } ] } } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0105,
+ "steps": 14 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0144,
+ "steps": 16 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
index bb9877d0edec46bfc076a60c8fec6e40a38d39dd..af38ce7e80b446ee46f0b0d03697a2f0e5b68151 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part2.json
@@ -2,37 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_21) /\\ (i_1<=i_22) /\\ (0<=i_0) /\\ (i_21<=i_0) /\\ (i_22<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.4508,
- "steps": 55 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 9 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "i_21",
- "pattern": "$i" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 9": [ { "prover": "qed",
- "verdict": "valid" } ] } } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0143,
+ "steps": 18 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.015,
+ "steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
index bc59c057755459f749de24cab6d58ac381fc28e6..1b85707f2bf3d68f368dd6c1e48d767387eb7973 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v2_loop_assigns_part3.json
@@ -2,37 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_8) /\\ (i_1<=i_9) /\\ (0<=i_0) /\\ (i_8<=i_0) /\\ (i_9<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.4508,
- "steps": 55 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 9 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "i_8",
- "pattern": "$i" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 9": [ { "prover": "qed",
- "verdict": "valid" } ] } } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0148,
+ "steps": 18 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0153,
+ "steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
index c128ee8585d1150eee8299f9655216d8f870f3e3..dd37abbd3efef97827a1c8cf3d0d6ab89d9965ea 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_assigns_part2.json
@@ -2,9 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_148) /\\ (i_1<=i_149) /\\ (0<=i_0) /\\ (i_148<=i_0) /\\ (i_149<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.0318,
- "steps": 39 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.562,
- "steps": 414 } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0079,
+ "steps": 9 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0082,
+ "steps": 11 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
index a233cfc63116980ec3afdda54cf88447e3faf3e3..e576684bbcd49f308ca2e2e7db841764ef15b6a9 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part2.json
@@ -2,37 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_13) /\\ (i_1<=i_14) /\\ (0<=i_0) /\\ (i_13<=i_0) /\\ (i_14<=i_1)\n/\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "valid", "time": 0.3477,
- "steps": 70 } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 9 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "i_13",
- "pattern": "$i" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 9": [ { "prover": "qed",
- "verdict": "valid" } ] } } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0139,
+ "steps": 23 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0168,
+ "steps": 27 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
index 7ddd11a4d437cfef3f03a5554b025094c9eb022e..29b715f01c2b1393aeb89cb3a7c98efb56f73d2e 100644
--- a/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
+++ b/src/plugins/wp/tests/wp_typed/oracle_qualif/user_init.1.session/script/init_t2_v3_loop_assigns_part3.json
@@ -2,85 +2,9 @@
"select": { "select": "clause-goal",
"target": "exists i_0,i_1:int.\n(i_0<=i_4) /\\ (i_1<=i_6) /\\ (0<=i_0) /\\ (i_4<=i_0) /\\ (i_6<=i_1) /\\ (i_0<=9)",
"pattern": "\\E\\E&<=<=<=<=<=<=#1$i#0$i0#1$i#1" },
- "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 19 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "i_6",
- "pattern": "$i" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 10": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 11": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 12": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 13": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 14": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 15": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 16": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 17": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 18": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 19": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 19": [ { "prover": "qed",
- "verdict": "valid" } ] } } ],
- "Goal 2/2": [ { "prover": "Alt-Ergo:2.3.0",
- "verdict": "timeout", "time": 10. },
- { "header": "Range", "tactic": "Wp.range",
- "params": { "inf": 0, "sup": 9 },
- "select": { "select": "inside-goal",
- "occur": 0, "target": "i_4",
- "pattern": "$i" },
- "children": { "Lower 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 0": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 1": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 2": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 3": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 4": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 5": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 6": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 7": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 8": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Value 9": [ { "prover": "qed",
- "verdict": "valid" } ],
- "Upper 9": [ { "prover": "qed",
- "verdict": "valid" } ] } } ] } } ]
+ "children": { "Goal 1/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0143,
+ "steps": 17 } ],
+ "Goal 2/2": [ { "prover": "Alt-Ergo:2.0.0",
+ "verdict": "valid", "time": 0.0148,
+ "steps": 21 } ] } } ]