[wp] discard trivial tasks

src/plugins/wp/ProverWhy3.ml

@@ -1282,7 +1282,7 @@ let prove ?timeout ?steplimit ~prover wpo =
         then Task.return VCS.no_result (* Only generate *)
         else
           let drv , config , task = prover_task prover task in
-          if false && is_trivial task then
+          if is_trivial task then
             Task.return VCS.valid
           else
             let mode = get_mode () in

src/plugins/wp/tests/wp_acsl/oracle_qualif/e_imply.res.oracle

@@ -53,5 +53,5 @@
 [wp] Report out: 'tests/wp_acsl/result_qualif/e_imply.0.report.json'
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
-f                    8     34 (1..8)        42       100%
+f                    8     34               42       100%
 -------------------------------------------------------------

src/plugins/wp/tests/wp_acsl/oracle_qualif/sizeof.0.report.json

 { "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 2, "valid": 2, "rank": 0 },
                  "wp:main": { "total": 2, "valid": 2, "rank": 1 } },
   "wp:functions": { "foo": { "foo_assert_B": { "why3:Alt-Ergo,2.0.0": 
-                                                 { "total": 1, "valid": 1,
-                                                   "rank": 0 },
+                                                 { "total": 1, "valid": 1 },
                                                "wp:main": { "total": 1,
-                                                            "valid": 1,
-                                                            "rank": 1 } },
+                                                            "valid": 1 } },
                              "foo_assert_A": { "why3:Alt-Ergo,2.0.0": 
                                                  { "total": 1, "valid": 1,
                                                    "rank": 0 },

src/plugins/wp/tests/wp_bts/oracle_qualif/bts0843.res.oracle

@@ -16,5 +16,5 @@
 -------------------------------------------------------------
 Functions           WP     Alt-Ergo        Total   Success
 f3                   1     -                 1       100%
-g3                   1      2 (1..12)        3       100%
+g3                   1      2                3       100%
 -------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.0.report.json

-{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1, "rank": 0 },
-                 "wp:main": { "total": 1, "valid": 1, "rank": 1 } },
+{ "wp:global": { "why3:Alt-Ergo,2.0.0": { "total": 1, "valid": 1 },
+                 "wp:main": { "total": 1, "valid": 1 } },
   "wp:axiomatics": { "": { "lemma_foo": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                   "valid": 1,
-                                                                   "rank": 0 },
+                                                                   "valid": 1 },
                                           "wp:main": { "total": 1,
-                                                       "valid": 1,
-                                                       "rank": 1 } },
+                                                       "valid": 1 } },
                            "wp:section": { "why3:Alt-Ergo,2.0.0": { "total": 1,
-                                                                    "valid": 1,
-                                                                    "rank": 0 },
+                                                                    "valid": 1 },
                                            "wp:main": { "total": 1,
-                                                        "valid": 1,
-                                                        "rank": 1 } } } } }
+                                                        "valid": 1 } } } } }

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_447.res.oracle

@@ -11,5 +11,5 @@
 [wp] Report out: 'tests/wp_bts/result_qualif/issue_447.0.report.json'
 -------------------------------------------------------------
 Axiomatics          WP     Alt-Ergo        Total   Success
-Lemma               -       1 (1..12)        1       100%
+Lemma               -       1                1       100%
 -------------------------------------------------------------