diff --git a/src/plugins/wp/Cint.ml b/src/plugins/wp/Cint.ml
index dbd70d5fa0db7f7e5bd91e0c2dd30fa3692d58c2..ab9d1aaa714c09cae2ff0019e63ee05542569669 100644
--- a/src/plugins/wp/Cint.ml
+++ b/src/plugins/wp/Cint.ml
@@ -897,9 +897,12 @@ module Dom = struct
if Ival.equal v old then old'
else Some v) t v dom
+ let add_with_bot t v dom =
+ if is_top_ival v then dom else Tmap.add t v dom
+
let add t v dom =
if Ival.is_bottom v then raise Lang.Contradiction;
- if is_top_ival v then dom else Tmap.add t v dom
+ add_with_bot t v dom
let remove t dom = Tmap.remove t dom
@@ -1114,7 +1117,7 @@ let is_cint_simplifier =
if quant = Forall
then reduce_on_pos tvar var_domain t
else reduce_on_neg tvar var_domain t;
- domain <- Dom.add tvar !var_domain domain;
+ domain <- Dom.add_with_bot tvar !var_domain domain;
qv, Some (tvar, var_domain)
| _ -> qv, None) ctx
in
diff --git a/src/plugins/wp/tests/wp_bts/issue_825.i b/src/plugins/wp/tests/wp_bts/issue_825.i
new file mode 100644
index 0000000000000000000000000000000000000000..3810f22f258670830a5d6e468af2993ecdbbf394
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/issue_825.i
@@ -0,0 +1,21 @@
+/*@
+ ensures \false ;
+ assigns \nothing;
+*/
+void job(void)
+{
+ int i=0, K=0;
+ /*@
+ loop invariant \forall integer j; 0 < j < 0 ==> \false ;
+ loop assigns i ;
+ */
+ while (i < 10) {
+ K ++;
+ 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
new file mode 100644
index 0000000000000000000000000000000000000000..65c234448ba7d4d4dff459d117eb43ab42bf7ee7
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle/issue_825.res.oracle
@@ -0,0 +1,56 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_825.i (no preprocessing)
+[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
+------------------------------------------------------------
+
+Goal Post-condition (file tests/wp_bts/issue_825.i, line 2) in 'job':
+Assume { Type: is_sint32(i). (* Else *) Have: 10 <= i. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Preservation of Invariant (file tests/wp_bts/issue_825.i, line 9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Establishment of Invariant (file tests/wp_bts/issue_825.i, line 9):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_bts/issue_825.i, line 10) (1/2):
+Prove: true.
+
+------------------------------------------------------------
+
+Goal Loop assigns (file tests/wp_bts/issue_825.i, line 10) (2/2):
+Effect at line 13
+Assume { Type: is_sint32(i). (* Then *) Have: i <= 9. }
+Prove: false.
+
+------------------------------------------------------------
+
+Goal Assigns nothing in 'job':
+Effect at line 12
+Prove: true.
+
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/118942e3748b5cc75d45b55bc13dbaa6.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/118942e3748b5cc75d45b55bc13dbaa6.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/118942e3748b5cc75d45b55bc13dbaa6.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.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.0.session/cache/f64541ce5299d6cdd4b7e923e5d59a5f.json b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/f64541ce5299d6cdd4b7e923e5d59a5f.json
new file mode 100644
index 0000000000000000000000000000000000000000..b8e36e2803fcc35bf7625695f4ebcfc62989c064
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/f64541ce5299d6cdd4b7e923e5d59a5f.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
new file mode 100644
index 0000000000000000000000000000000000000000..35895046c313f3c5b9afccb4df714ce09f77ecc0
--- /dev/null
+++ b/src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.res.oracle
@@ -0,0 +1,22 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_bts/issue_825.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] Loading driver 'share/wp.driver'
+[wp] Warning: Missing RTE guards
+[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 / 8
+ Qed: 4
+ Alt-Ergo: 0 (unsuccess: 4)
+------------------------------------------------------------
+ Functions WP Alt-Ergo Total Success
+ job 4 - 6 66.7%
+ issue - - 2 0.0%
+------------------------------------------------------------