diff --git a/src/plugins/wp/wpApi.ml b/src/plugins/wp/wpApi.ml index 56a72d3c7c969d3c2fac17a00002ff8535860ff2..3fc1548fc169de1fe84307ae62cb2a98ee1706a6 100644 --- a/src/plugins/wp/wpApi.ml +++ b/src/plugins/wp/wpApi.ml @@ -117,7 +117,7 @@ struct "total", Jnumber; ]) let to_json (smoke,cs) : Json.t = - let verdict = match cs.Stats.verdict with + let verdict = match cs.Stats.best with | VCS.Valid -> if smoke then "Doomed" else "Valid" | VCS.Unknown -> if smoke then "Passed" else "Unknown" | Failed -> "Failure" @@ -125,7 +125,6 @@ struct | Computing _ -> "Computing" | Timeout -> "Timeout" | Stepout -> "Stepout" - | Invalid -> "Invalid" in let summary = Format.asprintf "%s%a" verdict (Stats.pp_stats ~shell:false ~cache:Update) cs @@ -133,7 +132,7 @@ struct "summary", `String summary ; "tactics", `Int cs.tactics ; "proved", `Int cs.proved ; - "total", `Int (Stats.proofs cs) ; + "total", `Int (Stats.subgoals cs) ; ] end diff --git a/src/plugins/wp/wpTipApi.ml b/src/plugins/wp/wpTipApi.ml index ce27c6b39a554194dbded8fbc1c5ba064538f0d3..2bceb850f9990f3d6ddfb2ddf1e26d71e08779d5 100644 --- a/src/plugins/wp/wpTipApi.ml +++ b/src/plugins/wp/wpTipApi.ml @@ -64,7 +64,7 @@ let () = set_proved rq (ProofEngine.proved node) ; set_pending rq (ProofEngine.pending node) ; let s = ProofEngine.stats node in - set_size rq (Stats.proofs s) ; + set_size rq (Stats.subgoals s) ; set_stats rq (Pretty_utils.to_string Stats.pretty s) ; end