diff --git a/Changelog b/Changelog
index 14ce523618ef402165097b2c4c7b4fbe3d59ceb0..3c562140b14dda2daa1a499b648cde01a44a744b 100644
--- a/Changelog
+++ b/Changelog
@@ -18,6 +18,9 @@
 Open Source Release <next-release>
 ###############################################################################
 
+*   RTE       [2024-10-04] Fixed missing assertion on modulo signed overflow.
+*   Eva       [2024-10-04] Fixed missing signed overflow alarm on modulo.
+-   Eva       [2024-10-04] Fewer false alarms of signed overflow on divisions.
 o!  Kernel    [2024-09-30] ACSL extensions are now associated to a plug-in,
               allowing the registration of several extensions with the same name
               from different plug-ins
diff --git a/src/plugins/eva/ast/eva_ast_builder.ml b/src/plugins/eva/ast/eva_ast_builder.ml
index 1faa1e6f1dc9af1562e723b2e979439ee994ff4b..6b8f061985b4b973e1746bfe692491f51f4501be 100644
--- a/src/plugins/eva/ast/eva_ast_builder.ml
+++ b/src/plugins/eva/ast/eva_ast_builder.ml
@@ -202,6 +202,7 @@ struct
     | _ -> invalid_arg "unsupported construction"
 
   let add = binop PlusA
+  let div = binop Div
   let eq = binop Eq
   let ne = binop Ne
 
diff --git a/src/plugins/eva/ast/eva_ast_builder.mli b/src/plugins/eva/ast/eva_ast_builder.mli
index 7a7bdcdcdc614698b005d31bd49cca0ec52bc539..448da7c1e6af41fccbf4959492dc1a7605b235ea 100644
--- a/src/plugins/eva/ast/eva_ast_builder.mli
+++ b/src/plugins/eva/ast/eva_ast_builder.mli
@@ -73,6 +73,7 @@ sig
 
   val cast: typ -> exp -> exp (* (typ)x *)
   val add: exp -> exp -> exp (* x + y *)
+  val div: exp -> exp -> exp (* x / y *)
   val eq: exp -> exp -> exp (* x == y *)
   val ne: exp -> exp -> exp (* x != y *)
 
diff --git a/src/plugins/eva/engine/evaluation.ml b/src/plugins/eva/engine/evaluation.ml
index cbb95ced117ad297b74bf51bc738689398b55540..8421d8d9269c1a1adc54b3b732127460bebd8c1c 100644
--- a/src/plugins/eva/engine/evaluation.ml
+++ b/src/plugins/eva/engine/evaluation.ml
@@ -342,6 +342,23 @@ module Make
                     Forward Operations, Alarms and Reductions
      ------------------------------------------------------------------------ *)
 
+  (* Applies function [f] on the optional value in a truth. *)
+  let apply_on_truth f = function
+    | `Unknown v -> `Unknown (f v)
+    | `TrueReduced v -> `TrueReduced (f v)
+    | `True | `False | `Unreachable as x -> x
+
+  (* Assumes that the abstract value [value] represents only values
+     different from integer [i]. *)
+  let assume_non_equal context typ value i =
+    let forward_binop = Value.forward_binop context typ in
+    (* Bottom should never happen on addition or subtraction. *)
+    let add v1 v2 = Bottom.non_bottom (forward_binop PlusA v1 v2) in
+    let sub v1 v2 = Bottom.non_bottom (forward_binop MinusA v1 v2) in
+    let v_i = Value.inject_int typ i in
+    let truth = Value.assume_non_zero (sub value v_i) in
+    apply_on_truth (fun value -> add value v_i) truth
+
   (* Handles the result of an [assume] function from value abstractions (see
      abstract_values.mli for more details), applied to the initial [value].
      If the value could have been reduced, [reduce] is applied on the new value.
@@ -369,22 +386,37 @@ module Make
     let reduce = reduce_argument (expr, value) in
     process_truth ~reduce ~alarm value truth
 
-  (* Processes the results of assume_comparable, that affects both arguments of
-     the comparison. *)
-  let reduce_by_double_truth ~alarm (e1, v1) (e2, v2) truth =
+  (* Interprets a [truth] about a pair of values (v1, v2), and reduce both
+     values accordingly. Used on the result of [Value.assume_comparable], which
+     affects both arguments of the comparison. *)
+  let reduce_both_by_truth ~alarm (e1, v1) (e2, v2) truth =
     let reduce (new_value1, new_value2) =
       Option.iter (fun e1 -> reduce_argument (e1, v1) new_value1) e1;
       reduce_argument (e2, v2) new_value2;
     in
     process_truth ~reduce ~alarm (v1, v2) truth
 
+  (* Creates a disjunctive truth about the pair of values (v1, v2). *)
+  let disjunctive_truth (v1, truth1) (v2, truth2) =
+    match truth1, truth2 with
+    | (`True | `TrueReduced _), _
+    | _, (`True | `TrueReduced _) -> `True
+    | `Unreachable, _ | _, `Unreachable -> `Unreachable
+    | `False, `False -> `False
+    | `False, `Unknown v2 -> `Unknown (v1, v2)
+    | `Unknown v1, `False -> `Unknown (v1, v2)
+    | `Unknown _, `Unknown _ ->
+      (* [v1] (resp. [v2]) cannot be reduced as [truth2] (resp. [truth1])
+         might be true for some values. *)
+      `Unknown (v1, v2)
+
   let is_true = function
     | `True | `TrueReduced _ -> true
     | _ -> false
 
+  (* Overflow of div is processed separately in [assume_valid_div]. *)
   let may_overflow = function
-    | Shiftlt | Mult | MinusPP | MinusPI | PlusPI
-    | PlusA | MinusA | Div -> true
+    | Shiftlt | Mult | MinusPP | MinusPI | PlusPI | PlusA | MinusA -> true
     | _ -> false
 
   let truncate_bound overflow_kind bound bound_kind expr value =
@@ -541,15 +573,37 @@ module Make
     let truth = Value.assume_bounded Alarms.Upper_bound size_int value in
     reduce_by_truth ~alarm (index_expr, value) truth
 
-  let assume_valid_binop typ (e1, v1 as arg1) op (e2, v2 as arg2) =
+  (* Checks the arguments of a division and creates a division by zero alarm
+     if [v2] can be equal to 0, and an overflow alarm if [typ] is a signed
+     integer type, [v1] can be equal to min_int AND [v2] can be equal to -1.
+     Also reduces the values of [v1] or [v2] accordingly when possible. *)
+  let assume_valid_div context typ (e1, v1) (e2, v2) =
     let open Evaluated.Operators in
+    let truth = Value.assume_non_zero v2 in
+    let alarm () = Alarms.Division_by_zero (Eva_ast.to_cil_exp e2) in
+    let* v2 = reduce_by_truth ~alarm (e2, v2) truth in
+    match Eval_typ.integer_range ~ptr:false typ with
+    | Some range when range.i_signed ->
+      let min_int = Eval_typ.range_lower_bound range in
+      let max_int = Eval_typ.range_upper_bound range in
+      let alarm () =
+        let expr = Eva_ast.Build.div e1 e2 in
+        let cil_expr = Eva_ast.to_cil_exp expr in
+        Alarms.(Overflow (Signed, cil_expr, max_int, Upper_bound))
+      in
+      let truth1 = assume_non_equal context typ v1 min_int in
+      let truth2 = assume_non_equal context typ v2 Integer.minus_one in
+      let truth = disjunctive_truth (v1, truth1) (v2, truth2) in
+      reduce_both_by_truth ~alarm (Some e1, v1) (e2, v2) truth
+    | _ -> return (v1, v2)
+
+  let assume_valid_binop context typ (e1, v1 as arg1) op (e2, v2 as arg2) =
     if Cil.isIntegralType typ then
       match op with
       | Div | Mod ->
-        let truth = Value.assume_non_zero v2 in
-        let alarm () = Alarms.Division_by_zero (Eva_ast.to_cil_exp e2) in
-        let+ v2 = reduce_by_truth ~alarm arg2 truth in
-        v1, v2
+        (* The behavior of a%b is undefined if the behavior of a/b is undefined,
+           according to section 6.5.5 §5 and §6 of the C standard. *)
+        assume_valid_div context typ arg1 arg2
       | Shiftrt ->
         let warn_negative = Kernel.RightShiftNegative.get () in
         reduce_shift ~warn_negative typ arg1 arg2
@@ -563,7 +617,7 @@ module Make
           Alarms.Differing_blocks (Eva_ast.to_cil_exp e1, Eva_ast.to_cil_exp e2)
         in
         let arg1 = Some e1, v1 in
-        reduce_by_double_truth ~alarm arg1 arg2 truth
+        reduce_both_by_truth ~alarm arg1 arg2 truth
       | _ -> return (v1, v2)
     else return (v1, v2)
 
@@ -587,7 +641,7 @@ module Make
       if warn_pointer_comparison typ then
         if propagate_all
         then `Value (v1, v2), snd (interpret_truth ~alarm (v1, v2) truth)
-        else reduce_by_double_truth ~alarm (e1, v1) (e2, v2) truth
+        else reduce_both_by_truth ~alarm (e1, v1) (e2, v2) truth
       else `Value (v1, v2), Alarmset.none
     in
     let result = let* v1, v2 = args in compute v1 v2 in
@@ -616,7 +670,7 @@ module Make
       let e1 = if Eva_ast.is_zero_ptr e1 then None else Some e1 in
       forward_comparison ~compute typ_e1 kind (e1, v1) arg2
     | None ->
-      let& v1, v2 = assume_valid_binop typ arg1 op arg2 in
+      let& v1, v2 = assume_valid_binop context typ arg1 op arg2 in
       Value.forward_binop context typ_e1 op v1 v2
 
   let forward_unop context unop (e, v as arg) =
diff --git a/src/plugins/eva/utils/eval_typ.ml b/src/plugins/eva/utils/eval_typ.ml
index 69649a738b3b319bb93158709b0077273d87d59b..9781c483f5f8047803f54a7e3eb6e2d28435f0ad 100644
--- a/src/plugins/eva/utils/eval_typ.ml
+++ b/src/plugins/eva/utils/eval_typ.ml
@@ -191,6 +191,13 @@ let classify_as_scalar typ =
   | TFloat (fk, _) -> Some (TSFloat fk)
   | _ -> None
 
+let integer_range ~ptr typ =
+  match Cil.unrollType typ with
+  | TInt (ik, attrs) | TEnum ({ekind=ik}, attrs) ->
+    Some (ik_attrs_range ik attrs)
+  | TPtr _ when ptr -> Some (pointer_range ())
+  | _ -> None
+
 let need_cast t1 t2 =
   match classify_as_scalar t1, classify_as_scalar t2 with
   | None, None -> Cil.need_cast t1 t2
diff --git a/src/plugins/eva/utils/eval_typ.mli b/src/plugins/eva/utils/eval_typ.mli
index f00f1829f7e46a12296646253c0268611ce9f638..627573586023bea6de6e685c7fccdd98af6b5df5 100644
--- a/src/plugins/eva/utils/eval_typ.mli
+++ b/src/plugins/eva/utils/eval_typ.mli
@@ -86,3 +86,7 @@ type scalar_typ =
 
 (* Classifies a cil type as a scalar type; returns None for non-scalar types. *)
 val classify_as_scalar: typ -> scalar_typ option
+
+(* Returns the range of a cil integer type; returns None for non-integer types.
+   Pointers are considered as integer types if [ptr] is true. *)
+val integer_range: ptr:bool -> typ -> integer_range option
diff --git a/src/plugins/rte/rte.ml b/src/plugins/rte/rte.ml
index 8104e697961bc09ee043e9ae140403d899514772..9bfa0a718baef775b3ca14e8e30be67d3ef71eaf 100644
--- a/src/plugins/rte/rte.ml
+++ b/src/plugins/rte/rte.ml
@@ -234,10 +234,7 @@ let signed_div_assertion ~remove_trivial ~on_alarm (exp, lexp, rexp) =
      the minimum (negative) value for the signed integer type,
      and divisor is equal to -1. Under the hypothesis (cf Value) that
      integers are represented in two's complement.
-     Nothing done for modulo (the result of TYPE_MIN % -1 is 0, which does not
-     overflow).
-     Still it may be dangerous on a number of compilers / architectures
-     (modulo may be performed in parallel with division) *)
+  *)
   let t = Cil.unrollType (Cil.typeOf rexp) in
   let size = Cil.bitsSizeOf t in
   (* check dividend_expr / divisor_expr : if constants ... *)
diff --git a/src/plugins/rte/visit.ml b/src/plugins/rte/visit.ml
index 80db7522f948e78cb08114da69baa96f68494b1a..a442aba7198ef0bcb239d9cfd765c1f278b0551e 100644
--- a/src/plugins/rte/visit.ml
+++ b/src/plugins/rte/visit.ml
@@ -215,15 +215,15 @@ class annot_visitor kf flags on_alarm = object (self)
     | _ ->
       let generate () =
         match exp.enode with
-        | BinOp((Div | Mod) as op, lexp, rexp, ty) ->
+        | BinOp((Div | Mod), lexp, rexp, ty) ->
           (match Cil.unrollType ty with
            | TInt(kind,_) ->
              (* add assertion "divisor not zero" *)
              if self#do_div_mod () then
                self#generate_assertion Rte.divmod_assertion rexp;
-             if self#do_signed_overflow () && op = Div && Cil.isSigned kind then
-               (* treat the special case of signed division overflow
-                  (no signed modulo overflow) *)
+             if self#do_signed_overflow () && Cil.isSigned kind then
+               (* treat the special case of signed division/modulo overflow *)
+               let exp = { exp with enode = BinOp (Div, lexp, rexp, ty) } in
                self#generate_assertion Rte.signed_div_assertion (exp, lexp, rexp)
            | TFloat(fkind,_) when self#do_finite_float () ->
              self#generate_assertion Rte.finite_float_assertion (fkind,exp);
diff --git a/src/plugins/wp/tests/wp_gallery/euclid.c b/src/plugins/wp/tests/wp_gallery/euclid.c
index 130896edb869eda985da946cc155712452c388bb..a2edb06407a9901a8107230618b343d4e38bddfd 100644
--- a/src/plugins/wp/tests/wp_gallery/euclid.c
+++ b/src/plugins/wp/tests/wp_gallery/euclid.c
@@ -29,6 +29,7 @@ int euclid_gcd(int a, int b)
   int r;
   /*@
     loop assigns a, b, r;
+    loop invariant \abs(a) <= INT_MAX && \abs(b) <= INT_MAX ;
     loop invariant gcd(a,b) == \at( gcd(a,b), Pre );
     loop variant \abs(b);
   */
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
index 5de7d3a8e0a74e093ca04765c8370a920f6ec4ca..42c40f083cedc77c9bc1d92e6cb7212035a8aed2 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/euclid.res.oracle
@@ -4,7 +4,7 @@
 [rte:annot] annotating function euclid_gcd
 [wp] [Valid] Goal euclid_gcd_exits (Cfg) (Unreachable)
 [wp] [Valid] Goal euclid_gcd_terminates (Cfg) (Trivial)
-[wp] 16 goals scheduled
+[wp] 19 goals scheduled
 [wp] [Passed] (Unsuccess) typed_euclid_euclid_gcd_wp_smoke_default_requires (Alt-Ergo) (Cached)
 [wp] [Passed] (Unsuccess) typed_euclid_euclid_gcd_wp_smoke_dead_loop_s1 (Alt-Ergo) (Cached)
 [wp] [Passed] (Unsuccess) typed_euclid_euclid_gcd_wp_smoke_dead_code_s6 (Alt-Ergo) (Cached)
@@ -13,21 +13,24 @@
 [wp] [Valid] typed_euclid_euclid_gcd_ensures (Alt-Ergo) (Cached)
 [wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_preserved (Alt-Ergo) (Cached)
 [wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_established (Qed)
+[wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_2_preserved (Alt-Ergo) (Cached)
+[wp] [Valid] typed_euclid_euclid_gcd_loop_invariant_2_established (Qed)
 [wp] [Valid] typed_euclid_euclid_gcd_assert_rte_division_by_zero (Qed)
 [wp] [Valid] typed_euclid_euclid_gcd_assert_rte_signed_overflow (Alt-Ergo) (Cached)
+[wp] [Valid] typed_euclid_euclid_gcd_assert_rte_signed_overflow_2 (Alt-Ergo) (Cached)
 [wp] [Valid] typed_euclid_euclid_gcd_loop_assigns (Qed)
 [wp] [Valid] typed_euclid_euclid_gcd_assigns_part1 (Qed)
 [wp] [Valid] typed_euclid_euclid_gcd_assigns_part2 (Qed)
 [wp] [Valid] typed_euclid_euclid_gcd_assigns_part3 (Qed)
 [wp] [Valid] typed_euclid_euclid_gcd_loop_variant_decrease (Alt-Ergo) (Cached)
 [wp] [Valid] typed_euclid_euclid_gcd_loop_variant_positive (Qed)
-[wp] Proved goals:   18 / 18
+[wp] Proved goals:   21 / 21
   Terminating:     1
   Unreachable:     1
-  Qed:             7
-  Alt-Ergo:        9
+  Qed:             8
+  Alt-Ergo:       11
   Smoke Tests:     5 / 5
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  euclid_gcd                7        9       16       100%
+  euclid_gcd                8       11       19       100%
 ------------------------------------------------------------
diff --git a/tests/rte/oracle/divmod.res.oracle b/tests/rte/oracle/divmod.res.oracle
index 547de8eb072a7a22a19f9248bf80dfda2672bc44..55bdb14cf875879072171af8f65d8a6e66637543 100644
--- a/tests/rte/oracle/divmod.res.oracle
+++ b/tests/rte/oracle/divmod.res.oracle
@@ -4,6 +4,10 @@
   guaranteed RTE:
   assert
   signed_overflow: (int)((int)(-2147483647) - 1) / (int)(-1) ≤ 2147483647;
+[rte] divmod.c:14: Warning: 
+  guaranteed RTE:
+  assert
+  signed_overflow: (int)((int)(-2147483647) - 1) / (int)(-1) ≤ 2147483647;
 [rte] divmod.c:16: Warning: guaranteed RTE: assert division_by_zero: 0 ≢ 0;
 [rte] divmod.c:17: Warning: 
   guaranteed RTE:
@@ -36,6 +40,10 @@ int main(void)
         (int)((int)(-2147483647) - 1) / (int)(-1) ≤ 2147483647;
   */
   z = (-2147483647 - 1) / -1;
+  /*@ assert
+      rte: signed_overflow:
+        (int)((int)(-2147483647) - 1) / (int)(-1) ≤ 2147483647;
+  */
   z = (-2147483647 - 1) % -1;
   /*@ assert rte: division_by_zero: 0 ≢ 0; */
   uz = (unsigned int)(1 / 0);
diff --git a/tests/rte/oracle/divmod_typedef.res.oracle b/tests/rte/oracle/divmod_typedef.res.oracle
index 9bf2d9db039ff682b472bd157edb0c259d00c8d5..b42cf255103b5384d6e002c1cf957cb6e95bdb5a 100644
--- a/tests/rte/oracle/divmod_typedef.res.oracle
+++ b/tests/rte/oracle/divmod_typedef.res.oracle
@@ -4,6 +4,10 @@
   guaranteed RTE:
   assert
   signed_overflow: (int)((int)(-2147483647) - 1) / (int)(-1) ≤ 2147483647;
+[rte] divmod_typedef.c:16: Warning: 
+  guaranteed RTE:
+  assert
+  signed_overflow: (int)((int)(-2147483647) - 1) / (int)(-1) ≤ 2147483647;
 [rte] divmod_typedef.c:18: Warning: 
   guaranteed RTE: assert division_by_zero: 0 ≢ 0;
 [rte] divmod_typedef.c:19: Warning: 
@@ -39,6 +43,10 @@ int main(void)
         (int)((int)(-2147483647) - 1) / (int)(-1) ≤ 2147483647;
   */
   z = (-2147483647 - 1) / -1;
+  /*@ assert
+      rte: signed_overflow:
+        (int)((int)(-2147483647) - 1) / (int)(-1) ≤ 2147483647;
+  */
   z = (-2147483647 - 1) % -1;
   /*@ assert rte: division_by_zero: 0 ≢ 0; */
   uz = (tuint)(1 / 0);
diff --git a/tests/value/div.i b/tests/value/div.i
index 55857e727f928c53392e6edb8dae1ec056a31a7d..74d9eb4233714a9c7ce0918cd5bab5a2f388cbb9 100644
--- a/tests/value/div.i
+++ b/tests/value/div.i
@@ -1,14 +1,14 @@
 /* run.config*
-   STDOPT: #"-eva-remove-redundant-alarms"
-   PLUGIN: @PTEST_PLUGIN@ rtegen
-   OPT: -machdep x86_32 @RTE_TEST@ -then -eva @EVA_CONFIG@
+   STDOPT: #""
 */
+
+volatile int nondet;
 int X,Y,Z1,Z2,T,U1,U2,V,W1,W2;
 int a,b,d1,d2,d0,e;
 int t[5]={1,2,3};
 int *p;
 
-void main (void) {
+void test (void) {
   int i;
   volatile int c=0;
   while (c+1)
@@ -36,3 +36,53 @@ void main (void) {
   d0 = 100 / (int)(&X);
   e = - (int) &X;
 }
+
+/* Tests the emission of overflow alarms on a division x/y only if [x] may be
+   equal to MIN_INT and [y] may be equal to -1. Also tests the reduction of the
+   possible values of [x] or [y] when possible. Similar test in file modulo.i. */
+void test_overflow_alarms (void) {
+  int min_int = -2147483648;
+  int min_one = -1;
+  int a = nondet ? min_int : 10;
+  int b = nondet ? -1 : 2;
+  int x = nondet;
+  int y = nondet;
+  int r = 0;
+  if (nondet) {
+    r = a / b; // Overflow alarm.
+    // No reduction as [a] and [b] cannot be reduced simultaneously.
+    Frama_C_show_each(a, b);
+  }
+  if (nondet) {
+    r = a / min_one; // Overflow alarm.
+    r = a / min_one; // No alarm if [a] has been reduced.
+    Frama_C_show_each_ten(a); // Check the reduction of [a].
+  }
+  if (nondet) {
+    r = min_int / b; // Overflow alarm.
+    r = min_int / b; // No alarm if [b] has been reduced.
+    Frama_C_show_each_two(b); // Check the reduction of [b]
+  }
+  if (nondet) {
+    r = x / min_one; // Overflow alarm.
+    r = x / min_one; // No alarm if [x] has been reduced.
+    Frama_C_show_each(x); // All integers except MIN_INT.
+  }
+  if (nondet) {
+    r = min_int / x; // Overflow alarm and division by zero alarm.
+    // All integers except -1 and 0, but not representable as an interval.
+    Frama_C_show_each(x);
+  }
+  if (nondet) {
+    r = min_int / min_one; // Invalid alarm.
+    Frama_C_show_each_BOTTOM(min_int, min_one);
+  }
+  // Overflow alarm and division by zero alarm,
+  // no possible reduction: [x] and [y] must be top_int as the end.
+  r = x / y;
+}
+
+void main (void) {
+  test();
+  test_overflow_alarms();
+}
diff --git a/tests/value/modulo.i b/tests/value/modulo.i
index e802427c601e40b1b4eeb7ef6856a121ecb1a95c..98f5deb88d06b4ce647dcb7df97bc616352b6dd4 100644
--- a/tests/value/modulo.i
+++ b/tests/value/modulo.i
@@ -147,7 +147,9 @@ void pos_rem(void) {
   int l = (int)*(signed char*)&n; // Best rem is ([0..72] \cup {255})%255, we approximate by [-128..127]
 }
 
-/* No overflow alarms should be emitted on mod operations, even on addresses. */
+/* On modulo, overflow alarms should only be emitted on INT_MIN % -1, which
+   is not possible on addresses. However, garbled mixes on arithmetic operations
+   involving addresses currently lose all precision and lead to false alarms. */
 void address_modulo(void) {
   int* ptr = v ? &A : &B;
   unsigned int uaddr = (unsigned int) ptr;
@@ -159,6 +161,51 @@ void address_modulo(void) {
   r = uaddr % i;
 }
 
+/* Tests the emission of overflow alarms on operation x%y only if [x] may be
+   equal to MIN_INT and [y] may be equal to -1. Also tests the reduction of the
+   possible values of [x] or [y] when possible. Similar test in file div.i. */
+void test_overflow_alarms (void) {
+  int min_int = -2147483648;
+  int min_one = -1;
+  int a = v ? min_int : 10;
+  int b = v ? -1 : 2;
+  int x = v;
+  int y = v;
+  int r = 0;
+  if (v) {
+    r = a % b; // Overflow alarm.
+    // No reduction as [a] and [b] cannot be reduced simultaneously.
+    Frama_C_show_each(a, b);
+  }
+  if (v) {
+    r = a % min_one; // Overflow alarm.
+    r = a % min_one; // No alarm if [a] has been reduced.
+    Frama_C_show_each_ten(a); // Check the reduction of [a].
+  }
+  if (v) {
+    r = min_int % b; // Overflow alarm.
+    r = min_int % b; // No alarm if [b] has been reduced.
+    Frama_C_show_each_two(b); // Check the reduction of [b]
+  }
+  if (v) {
+    r = x % min_one; // Overflow alarm.
+    r = x % min_one; // No alarm if [x] has been reduced.
+    Frama_C_show_each(x); // All integers except MIN_INT.
+  }
+  if (v) {
+    r = min_int % x; // Overflow alarm and division by zero alarm.
+    // All integers except -1 and 0, but not representable as an interval.
+    Frama_C_show_each(x);
+  }
+  if (v) {
+    r = min_int % min_one; // Invalid alarm.
+    Frama_C_show_each_BOTTOM(min_int, min_one);
+  }
+  // Overflow alarm and division by zero alarm,
+  // no possible reduction: [x] and [y] must be top_int as the end.
+  r = x / y;
+}
+
 void main() {
   if (v) { pgcd1(a, b); }
   if (v) { pgcd2(a, b); }
@@ -170,4 +217,5 @@ void main() {
   extract_bits_modulo();
   pos_rem();
   address_modulo();
+  test_overflow_alarms();
 }
diff --git a/tests/value/oracle/addition.res.oracle b/tests/value/oracle/addition.res.oracle
index 394936b8b9df05a61b4935cb721c0e66380efa36..38e7399ccb347f9cd480cae8b28a109c9c7234a8 100644
--- a/tests/value/oracle/addition.res.oracle
+++ b/tests/value/oracle/addition.res.oracle
@@ -102,10 +102,6 @@
   assert \pointer_comparable((void *)(&p1 + 1), (void *)(&p2));
 [eva:alarm] addition.i:50: Warning: 
   pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
-[eva:alarm] addition.i:50: Warning: 
-  signed overflow. assert -2147483648 ≤ (int)(&p1) / 2;
-[eva:alarm] addition.i:50: Warning: 
-  signed overflow. assert (int)(&p1) / 2 ≤ 2147483647;
 [eva:garbled-mix:write] addition.i:50: Warning: 
   Assigning imprecise value to p9 because of arithmetic operation on addresses.
 [eva:alarm] addition.i:52: Warning: 
@@ -136,8 +132,11 @@
   out of bounds read. assert \valid_read(*((int **)45));
 [eva] addition.i:87: Frama_C_show_each_1: [-10..15]
 [eva] addition.i:88: assertion got status valid.
+[eva:alarm] addition.i:98: Warning: 
+  signed overflow. assert p17 / (int)(-1) ≤ 2147483647;
 [eva] Recording results for main
 [eva] Done for function main
+[eva] addition.i:98: assertion 'Eva,signed_overflow' got final status invalid.
 [scope:rm_asserts] removing 9 assertion(s)
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function main:
@@ -165,7 +164,7 @@
      {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
   p15 ∈ {-1}
   p16 ∈ {2949122}
-  p17 ∈ {-2147483648; 0}
+  p17 ∈ {-2147483648}
   u1 ∈ {8}
   q1 ∈ {{ &p1 }}
   quo1 ∈ {3}
@@ -342,10 +341,6 @@
   assert \pointer_comparable((void *)(&p1 + 1), (void *)(&p2));
 [eva:alarm] addition.i:50: Warning: 
   pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
-[eva:alarm] addition.i:50: Warning: 
-  signed overflow. assert -2147483648 ≤ (int)(&p1) / 2;
-[eva:alarm] addition.i:50: Warning: 
-  signed overflow. assert (int)(&p1) / 2 ≤ 2147483647;
 [eva:alarm] addition.i:52: Warning: 
   pointer downcast. assert (unsigned int)(&p1) ≤ 2147483647;
 [eva:alarm] addition.i:56: Warning: 
@@ -363,6 +358,8 @@
 [eva:alarm] addition.i:66: Warning: 
   out of bounds read. assert \valid_read(*((int **)45));
 [eva] addition.i:87: Frama_C_show_each_1: [-10..15]
+[eva:alarm] addition.i:98: Warning: 
+  signed overflow. assert p17 / (int)(-1) ≤ 2147483647;
 [eva] Recording results for main
 [eva] Done for function main
 [scope:rm_asserts] removing 9 assertion(s)
@@ -393,7 +390,7 @@
      {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
   p15 ∈ {-1}
   p16 ∈ {2; 2949122; 3014658}
-  p17 ∈ {-2147483648; 0}
+  p17 ∈ {-2147483648}
   u1 ∈ {8}
   q1 ∈ {{ &p1 }}
   quo1 ∈ {3}
diff --git a/tests/value/oracle/div.1.res.oracle b/tests/value/oracle/div.1.res.oracle
deleted file mode 100644
index d2a683468cbd53aa220ad3eab5454b1ab977ed7c..0000000000000000000000000000000000000000
--- a/tests/value/oracle/div.1.res.oracle
+++ /dev/null
@@ -1,138 +0,0 @@
-[kernel] Parsing div.i (no preprocessing)
-[rte:annot] annotating function main
-[eva] Analyzing a complete application starting at main
-[eva] Computing initial state
-[eva] Initial state computed
-[eva:initial-state] Values of globals at initialization
-  X ∈ {0}
-  Y ∈ {0}
-  Z1 ∈ {0}
-  Z2 ∈ {0}
-  T ∈ {0}
-  U1 ∈ {0}
-  U2 ∈ {0}
-  V ∈ {0}
-  W1 ∈ {0}
-  W2 ∈ {0}
-  a ∈ {0}
-  b ∈ {0}
-  d1 ∈ {0}
-  d2 ∈ {0}
-  d0 ∈ {0}
-  e ∈ {0}
-  t[0] ∈ {1}
-   [1] ∈ {2}
-   [2] ∈ {3}
-   [3..4] ∈ {0}
-  p ∈ {0}
-[eva:alarm] div.i:14: Warning: 
-  assertion 'rte,signed_overflow' got status unknown.
-[eva:alarm] div.i:14: Warning: signed overflow. assert c + 1 ≤ 2147483647;
-[eva] div.i:16: assertion 'rte,signed_overflow' got status valid.
-[eva:alarm] div.i:17: Warning: 
-  assertion 'rte,signed_overflow' got status unknown.
-[eva:alarm] div.i:17: Warning: signed overflow. assert c + 2 ≤ 2147483647;
-[eva] div.i:17: assertion 'rte,signed_overflow' got status valid.
-[eva] div.i:14: starting to merge loop iterations
-[eva:alarm] div.i:17: Warning: 
-  assertion 'rte,signed_overflow' got status unknown.
-[eva:alarm] div.i:17: Warning: signed overflow. assert -2147483648 ≤ X - 1;
-[eva:alarm] div.i:16: Warning: 
-  assertion 'rte,signed_overflow' got status unknown.
-[eva:alarm] div.i:16: Warning: signed overflow. assert X + 1 ≤ 2147483647;
-[eva] div.i:22: assertion 'rte,signed_overflow' got status valid.
-[eva] div.i:25: assertion 'rte,signed_overflow' got status valid.
-[eva] div.i:28: assertion 'rte,signed_overflow' got status valid.
-[eva:alarm] div.i:32: Warning: 
-  assertion 'rte,division_by_zero' got status unknown.
-[eva:alarm] div.i:32: Warning: division by zero. assert Z2 ≢ 0;
-[eva:alarm] div.i:33: Warning: 
-  assertion 'rte,pointer_downcast' got status unknown.
-[eva:alarm] div.i:33: Warning: 
-  assertion 'rte,division_by_zero' got status unknown.
-[eva:alarm] div.i:33: Warning: 
-  assertion 'rte,signed_overflow' got status unknown.
-[eva:alarm] div.i:33: Warning: division by zero. assert Z2 ≢ 0;
-[eva:alarm] div.i:33: Warning: 
-  pointer downcast. assert (unsigned int)(&Z2) ≤ 2147483647;
-[eva:alarm] div.i:33: Warning: 
-  signed overflow. assert -2147483648 ≤ (int)(&Z2) / Z2;
-[eva:alarm] div.i:33: Warning: 
-  signed overflow. assert (int)(&Z2) / Z2 ≤ 2147483647;
-[eva:garbled-mix:write] div.i:33: 
-  Assigning imprecise value to b because of arithmetic operation on addresses.
-[eva:alarm] div.i:34: Warning: 
-  assertion 'rte,pointer_downcast' got status unknown.
-[eva:alarm] div.i:34: Warning: 
-  assertion 'rte,division_by_zero' got status unknown.
-[eva:alarm] div.i:34: Warning: 
-  pointer downcast. assert (unsigned int)(&X + 2) ≤ 2147483647;
-[eva:alarm] div.i:34: Warning: division by zero. assert (int)(&X + 2) ≢ 0;
-[eva:alarm] div.i:34: Warning: 
-  signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 2);
-[eva:alarm] div.i:34: Warning: 
-  signed overflow. assert 100 / (int)(&X + 2) ≤ 2147483647;
-[eva:garbled-mix:write] div.i:34: 
-  Assigning imprecise value to d2 because of arithmetic operation on addresses.
-[eva:alarm] div.i:35: Warning: 
-  assertion 'rte,pointer_downcast' got status unknown.
-[eva] div.i:35: assertion 'rte,division_by_zero' got status valid.
-[eva:alarm] div.i:35: Warning: 
-  pointer downcast. assert (unsigned int)(&X + 1) ≤ 2147483647;
-[eva:alarm] div.i:35: Warning: 
-  signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 1);
-[eva:alarm] div.i:35: Warning: 
-  signed overflow. assert 100 / (int)(&X + 1) ≤ 2147483647;
-[eva:garbled-mix:write] div.i:35: 
-  Assigning imprecise value to d1 because of arithmetic operation on addresses.
-[eva:alarm] div.i:36: Warning: 
-  assertion 'rte,pointer_downcast' got status unknown.
-[eva] div.i:36: assertion 'rte,division_by_zero' got status valid.
-[eva:alarm] div.i:36: Warning: 
-  pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
-[eva:alarm] div.i:36: Warning: 
-  signed overflow. assert -2147483648 ≤ 100 / (int)(&X);
-[eva:alarm] div.i:36: Warning: 
-  signed overflow. assert 100 / (int)(&X) ≤ 2147483647;
-[eva:garbled-mix:write] div.i:36: 
-  Assigning imprecise value to d0 because of arithmetic operation on addresses.
-[eva:alarm] div.i:37: Warning: 
-  assertion 'rte,pointer_downcast' got status unknown.
-[eva:alarm] div.i:37: Warning: 
-  assertion 'rte,signed_overflow' got status unknown.
-[eva:alarm] div.i:37: Warning: 
-  pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
-[eva:alarm] div.i:37: Warning: 
-  signed overflow. assert -2147483648 ≤ -((int)(&X));
-[eva:alarm] div.i:37: Warning: 
-  signed overflow. assert -((int)(&X)) ≤ 2147483647;
-[eva:garbled-mix:write] div.i:37: 
-  Assigning imprecise value to e because of arithmetic operation on addresses.
-[eva] Recording results for main
-[eva] Done for function main
-[eva] div.i:22: assertion 'rte,signed_overflow' got final status valid.
-[eva] div.i:25: assertion 'rte,signed_overflow' got final status valid.
-[eva] div.i:28: assertion 'rte,signed_overflow' got final status valid.
-[eva] div.i:35: assertion 'rte,division_by_zero' got final status valid.
-[eva] div.i:36: assertion 'rte,division_by_zero' got final status valid.
-[scope:rm_asserts] removing 2 assertion(s)
-[eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main:
-  X ∈ [--..--]
-  Y ∈ [-126..333],9%27
-  Z1 ∈ [-42..111],3%9
-  Z2 ∈ [-25..66]
-  T ∈ [34..493],7%27
-  U1 ∈ [11..164],2%9
-  U2 ∈ [6..98]
-  V ∈ [-125..334],10%27
-  W1 ∈ [-41..111]
-  W2 ∈ [-25..66]
-  a ∈ [-40000..40000]
-  b ∈ {{ garbled mix of &{Z2} (origin: Arithmetic {div.i:33}) }}
-  d1 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:35}) }}
-  d2 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:34}) }}
-  d0 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:36}) }}
-  e ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:37}) }}
-  p ∈ {{ &t[3] }}
-  c ∈ [--..--]
diff --git a/tests/value/oracle/div.0.res.oracle b/tests/value/oracle/div.res.oracle
similarity index 55%
rename from tests/value/oracle/div.0.res.oracle
rename to tests/value/oracle/div.res.oracle
index 5595ff6926a98d1312568297b44dd166c8d063ce..4b8b6e318ca562e2e3c59d8b535d6efc78f52d03 100644
--- a/tests/value/oracle/div.0.res.oracle
+++ b/tests/value/oracle/div.res.oracle
@@ -3,6 +3,7 @@
 [eva] Computing initial state
 [eva] Initial state computed
 [eva:initial-state] Values of globals at initialization
+  nondet ∈ [--..--]
   X ∈ {0}
   Y ∈ {0}
   Z1 ∈ {0}
@@ -24,6 +25,8 @@
    [2] ∈ {3}
    [3..4] ∈ {0}
   p ∈ {0}
+[eva] computing for function test <- main.
+  Called from div.i:86.
 [eva:alarm] div.i:14: Warning: signed overflow. assert c + 1 ≤ 2147483647;
 [eva:alarm] div.i:17: Warning: signed overflow. assert c + 2 ≤ 2147483647;
 [eva] div.i:14: starting to merge loop iterations
@@ -33,8 +36,6 @@
 [eva:alarm] div.i:33: Warning: division by zero. assert Z2 ≢ 0;
 [eva:alarm] div.i:33: Warning: 
   pointer downcast. assert (unsigned int)(&Z2) ≤ 2147483647;
-[eva:alarm] div.i:33: Warning: 
-  signed overflow. assert -2147483648 ≤ (int)(&Z2) / Z2;
 [eva:alarm] div.i:33: Warning: 
   signed overflow. assert (int)(&Z2) / Z2 ≤ 2147483647;
 [eva:garbled-mix:write] div.i:33: 
@@ -42,26 +43,14 @@
 [eva:alarm] div.i:34: Warning: 
   pointer downcast. assert (unsigned int)(&X + 2) ≤ 2147483647;
 [eva:alarm] div.i:34: Warning: division by zero. assert (int)(&X + 2) ≢ 0;
-[eva:alarm] div.i:34: Warning: 
-  signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 2);
-[eva:alarm] div.i:34: Warning: 
-  signed overflow. assert 100 / (int)(&X + 2) ≤ 2147483647;
 [eva:garbled-mix:write] div.i:34: 
   Assigning imprecise value to d2 because of arithmetic operation on addresses.
 [eva:alarm] div.i:35: Warning: 
   pointer downcast. assert (unsigned int)(&X + 1) ≤ 2147483647;
-[eva:alarm] div.i:35: Warning: 
-  signed overflow. assert -2147483648 ≤ 100 / (int)(&X + 1);
-[eva:alarm] div.i:35: Warning: 
-  signed overflow. assert 100 / (int)(&X + 1) ≤ 2147483647;
 [eva:garbled-mix:write] div.i:35: 
   Assigning imprecise value to d1 because of arithmetic operation on addresses.
 [eva:alarm] div.i:36: Warning: 
   pointer downcast. assert (unsigned int)(&X) ≤ 2147483647;
-[eva:alarm] div.i:36: Warning: 
-  signed overflow. assert -2147483648 ≤ 100 / (int)(&X);
-[eva:alarm] div.i:36: Warning: 
-  signed overflow. assert 100 / (int)(&X) ≤ 2147483647;
 [eva:garbled-mix:write] div.i:36: 
   Assigning imprecise value to d0 because of arithmetic operation on addresses.
 [eva:alarm] div.i:37: Warning: 
@@ -72,11 +61,37 @@
   signed overflow. assert -((int)(&X)) ≤ 2147483647;
 [eva:garbled-mix:write] div.i:37: 
   Assigning imprecise value to e because of arithmetic operation on addresses.
+[eva] Recording results for test
+[eva] Done for function test
+[eva] computing for function test_overflow_alarms <- main.
+  Called from div.i:87.
+[eva:alarm] div.i:52: Warning: signed overflow. assert a_0 / b_0 ≤ 2147483647;
+[eva] div.i:54: Frama_C_show_each: {-2147483648; 10}, {-1; 2}
+[eva:alarm] div.i:57: Warning: 
+  signed overflow. assert a_0 / min_one ≤ 2147483647;
+[eva] div.i:59: Frama_C_show_each_ten: {10}
+[eva:alarm] div.i:62: Warning: 
+  signed overflow. assert min_int / b_0 ≤ 2147483647;
+[eva] div.i:64: Frama_C_show_each_two: {2}
+[eva:alarm] div.i:67: Warning: 
+  signed overflow. assert x / min_one ≤ 2147483647;
+[eva] div.i:69: Frama_C_show_each: [-2147483647..2147483647]
+[eva:alarm] div.i:72: Warning: division by zero. assert x ≢ 0;
+[eva:alarm] div.i:72: Warning: 
+  signed overflow. assert min_int / x ≤ 2147483647;
+[eva] div.i:74: Frama_C_show_each: [-2147483648..2147483647]
+[eva:alarm] div.i:77: Warning: 
+  signed overflow. assert min_int / min_one ≤ 2147483647;
+[eva:alarm] div.i:82: Warning: division by zero. assert y ≢ 0;
+[eva:alarm] div.i:82: Warning: signed overflow. assert x / y ≤ 2147483647;
+[eva] Recording results for test_overflow_alarms
+[eva] Done for function test_overflow_alarms
 [eva] Recording results for main
 [eva] Done for function main
+[eva] div.i:77: assertion 'Eva,signed_overflow' got final status invalid.
 [scope:rm_asserts] removing 2 assertion(s)
 [eva] ====== VALUES COMPUTED ======
-[eva:final-states] Values at end of function main:
+[eva:final-states] Values at end of function test:
   X ∈ [--..--]
   Y ∈ [-126..333],9%27
   Z1 ∈ [-42..111],3%9
@@ -95,10 +110,60 @@
   e ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:37}) }}
   p ∈ {{ &t[3] }}
   c ∈ [--..--]
+[eva:final-states] Values at end of function test_overflow_alarms:
+  min_int ∈ {-2147483648}
+  min_one ∈ {-1}
+  a_0 ∈ {-2147483648; 10}
+  b_0 ∈ {-1; 2}
+  x ∈ [--..--]
+  y ∈ [--..--]
+  r ∈ [--..--]
+[eva:final-states] Values at end of function main:
+  X ∈ [--..--]
+  Y ∈ [-126..333],9%27
+  Z1 ∈ [-42..111],3%9
+  Z2 ∈ [-25..66]
+  T ∈ [34..493],7%27
+  U1 ∈ [11..164],2%9
+  U2 ∈ [6..98]
+  V ∈ [-125..334],10%27
+  W1 ∈ [-41..111]
+  W2 ∈ [-25..66]
+  a ∈ [-40000..40000]
+  b ∈ {{ garbled mix of &{Z2} (origin: Arithmetic {div.i:33}) }}
+  d1 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:35}) }}
+  d2 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:34}) }}
+  d0 ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:36}) }}
+  e ∈ {{ garbled mix of &{X} (origin: Arithmetic {div.i:37}) }}
+  p ∈ {{ &t[3] }}
+[from] Computing for function test
+[from] Done for function test
+[from] Computing for function test_overflow_alarms
+[from] Done for function test_overflow_alarms
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
   These dependencies hold at termination for the executions that terminate:
+[from] Function test:
+  X FROM X (and SELF)
+  Y FROM X
+  Z1 FROM X
+  Z2 FROM X
+  T FROM X
+  U1 FROM X
+  U2 FROM X
+  V FROM X
+  W1 FROM X
+  W2 FROM X
+  a FROM X
+  b FROM X
+  d1 FROM \nothing
+  d2 FROM \nothing
+  d0 FROM \nothing
+  e FROM \nothing
+  p FROM \nothing
+[from] Function test_overflow_alarms:
+  NO EFFECTS
 [from] Function main:
   X FROM X (and SELF)
   Y FROM X
@@ -118,7 +183,15 @@
   e FROM \nothing
   p FROM \nothing
 [from] ====== END OF DEPENDENCIES ======
-[inout] Out (internal) for function main:
+[inout] Out (internal) for function test:
     X; Y; Z1; Z2; T; U1; U2; V; W1; W2; a; b; d1; d2; d0; e; p; c
-[inout] Inputs for function main:
+[inout] Inputs for function test:
     X; Y; Z2; T; V
+[inout] Out (internal) for function test_overflow_alarms:
+    min_int; min_one; a_0; tmp; b_0; tmp_0; x; y; r
+[inout] Inputs for function test_overflow_alarms:
+    nondet
+[inout] Out (internal) for function main:
+    X; Y; Z1; Z2; T; U1; U2; V; W1; W2; a; b; d1; d2; d0; e; p
+[inout] Inputs for function main:
+    nondet; X; Y; Z2; T; V
diff --git a/tests/value/oracle/modulo.res.oracle b/tests/value/oracle/modulo.res.oracle
index 2735d95852af1642e100d42a180b75add289acd7..ae4d87e429f59ff097f62faef522546fe398506e 100644
--- a/tests/value/oracle/modulo.res.oracle
+++ b/tests/value/oracle/modulo.res.oracle
@@ -26,8 +26,8 @@
   b ∈ [--..--]
   i2 ∈ [--..--]
 [eva] computing for function pgcd1 <- main.
-  Called from modulo.i:163.
-[eva:alarm] modulo.i:163: Warning: 
+  Called from modulo.i:210.
+[eva:alarm] modulo.i:210: Warning: 
   function pgcd1: precondition got status unknown.
 [eva] modulo.i:37: loop invariant got status valid.
 [eva] modulo.i:38: loop invariant got status valid.
@@ -40,8 +40,8 @@
 [eva] Recording results for pgcd1
 [eva] Done for function pgcd1
 [eva] computing for function pgcd2 <- main.
-  Called from modulo.i:164.
-[eva:alarm] modulo.i:164: Warning: 
+  Called from modulo.i:211.
+[eva:alarm] modulo.i:211: Warning: 
   function pgcd2: precondition got status unknown.
 [eva] modulo.i:50: loop invariant got status valid.
 [eva] modulo.i:53: Frama_C_show_each_2: [-10..10], [1..10], [-9..9]
@@ -49,15 +49,15 @@
 [eva] Recording results for pgcd2
 [eva] Done for function pgcd2
 [eva] computing for function pgcd3 <- main.
-  Called from modulo.i:165.
-[eva:alarm] modulo.i:165: Warning: 
+  Called from modulo.i:212.
+[eva:alarm] modulo.i:212: Warning: 
   function pgcd3: precondition got status unknown.
 [eva:alarm] modulo.i:63: Warning: division by zero. assert b_0 ≢ 0;
 [eva] modulo.i:64: Frama_C_show_each_3: [-10..10], [-10..10], [-9..9]
 [eva] Recording results for pgcd3
 [eva] Done for function pgcd3
 [eva] computing for function main2 <- main.
-  Called from modulo.i:167.
+  Called from modulo.i:214.
 [eva:alarm] modulo.i:9: Warning: signed overflow. assert -2147483648 ≤ 4 * i;
 [eva:alarm] modulo.i:9: Warning: signed overflow. assert 4 * i ≤ 2147483647;
 [eva:alarm] modulo.i:10: Warning: signed overflow. assert -2147483648 ≤ 4 * i;
@@ -69,12 +69,12 @@
 [eva] Recording results for main2
 [eva] Done for function main2
 [eva] computing for function simultaneous_congruences <- main.
-  Called from modulo.i:168.
+  Called from modulo.i:215.
 [eva:alarm] modulo.i:76: Warning: assertion got status unknown.
 [eva] Recording results for simultaneous_congruences
 [eva] Done for function simultaneous_congruences
 [eva] computing for function shift_modulo <- main.
-  Called from modulo.i:169.
+  Called from modulo.i:216.
 [eva:alarm] modulo.i:100: Warning: assertion got status unknown.
 [eva:alarm] modulo.i:103: Warning: 
   signed overflow. assert (int)((int)(i * 12) + 5) << 25 ≤ 2147483647;
@@ -83,34 +83,61 @@
 [eva] Recording results for shift_modulo
 [eva] Done for function shift_modulo
 [eva] computing for function extract_bits_modulo <- main.
-  Called from modulo.i:170.
+  Called from modulo.i:217.
 [eva:alarm] modulo.i:109: Warning: assertion got status unknown.
 [eva] Recording results for extract_bits_modulo
 [eva] Done for function extract_bits_modulo
 [eva] computing for function pos_rem <- main.
-  Called from modulo.i:171.
+  Called from modulo.i:218.
 [eva:alarm] modulo.i:137: Warning: assertion got status unknown.
 [eva:alarm] modulo.i:142: Warning: assertion got status unknown.
 [eva:alarm] modulo.i:146: Warning: assertion got status unknown.
 [eva] Recording results for pos_rem
 [eva] Done for function pos_rem
 [eva] computing for function address_modulo <- main.
-  Called from modulo.i:172.
-[eva:garbled-mix:write] modulo.i:156: 
-  Assigning imprecise value to r because of arithmetic operation on addresses.
-[eva:alarm] modulo.i:157: Warning: division by zero. assert i ≢ 0;
-[eva:garbled-mix:write] modulo.i:157: 
-  Assigning imprecise value to r because of arithmetic operation on addresses.
+  Called from modulo.i:219.
 [eva:garbled-mix:write] modulo.i:158: 
   Assigning imprecise value to r because of arithmetic operation on addresses.
+[eva:alarm] modulo.i:159: Warning: division by zero. assert i ≢ 0;
 [eva:alarm] modulo.i:159: Warning: 
-  division by zero. assert (unsigned int)i ≢ 0;
+  signed overflow. assert addr / i ≤ 2147483647;
 [eva:garbled-mix:write] modulo.i:159: 
   Assigning imprecise value to r because of arithmetic operation on addresses.
+[eva:garbled-mix:write] modulo.i:160: 
+  Assigning imprecise value to r because of arithmetic operation on addresses.
+[eva:alarm] modulo.i:161: Warning: 
+  division by zero. assert (unsigned int)i ≢ 0;
+[eva:garbled-mix:write] modulo.i:161: 
+  Assigning imprecise value to r because of arithmetic operation on addresses.
 [eva] Recording results for address_modulo
 [eva] Done for function address_modulo
+[eva] computing for function test_overflow_alarms <- main.
+  Called from modulo.i:220.
+[eva:alarm] modulo.i:176: Warning: 
+  signed overflow. assert a_0 / b_0 ≤ 2147483647;
+[eva] modulo.i:178: Frama_C_show_each: {-2147483648; 10}, {-1; 2}
+[eva:alarm] modulo.i:181: Warning: 
+  signed overflow. assert a_0 / min_one ≤ 2147483647;
+[eva] modulo.i:183: Frama_C_show_each_ten: {10}
+[eva:alarm] modulo.i:186: Warning: 
+  signed overflow. assert min_int / b_0 ≤ 2147483647;
+[eva] modulo.i:188: Frama_C_show_each_two: {2}
+[eva:alarm] modulo.i:191: Warning: 
+  signed overflow. assert x / min_one ≤ 2147483647;
+[eva] modulo.i:193: Frama_C_show_each: [-2147483647..2147483647]
+[eva:alarm] modulo.i:196: Warning: division by zero. assert x ≢ 0;
+[eva:alarm] modulo.i:196: Warning: 
+  signed overflow. assert min_int / x ≤ 2147483647;
+[eva] modulo.i:198: Frama_C_show_each: [-2147483648..2147483647]
+[eva:alarm] modulo.i:201: Warning: 
+  signed overflow. assert min_int / min_one ≤ 2147483647;
+[eva:alarm] modulo.i:206: Warning: division by zero. assert y ≢ 0;
+[eva:alarm] modulo.i:206: Warning: signed overflow. assert x / y ≤ 2147483647;
+[eva] Recording results for test_overflow_alarms
+[eva] Done for function test_overflow_alarms
 [eva] Recording results for main
 [eva] Done for function main
+[eva] modulo.i:201: assertion 'Eva,signed_overflow' got final status invalid.
 [scope:rm_asserts] removing 2 assertion(s)
 [eva] ====== VALUES COMPUTED ======
 [eva:final-states] Values at end of function address_modulo:
@@ -118,7 +145,7 @@
   uaddr ∈ {{ (unsigned int)&A ; (unsigned int)&B }}
   addr ∈ {{ (int)&A ; (int)&B }}
   i ∈ [-99..99]
-  r ∈ {{ garbled mix of &{A; B} (origin: Arithmetic {modulo.i:159}) }}
+  r ∈ {{ garbled mix of &{A; B} (origin: Arithmetic {modulo.i:161}) }}
 [eva:final-states] Values at end of function extract_bits_modulo:
   i ∈ [0..10]
   aa1 ∈ [1291..32011],1291%3072
@@ -185,6 +212,14 @@
   o1 ∈ [11..268435451],11%24
   o2 ∈ [11..268435451],11%24
   o3 ∈ [11..268435451],11%24
+[eva:final-states] Values at end of function test_overflow_alarms:
+  min_int ∈ {-2147483648}
+  min_one ∈ {-1}
+  a_0 ∈ {-2147483648; 10}
+  b_0 ∈ {-1; 2}
+  x ∈ [--..--]
+  y ∈ [--..--]
+  r ∈ [--..--]
 [eva:final-states] Values at end of function main:
   A ∈ {0}
   B ∈ {-3; 1}
@@ -221,6 +256,8 @@
 [from] Done for function shift_modulo
 [from] Computing for function simultaneous_congruences
 [from] Done for function simultaneous_congruences
+[from] Computing for function test_overflow_alarms
+[from] Done for function test_overflow_alarms
 [from] Computing for function main
 [from] Done for function main
 [from] ====== DEPENDENCIES COMPUTED ======
@@ -259,6 +296,8 @@
   NO EFFECTS
 [from] Function simultaneous_congruences:
   NO EFFECTS
+[from] Function test_overflow_alarms:
+  NO EFFECTS
 [from] Function main:
   A FROM v
   B FROM v
@@ -315,6 +354,10 @@
     n1; n2; n3; m1; m2; o1; o2; o3
 [inout] Inputs for function simultaneous_congruences:
     i2
+[inout] Out (internal) for function test_overflow_alarms:
+    min_int; min_one; a_0; tmp; b_0; tmp_0; x; y; r
+[inout] Inputs for function test_overflow_alarms:
+    v
 [inout] Out (internal) for function main:
     A; B; C; D; E; F; G; H; I; J; K; L; M; N; O; P; Q
 [inout] Inputs for function main:
diff --git a/tests/value/oracle_equality/addition.res.oracle b/tests/value/oracle_equality/addition.res.oracle
index cfbd463cdffd29c09f0e53feed5f870850e73e5c..65ebb74096e4603daeeec2aae113e4432411625a 100644
--- a/tests/value/oracle_equality/addition.res.oracle
+++ b/tests/value/oracle_equality/addition.res.oracle
@@ -1,29 +1,30 @@
-129,134d128
+125,130d124
 < [eva:alarm] addition.i:61: Warning: 
 <   signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
 < [eva:alarm] addition.i:61: Warning: 
 <   signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
 < [eva:garbled-mix:write] addition.i:61: Warning: 
 <   Assigning imprecise value to p14 because of misaligned read of addresses.
-141c135,140
-< [scope:rm_asserts] removing 9 assertion(s)
----
+138a133,137
 > [eva:garbled-mix:summary] Warning: 
 >   Origins of garbled mix generated during analysis:
 >     addition.i:59: misaligned read of addresses
 >       (read in 1 statement, propagated through 2 statements)
 >       garbled mix of &{p1}
+140c139
+< [scope:rm_asserts] removing 9 assertion(s)
+---
 > [scope:rm_asserts] removing 7 assertion(s)
-165c164
+164c163
 <      {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
 ---
 >      {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}
-359,362d357
+354,357d352
 < [eva:alarm] addition.i:61: Warning: 
 <   signed overflow. assert -2147483648 ≤ (int)*((char *)(&q1)) + 2;
 < [eva:alarm] addition.i:61: Warning: 
 <   signed overflow. assert (int)*((char *)(&q1)) + 2 ≤ 2147483647;
-368c363,368
+365c360,365
 < [scope:rm_asserts] removing 9 assertion(s)
 ---
 > [eva:garbled-mix:summary] Warning: 
@@ -32,7 +33,7 @@
 >       (read in 1 statement, propagated through 2 statements)
 >       garbled mix of &{p1}
 > [scope:rm_asserts] removing 7 assertion(s)
-393c393
+390c390
 <      {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:61}) }}
 ---
 >      {{ garbled mix of &{p1} (origin: Misaligned read {addition.i:59}) }}