diff --git a/src/plugins/wp/tests/wp_bts/issue_825.i b/src/plugins/wp/tests/wp_bts/issue_825.i
index b4c514fccc8a01fa1619db4a0113f0f09d11b58d..3810f22f258670830a5d6e468af2993ecdbbf394 100644
--- a/src/plugins/wp/tests/wp_bts/issue_825.i
+++ b/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);
+ ;
+}
diff --git a/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle b/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
index c6a5972a861a52e3690a6835f88f29ee5ab6c152..65c234448ba7d4d4dff459d117eb43ab42bf7ee7 100644
--- a/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
+++ b/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
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/2e52caad3f8b8552be7c703a245947cf.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/2e52caad3f8b8552be7c703a245947cf.json
new file mode 100644
index 0000000000000000000000000000000000000000..56c395504289168c539ec44e6877a919ac85adc8
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/2e52caad3f8b8552be7c703a245947cf.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "unknown" }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/7da8f94d00d90464616019326ebbc808.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/7da8f94d00d90464616019326ebbc808.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/7da8f94d00d90464616019326ebbc808.json
@@ -0,0 +1 @@
+{ "prover": "Alt-Ergo:2.0.0", "verdict": "timeout", "time": 10. }
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
index 84d7a31b97c2f8ea8ea417ae009be4530ddc85de..35895046c313f3c5b9afccb4df714ce09f77ecc0 100644
--- a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
+++ b/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%
------------------------------------------------------------