[WP] some more tests

src/plugins/wp/tests/wp_bts/issue_825.i

@@ -14,3 +14,8 @@ void job(void)
     i ++;
   }
 }
+void issue(int a) {
+  //@ check ko:  \exists integer j; 0 < j < 0;
+  //@ check ko: (\forall integer j; 0 < j < 0 ==> \false) ==> (a == 0);
+  ;
+}

src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle

@@ -3,6 +3,20 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
+------------------------------------------------------------
+  Function issue
+------------------------------------------------------------
+
+Goal Check 'ko' (file tests/wp_bts/issue_825.i, line 18):
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Check 'ko' (file tests/wp_bts/issue_825.i, line 19):
+Assume { Type: is_sint32(a). }
+Prove: a = 0.
+
+------------------------------------------------------------
 ------------------------------------------------------------
   Function job
 ------------------------------------------------------------

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/2e52caad3f8b8552be7c703a245947cf.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/7da8f94d00d90464616019326ebbc808.json

+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }

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

@@ -3,17 +3,20 @@
 [wp] Running WP plugin...
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
-[wp] 6 goals scheduled
+[wp] 8 goals scheduled
+[wp] [Alt-Ergo] Goal typed_issue_check_ko : Unsuccess
+[wp] [Alt-Ergo] Goal typed_issue_check_ko_2 : Unsuccess
 [wp] [Alt-Ergo] Goal typed_job_ensures : Unsuccess
 [wp] [Qed] Goal typed_job_loop_invariant_preserved : Valid
 [wp] [Qed] Goal typed_job_loop_invariant_established : Valid
 [wp] [Qed] Goal typed_job_loop_assigns_part1 : Valid
 [wp] [Alt-Ergo] Goal typed_job_loop_assigns_part2 : Unsuccess
 [wp] [Qed] Goal typed_job_assigns : Valid
-[wp] Proved goals:    4 / 6
+[wp] Proved goals:    4 / 8
   Qed:             4 
-  Alt-Ergo:        0  (unsuccess: 2)
+  Alt-Ergo:        0  (unsuccess: 4)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
   job                       4        -        6      66.7%
+  issue                     -        -        2       0.0%
 ------------------------------------------------------------