[wp] fix quantified int simplifier

keep bottom domain in the right place

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

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

@@ -8,7 +8,8 @@
 ------------------------------------------------------------
 
 Goal Post-condition (file tests/wp_bts/issue_825.i, line 2) in 'job':
-Prove: true.
+Assume { Type: is_sint32(i). (* Else *) Have: 10 <= i. }
+Prove: false.
 
 ------------------------------------------------------------
 
@@ -29,7 +30,8 @@ Prove: true.
 
 Goal Loop assigns (file tests/wp_bts/issue_825.i, line 10) (2/2):
 Effect at line 13
-Prove: true.
+Assume { Type: is_sint32(i). (* Then *) Have: i <= 9. }
+Prove: false.
 
 ------------------------------------------------------------
 

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_825.0.session/cache/118942e3748b5cc75d45b55bc13dbaa6.json

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

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

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

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

@@ -4,15 +4,16 @@
 [wp] Loading driver 'share/wp.driver'
 [wp] Warning: Missing RTE guards
 [wp] 6 goals scheduled
-[wp] [Qed] Goal typed_job_ensures : Valid
+[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] [Qed] Goal typed_job_loop_assigns_part2 : Valid
+[wp] [Alt-Ergo] Goal typed_job_loop_assigns_part2 : Unsuccess
 [wp] [Qed] Goal typed_job_assigns : Valid
-[wp] Proved goals:    6 / 6
-  Qed:             6
+[wp] Proved goals:    4 / 6
+  Qed:             4 
+  Alt-Ergo:        0  (unsuccess: 2)
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  job                       6        -        6       100%
+  job                       4        -        6      66.7%
 ------------------------------------------------------------