From 6ab7dfb7192c7495b55b83d6e7a407939238024a Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Loi=CC=88c=20Correnson?= <loic.correnson@cea.fr>
Date: Wed, 7 Jun 2023 16:39:00 +0200
Subject: [PATCH] [wp] fix errors in stats
---
src/plugins/wp/Cache.ml | 3 +-
src/plugins/wp/ProofEngine.ml | 16 +++--
src/plugins/wp/ProverScript.ml | 61 +++++++++----------
src/plugins/wp/Stats.ml | 2 +-
src/plugins/wp/register.ml | 2 +-
.../oracle_qualif/unsigned.res.oracle | 2 +-
.../wp/tests/wp_tip/oracle/clear.res.oracle | 4 +-
.../wp_tip/oracle/induction_typing.res.oracle | 2 +-
.../wp/tests/wp_tip/oracle/split.res.oracle | 46 +++++++-------
.../oracle_qualif/induction.1.res.oracle | 2 +-
.../oracle_qualif/induction.2.res.oracle | 2 +-
.../oracle_qualif/strategy.0.res.oracle | 1 +
.../oracle_qualif/strategy.1.res.oracle | 2 +-
.../oracle_qualif/strategy.2.res.oracle | 2 +-
.../oracle_qualif/strategy.3.res.oracle | 2 +-
.../tac_split_quantifiers.res.oracle | 10 +--
16 files changed, 81 insertions(+), 78 deletions(-)
diff --git a/src/plugins/wp/Cache.ml b/src/plugins/wp/Cache.ml
index 247f0324a9f..f5867c9db28 100644
--- a/src/plugins/wp/Cache.ml
+++ b/src/plugins/wp/Cache.ml
@@ -156,8 +156,7 @@ let steps_seized steps steplimit =
let promote ?timeout ?steplimit (res : VCS.result) =
match res.verdict with
- | VCS.NoResult | VCS.Computing _ -> VCS.no_result
- | VCS.Failed -> res
+ | VCS.NoResult | VCS.Computing _ | VCS.Failed -> VCS.no_result
| VCS.Invalid | VCS.Valid | VCS.Unknown ->
if not (steps_fits res.prover_steps steplimit) then
{ res with verdict = Stepout }
diff --git a/src/plugins/wp/ProofEngine.ml b/src/plugins/wp/ProofEngine.ml
index d597ee19979..89a4bbb2c96 100644
--- a/src/plugins/wp/ProofEngine.ml
+++ b/src/plugins/wp/ProofEngine.ml
@@ -153,13 +153,20 @@ let pending n =
let k = ref 0 in
walk (fun _ -> incr k) n ; !k
+let is_prover_result (p,_) = p <> VCS.Tactical
+
+let prover_stats goal =
+ Stats.results ~smoke:(Wpo.is_smoke_test goal) @@
+ List.filter is_prover_result @@
+ Wpo.get_results goal
+
let rec consolidate n =
let s =
if Wpo.is_valid n.goal then
- Stats.results ~smoke:false (Wpo.get_results n.goal)
+ prover_stats n.goal
else
match n.script with
- | Opened | Script _ -> Stats.empty
+ | Opened | Script _ -> prover_stats n.goal
| Tactic(_,children) ->
let qed = Wpo.qed_time n.goal in
let results = List.map (fun (_,n) -> consolidate n) children in
@@ -175,15 +182,12 @@ let validate tree =
Wpo.set_result tree.main Tactical (Stats.script stats)
let consolidated wpo =
- let smoke = Wpo.is_smoke_test wpo in
- let prs = Wpo.get_results wpo in
try
if Wpo.is_smoke_test wpo || not (PROOFS.mem wpo) then raise Not_found ;
match PROOFS.get wpo with
| { root = Some { stats ; script = Tactic _ } } -> stats
| _ -> raise Not_found
- with Not_found ->
- Stats.results ~smoke prs
+ with Not_found -> prover_stats wpo
(* -------------------------------------------------------------------------- *)
(* --- Accessors --- *)
diff --git a/src/plugins/wp/ProverScript.ml b/src/plugins/wp/ProverScript.ml
index feb73306307..9494a3040b2 100644
--- a/src/plugins/wp/ProverScript.ml
+++ b/src/plugins/wp/ProverScript.ml
@@ -119,6 +119,7 @@ struct
width : int ;
auto : Strategy.heuristic list ; (* DEPRECATED *)
strategies : bool ;
+ mutable pending : int ; (* pending jobs *)
mutable signaled : bool ;
backtrack : int ;
mutable backtracking : backtracking option ;
@@ -139,20 +140,12 @@ struct
let progress env msg = env.progress (ProofEngine.main env.tree) msg
- let stuck env =
- if not env.signaled then
- begin
- ProofEngine.validate env.tree ;
- env.success (ProofEngine.main env.tree) None ;
- env.signaled <- true ;
- end
-
- let validate ?(finalize=false) env =
+ let validate env =
ProofEngine.validate env.tree ;
if not env.signaled then
let wpo = ProofEngine.main env.tree in
- let proved = Wpo.is_valid wpo in
- if proved || finalize then
+ let proved = Wpo.is_passed wpo in
+ if proved || env.pending = 0 then
begin
env.signaled <- true ;
List.iter
@@ -223,7 +216,7 @@ struct
~valid ~failed ~provers ~strategies
~depth ~width ~backtrack ~auto
~progress ~result ~success =
- { tree ; valid ; failed ; provers ;
+ { tree ; valid ; failed ; provers ; pending = 0 ;
depth ; width ; backtrack ; auto ; strategies ;
progress ; result ; success ;
backtracking = None ;
@@ -313,7 +306,7 @@ and autofork env ~depth fork =
forall (auto env ~depth) (List.map snd children)
end
else
- ( Env.validate env ; Task.return true )
+ Task.return true
(* -------------------------------------------------------------------------- *)
(* --- Proof Strategy Alternatives --- *)
@@ -430,9 +423,7 @@ let rec crawl env on_child node = function
| [] ->
let node = ProofEngine.anchor (Env.tree env) ?node () in
- automated env on_child node >>= fun ok ->
- if ok then Env.validate env else Env.stuck env ;
- Task.return ()
+ automated env on_child node
| Error(msg,json) :: alternatives ->
Wp_parameters.warning "@[<hov 2>Script Error: on goal %a@\n%S: %a@]@."
@@ -450,7 +441,7 @@ let rec crawl env on_child node = function
else Task.return false in
let continue ok =
if ok
- then (Env.validate env ; Task.return ())
+ then success
else crawl env on_child node alternatives
in
task >>= continue
@@ -460,11 +451,8 @@ let rec crawl env on_child node = function
begin
try
let residual = apply env node jtactic subscripts in
- if residual = [] then
- Env.validate env
- else
- List.iter (fun (_,n) -> on_child n) residual ;
- Task.return ()
+ List.iter (fun (_,n) -> on_child n) residual ;
+ Task.return true
with exn when Wp_parameters.protect exn ->
Wp_parameters.warning
"Script Error: on goal %a@\n\
@@ -493,14 +481,24 @@ let schedule job =
Task.spawn (ProverTask.server ()) (Task.thread (Task.todo job))
let rec process env node =
+ env.Env.pending <- succ env.Env.pending ;
schedule
begin fun () ->
Wp_parameters.debug ~dkey:dkey_pp_allgoals "%a" (pp_subgoal env) node ;
if ProofEngine.proved node then
- ( Env.validate env ; Task.return () )
+ begin
+ env.pending <- pred env.pending ;
+ Env.validate env ;
+ Task.return () ;
+ end
else
let script = Priority.sort (ProofEngine.bound node) in
- crawl env (process env) (Some node) script
+ crawl env (process env) (Some node) script >>=
+ begin fun _ ->
+ env.pending <- pred env.pending ;
+ Env.validate env ;
+ Task.return ()
+ end
end
let task
@@ -523,8 +521,10 @@ let task
~valid ~failed ~provers
~depth ~width ~backtrack ~auto ~strategies
~progress ~result ~success in
- crawl env (process env) None script >>?
- (fun _ -> ProofEngine.forward tree) ;
+ crawl env (process env) None script >>= fun _ ->
+ Env.validate env ;
+ ProofEngine.forward tree ;
+ Task.return ()
end
(* -------------------------------------------------------------------------- *)
@@ -579,9 +579,8 @@ let search
~progress ~result ~success in
schedule
begin fun () ->
- autosearch env ~depth:0 node >>=
- fun ok ->
- if ok then Env.validate ~finalize:true env else Env.stuck env ;
+ autosearch env ~depth:0 node >>= fun _ ->
+ Env.validate env ;
Task.return ()
end
end
@@ -602,8 +601,8 @@ let explore ?(depth=0) ?(strategy)
match strategy with
| None -> explore_hints env (process env)
| Some s -> explore_strategy env (fun _ -> ()) s
- in solver node >>= fun ok ->
- if ok then Env.validate ~finalize:true env else Env.stuck env ;
+ in solver node >>= fun _ ->
+ Env.validate env ;
Task.return ()
end
end
diff --git a/src/plugins/wp/Stats.ml b/src/plugins/wp/Stats.ml
index 50449ec8a3b..4b24c8f82fb 100644
--- a/src/plugins/wp/Stats.ml
+++ b/src/plugins/wp/Stats.ml
@@ -133,7 +133,7 @@ let consolidated = function
cs_trivial = 0 ;
cs_cached = 0 ;
cs_provers = [] }
- | u::w as results ->
+ | (u::w) as results ->
let (p,r) as pr = List.fold_left choose_best u w in
let trivial = is_trivial pr in
let cached = not trivial && List.for_all is_cached results in
diff --git a/src/plugins/wp/register.ml b/src/plugins/wp/register.ml
index 3b5f932999a..88e7725affd 100644
--- a/src/plugins/wp/register.ml
+++ b/src/plugins/wp/register.ml
@@ -353,7 +353,7 @@ let do_report_stats ~shell ~cache ~smoke goal (stats : Stats.stats) =
if smoke then
match stats.verdict with
| Valid -> "[Failed] (Doomed)"
- | Failed -> "[Unknown] (Failure)"
+ | Failed -> "[Failure] (Solver Error)"
| NoResult | Computing _ -> "[Unknown] (Incomplete)"
| (Unknown | Timeout | Stepout) when shell -> "[Passed] (Unsuccess)"
| Unknown -> "[Passed] (Unknown)"
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
index 45759f9d1ab..43ce8fab823 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unsigned.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing unsigned.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
-[wp] [Unsuccess] typed_lemma_U32 (Tactic)
+[wp] [Unsuccess] typed_lemma_U32 (Tactic) (Qed 1/2) (Cache miss 1)
[wp] Proved goals: 0 / 1
Unsuccess: 1
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
index c5e19ea143c..df8ab558675 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/clear.res.oracle
@@ -105,7 +105,7 @@
Prove: P_S(42).
------------------------------------------------------------
-[wp] [Unsuccess] typed_clear_in_step_check (Tactics 3)
+[wp] [Unsuccess] typed_clear_in_step_check (Tactics 3) (Cached)
[wp:script:allgoals]
typed_clear_ensures subgoal:
@@ -143,6 +143,6 @@
Prove: P_S(a + b).
------------------------------------------------------------
-[wp] [Unsuccess] typed_clear_ensures (Tactics 7)
+[wp] [Unsuccess] typed_clear_ensures (Tactics 7) (Cached)
[wp] Proved goals: 0 / 2
Unsuccess: 2
diff --git a/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
index 525e7f8c164..8ac7d4b65c8 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/induction_typing.res.oracle
@@ -54,7 +54,6 @@
Prove: false.
------------------------------------------------------------
-[wp] [Unsuccess] typed_function_loop_invariant_X_preserved (Tactic)
[wp:script:allgoals]
typed_function_loop_invariant_X_preserved subgoal:
@@ -115,6 +114,7 @@
Prove: ([ 1 ] *^ n) = a_1.
------------------------------------------------------------
+[wp] [Unsuccess] typed_function_loop_invariant_X_preserved (Tactic) (Cached)
[wp] Proved goals: 1 / 2
Qed: 1
Unsuccess: 1
diff --git a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
index 842c6408c91..8ce73ffc5be 100644
--- a/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle/split.res.oracle
@@ -201,7 +201,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_branch_ensures (Tactic)
[wp:script:allgoals]
typed_test_step_branch_ensures subgoal:
@@ -216,6 +215,7 @@
Prove: P_S.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_step_branch_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_step_or_ensures subgoal:
@@ -224,7 +224,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_or_ensures (Tactic)
[wp:script:allgoals]
typed_test_step_or_ensures subgoal:
@@ -241,6 +240,7 @@
Prove: P_S.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_step_or_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_step_and_ensures subgoal:
@@ -256,7 +256,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_and_ensures (Tactic)
+[wp] [Unsuccess] typed_test_step_and_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_step_peq_ensures subgoal:
@@ -265,7 +265,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_peq_ensures (Tactic)
[wp:script:allgoals]
typed_test_step_peq_ensures subgoal:
@@ -274,6 +273,7 @@
Prove: P_S.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_step_peq_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_step_pneq_ensures subgoal:
@@ -282,7 +282,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_pneq_ensures (Tactic)
[wp:script:allgoals]
typed_test_step_pneq_ensures subgoal:
@@ -291,6 +290,7 @@
Prove: P_S.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_step_pneq_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_step_neq_ensures subgoal:
@@ -299,7 +299,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_neq_ensures (Tactic)
[wp:script:allgoals]
typed_test_step_neq_ensures subgoal:
@@ -316,6 +315,7 @@
Prove: P_S.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_step_neq_ensures (Tactic) (Qed 1/3) (Cached)
[wp:script:allgoals]
typed_test_step_leq_ensures subgoal:
@@ -324,7 +324,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_leq_ensures (Tactic)
[wp:script:allgoals]
typed_test_step_leq_ensures subgoal:
@@ -340,6 +339,7 @@
Prover Qed returns Valid
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_step_leq_ensures (Tactic) (Qed 1/3) (Cached)
[wp:script:allgoals]
typed_test_step_lt_ensures subgoal:
@@ -354,7 +354,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_lt_ensures (Tactic)
[wp:script:allgoals]
typed_test_step_lt_ensures subgoal:
@@ -370,6 +369,7 @@
Prover Qed returns Valid
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_step_lt_ensures (Tactic) (Qed 1/3) (Cached)
[wp:script:allgoals]
typed_test_step_if_ensures subgoal:
@@ -379,7 +379,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_if_ensures (Tactic)
[wp:script:allgoals]
typed_test_step_if_ensures subgoal:
@@ -392,6 +391,7 @@
Prove: P_S.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_step_if_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_step_fa_if_ensures subgoal:
@@ -405,7 +405,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_fa_if_ensures (Tactic)
[wp:script:allgoals]
typed_test_step_fa_if_ensures subgoal:
@@ -419,6 +418,7 @@
Prove: P_S.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_step_fa_if_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_step_fa_or_ensures subgoal:
@@ -427,7 +427,6 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_fa_or_ensures (Tactic)
[wp:script:allgoals]
typed_test_step_fa_or_ensures subgoal:
@@ -436,6 +435,7 @@
Prove: P_S.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_step_fa_or_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_step_fa_and_ensures subgoal:
@@ -448,7 +448,7 @@
Prove: P_S.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_step_fa_and_ensures (Tactic)
+[wp] [Unsuccess] typed_test_step_fa_and_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_inside_leq_ensures subgoal:
@@ -463,7 +463,6 @@
Prove: P_Q.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_inside_leq_ensures (Tactic)
[wp:script:allgoals]
typed_test_inside_leq_ensures subgoal:
@@ -480,6 +479,7 @@
Prover Qed returns Valid
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_inside_leq_ensures (Tactic) (Qed 1/3) (Cached)
[wp:script:allgoals]
typed_test_inside_lt_ensures subgoal:
@@ -494,7 +494,6 @@
Prove: P_Q.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_inside_lt_ensures (Tactic)
[wp:script:allgoals]
typed_test_inside_lt_ensures subgoal:
@@ -511,6 +510,7 @@
Prover Qed returns Valid
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_inside_lt_ensures (Tactic) (Qed 1/3) (Cached)
[wp:script:allgoals]
typed_test_inside_neq_ensures subgoal:
@@ -525,7 +525,6 @@
Prove: P_Q.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_inside_neq_ensures (Tactic)
[wp:script:allgoals]
typed_test_inside_neq_ensures subgoal:
@@ -548,6 +547,7 @@
Prove: P_Q.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_inside_neq_ensures (Tactic) (Qed 1/3) (Cached)
[wp:script:allgoals]
typed_test_goal_and_ensures subgoal:
@@ -556,7 +556,6 @@
Prove: P_P.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_and_ensures (Tactic)
[wp:script:allgoals]
typed_test_goal_and_ensures subgoal:
@@ -573,6 +572,7 @@
Prove: P_R.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_goal_and_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_goal_eq_ensures subgoal:
@@ -581,7 +581,6 @@
Prove: (L_LP=true).
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_eq_ensures (Tactic)
[wp:script:allgoals]
typed_test_goal_eq_ensures subgoal:
@@ -590,6 +589,7 @@
Prove: (L_LQ=true).
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_goal_eq_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_goal_neq_ensures subgoal:
@@ -598,7 +598,6 @@
Prove: (L_LP=false).
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_neq_ensures (Tactic)
[wp:script:allgoals]
typed_test_goal_neq_ensures subgoal:
@@ -607,6 +606,7 @@
Prove: (L_LQ=false).
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_goal_neq_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_goal_if_ensures subgoal:
@@ -620,7 +620,6 @@
Prove: P_P.
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_if_ensures (Tactic)
[wp:script:allgoals]
typed_test_goal_if_ensures subgoal:
@@ -634,6 +633,7 @@
Prove: P_Q.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_goal_if_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_goal_ex_and_ensures subgoal:
@@ -642,7 +642,6 @@
Prove: exists i : Z. P_Pi(i) /\ P_Qi(i).
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_ex_and_ensures (Tactic)
[wp:script:allgoals]
typed_test_goal_ex_and_ensures subgoal:
@@ -651,6 +650,7 @@
Prove: P_P /\ P_Q.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_goal_ex_and_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_goal_ex_or_ensures subgoal:
@@ -659,7 +659,7 @@
Prove: P_P \/ P_Q \/ (exists i : Z. P_Pi(i)) \/ (exists i : Z. P_Qi(i)).
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_ex_or_ensures (Tactic)
+[wp] [Unsuccess] typed_test_goal_ex_or_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_goal_ex_if_ensures subgoal:
@@ -674,7 +674,6 @@
Prove: exists i : Z. P_Pi(i) /\ P_Qi(i).
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_ex_if_ensures (Tactic)
[wp:script:allgoals]
typed_test_goal_ex_if_ensures subgoal:
@@ -689,6 +688,7 @@
Prove: P_P /\ P_Q.
------------------------------------------------------------
+[wp] [Unsuccess] typed_test_goal_ex_if_ensures (Tactic) (Cached)
[wp:script:allgoals]
typed_test_goal_ex_imply_ensures subgoal:
@@ -702,6 +702,6 @@
Prove: exists i : Z. P_Qi(i).
------------------------------------------------------------
-[wp] [Unsuccess] typed_test_goal_ex_imply_ensures (Tactic)
+[wp] [Unsuccess] typed_test_goal_ex_imply_ensures (Tactic) (Cached)
[wp] Proved goals: 0 / 23
Unsuccess: 23
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle
index 9df7047dfa8..84e63024f8e 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.1.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing induction.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
-[wp] [Unsuccess] typed_lemma_ByInd (Tactic)
+[wp] [Unsuccess] typed_lemma_ByInd (Tactic) (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 1
Unsuccess: 1
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle
index 9df7047dfa8..84e63024f8e 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.2.res.oracle
@@ -2,7 +2,7 @@
[kernel] Parsing induction.i (no preprocessing)
[wp] Running WP plugin...
[wp] 1 goal scheduled
-[wp] [Unsuccess] typed_lemma_ByInd (Tactic)
+[wp] [Unsuccess] typed_lemma_ByInd (Tactic) (Alt-Ergo) (Cached)
[wp] Proved goals: 0 / 1
Unsuccess: 1
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.0.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.0.res.oracle
index 0bcfae5a929..77beeea6b77 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.0.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.0.res.oracle
@@ -20,6 +20,7 @@ Assume {
}
Prove: P_P(to_sint32(t + to_uint32(z + to_uint32(x + y)))).
Prover Alt-Ergo returns Unsuccess
+Prover Script returns Unsuccess
------------------------------------------------------------
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.1.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.1.res.oracle
index a439255effc..c4fd1d0306e 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.1.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.1.res.oracle
@@ -4,7 +4,7 @@
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_target_assigns (Qed)
-[wp] [Unsuccess] typed_target_ensures (Tactics 13)
+[wp] [Unsuccess] typed_target_ensures (Tactics 13) (Alt-Ergo 26/27) (Cached)
[wp] Proved goals: 1 / 2
Qed: 1
Unsuccess: 1
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.2.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.2.res.oracle
index ca5793fb1a1..e5f1d01e1af 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.2.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.2.res.oracle
@@ -4,7 +4,7 @@
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_target_assigns (Qed)
-[wp] [Unsuccess] typed_target_ensures (Tactics 3) (Alt-Ergo 4/4) (Cached)
+[wp] [Unsuccess] typed_target_ensures (Tactics 3) (Alt-Ergo 6/7) (Cached)
[wp] Proved goals: 1 / 2
Qed: 1
Unsuccess: 1
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.3.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.3.res.oracle
index ad30c792620..5ab1dd34d91 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.3.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/strategy.3.res.oracle
@@ -4,7 +4,7 @@
[wp] Warning: Missing RTE guards
[wp] 2 goals scheduled
[wp] [Valid] typed_target_assigns (Qed)
-[wp] [Unsuccess] typed_target_ensures (Tactics 3) (Alt-Ergo 4/4) (Cached)
+[wp] [Unsuccess] typed_target_ensures (Tactics 3) (Alt-Ergo 6/7) (Cached)
[wp] Proved goals: 1 / 2
Qed: 1
Unsuccess: 1
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
index 78efb6216be..612e769d605 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/tac_split_quantifiers.res.oracle
@@ -3,11 +3,11 @@
[wp] Running WP plugin...
[wp] Warning: Missing RTE guards
[wp] 5 goals scheduled
-[wp] [Unsuccess] typed_split_ensures_Goal_Exist_Or (Tactic)
-[wp] [Unsuccess] typed_split_ensures_Goal_Exist_And (Tactic)
-[wp] [Unsuccess] typed_split_ensures_Goal_Exist_And_bis (Tactic)
-[wp] [Unsuccess] typed_split_ensures_Hyp_Forall_And (Tactic)
-[wp] [Unsuccess] typed_split_ensures_Hyp_Forall_Or_bis (Tactic)
+[wp] [Unsuccess] typed_split_ensures_Goal_Exist_Or (Tactic) (Cache miss 1)
+[wp] [Unsuccess] typed_split_ensures_Goal_Exist_And (Tactic) (Cache miss 2)
+[wp] [Unsuccess] typed_split_ensures_Goal_Exist_And_bis (Tactic) (Cache miss 3)
+[wp] [Unsuccess] typed_split_ensures_Hyp_Forall_And (Tactic) (Cache miss 1)
+[wp] [Unsuccess] typed_split_ensures_Hyp_Forall_Or_bis (Tactic) (Cache miss 3)
[wp] Proved goals: 0 / 5
Unsuccess: 5
------------------------------------------------------------
--
GitLab