From c5abda21721dc83729b137a8ecf19c0d0cfea23f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Mon, 11 May 2020 10:18:32 +0200
Subject: [PATCH] [wp] fix some issues with Alt-Ergo
---
nix/default.nix | 2 +-
.../tests/wp_gallery/binary-multiplication.c | 2 +-
...multiplication-without-overflow.res.oracle | 8 +-
.../binary-multiplication.res.oracle | 8 +-
src/plugins/wp/tests/wp_plugin/nth.i | 3 +-
.../wp_plugin/oracle_qualif/config.res.oracle | 2 +-
.../oracle_qualif/fallback.res.oracle | 2 +-
.../wp_plugin/oracle_qualif/nth.0.res.oracle | 15 ----
.../{nth.1.res.oracle => nth.res.oracle} | 0
.../wp_plugin/oracle_qualif/trig.res.oracle | 8 +-
.../init_t2_bis_v2_assigns_exit_part2.json | 40 ++-------
.../init_t2_bis_v2_assigns_normal_part2.json | 40 ++-------
.../init_t2_bis_v2_loop_assigns_part2.json | 40 ++-------
.../init_t2_bis_v2_loop_assigns_part3.json | 88 ++-----------------
.../script/init_t2_v2_assigns_part2.json | 12 +--
.../init_t2_v2_loop_assigns_2_part2.json | 40 ++-------
.../init_t2_v2_loop_assigns_2_part3.json | 88 ++-----------------
.../script/init_t2_v2_loop_assigns_part2.json | 40 ++-------
.../script/init_t2_v2_loop_assigns_part3.json | 40 ++-------
.../script/init_t2_v3_assigns_part2.json | 12 +--
.../script/init_t2_v3_loop_assigns_part2.json | 40 ++-------
.../script/init_t2_v3_loop_assigns_part3.json | 88 ++-----------------
22 files changed, 89 insertions(+), 529 deletions(-)
delete mode 100644 src/plugins/wp/tests/wp_plugin/oracle_qualif/nth.0.res.oracle
rename src/plugins/wp/tests/wp_plugin/oracle_qualif/{nth.1.res.oracle => nth.res.oracle} (100%)
diff --git a/nix/default.nix b/nix/default.nix
index ed3ac4e26b1..588b4df87e0 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 fd2db56400c..6321440d676 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 9bc1b5ea726..0c30eb6cf12 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 42846ae5b12..42a2b002096 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 9c53c9927da..3e5a1d4e75d 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 d915bad48f5..c262dc3d274 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 d488804035c..4b005c11a31 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 f4998e8e664..00000000000
--- 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 6752a74f693..a4bc55ce426 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 ac9e9645d05..5f8c9d742ba 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 ac9e9645d05..db21e16a111 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 dae64876176..d93b3297e1b 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 cb2ffdd0827..827afd22e8c 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 0f29709407b..3f3ed3f3043 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 88270611f30..a44fae8d4af 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 e2ed0ca2fb0..b52da31442d 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 bb9877d0ede..af38ce7e80b 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 bc59c057755..1b85707f2bf 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 c128ee8585d..dd37abbd3ef 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 a233cfc6311..e576684bbcd 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 7ddd11a4d43..29b715f01c2 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 } ] } } ]
--
GitLab