diff --git a/doc/value/main.tex b/doc/value/main.tex
index 7bb3bdb724081a1d77fcbec1e60d12f4469883ad..d485034cdb6a965447f03490f5da9a8a1b37de58 100644
--- a/doc/value/main.tex
+++ b/doc/value/main.tex
@@ -4287,7 +4287,7 @@ the precision improvement provided by the octagon domain.
 \begin{lstlisting}
 void main (int y) {
   int k = Frama_C_interval(0, 10);
-  int x = y + k;               // x - y $\in$ [0..10]
+  int x = y - k;               // y - x $\in$ [0..10]
   int r = x + 3 - y;           // r $\in$ [-7..3]
   int t;
   if (y > 15)
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index b8968a5f1396f409525488716e457c1baa70c8b9..af0b45ea28f600470f52018c2dbfc441a71a5565 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -91,7 +91,7 @@ type operation = Add | Sub
 module Arith = struct
   open Ival
 
-  let top_float = Ival.inject_float Fval.top
+  let is_top ival = Ival.(equal top ival || equal top_float ival)
 
   let narrow x y =
     let r = narrow x y in
@@ -133,25 +133,6 @@ module Arith = struct
     let min = Eval_typ.range_lower_bound range in
     let max = Eval_typ.range_upper_bound range in
     Ival.inject_range (Some min) (Some max)
-
-  (* Does an ival represent all values of a C type [typ]? *)
-  let is_top_for_typ typ ival =
-    let open Eval_typ in
-    Ival.(equal top ival) ||
-    match classify_as_scalar typ with
-    | None -> assert false
-    | Some (TSFloat _) -> Ival.equal top_float ival
-    | Some (TSInt range | TSPtr range) ->
-      (* TODO: this could be more efficient. *)
-      let range = make_range range in
-      Ival.is_included range ival || Ival.is_included range (neg_int ival)
-
-  (* Does an ival represent all possible values of a pair of variables? *)
-  let is_top_for_pair pair =
-    let x, y = Pair.get pair in
-    if Cil_datatype.Typ.equal x.vtype y.vtype
-    then is_top_for_typ x.vtype
-    else fun ival -> is_top_for_typ x.vtype ival && is_top_for_typ y.vtype ival
 end
 
 (* -------------------------------------------------------------------------- *)
@@ -176,20 +157,32 @@ let _pretty_octagon fmt octagon =
    Use Ival.t to evaluate expressions. *)
 module Rewriting = struct
 
+  let overflow_alarm range =
+    if range.Eval_typ.i_signed
+    then Kernel.SignedOverflow.get ()
+    else Kernel.UnsignedOverflow.get ()
+
+  let downcast_alarm range =
+    if range.Eval_typ.i_signed
+    then Kernel.SignedDowncast.get ()
+    else Kernel.UnsignedDowncast.get ()
+
   (* Checks if the interval [ival] fits in the C type [typ].
      This is used to ensure that an expression cannot overflow: this module
      uses the mathematical semantics of arithmetic operations, and cannot
      soundly translate overflows in the C semantics.  *)
-  let may_overflow typ ival =
+  let may_overflow ?(cast=false) typ ival =
     let open Eval_typ in
     match classify_as_scalar typ with
     | None -> assert false (* This should not happen here. *)
     | Some (TSFloat _) -> false
     | Some (TSInt range | TSPtr range) ->
-      not
-        ((range.i_signed && Kernel.SignedOverflow.get ()) ||
-         (not range.i_signed && Kernel.UnsignedOverflow.get ()) ||
-         Ival.is_included ival (Arith.make_range range))
+      let alarm =
+        if cast
+        then downcast_alarm range
+        else overflow_alarm range
+      in
+      not (alarm || Ival.is_included ival (Arith.make_range range))
 
   (* Simplified form [±X-coeff] for expressions,
      where X is a variable and coeff an interval. *)
@@ -264,7 +257,7 @@ module Rewriting = struct
     | CastE (typ, e) ->
       if Cil.(isIntegralType typ && isIntegralType (typeOf e)) then
         evaluate e >> fun v ->
-        if may_overflow typ v then [] else rewrite evaluate e
+        if may_overflow ~cast:true typ v then [] else rewrite evaluate e
       else []
 
     | Info (e, _) -> rewrite evaluate e
@@ -288,11 +281,7 @@ module Rewriting = struct
         in
         let value = Arith.add (Cil.typeOf e1) var1.coeff var2.coeff in
         let value = if sign then value else Arith.neg value in
-        (* Do not include this rewriting if the [value] exceeds all possible
-           values for the type of [var1] and [var2]. *)
-        if Arith.is_top_for_pair variables value
-        then acc
-        else (sign, { variables; operation; value }) :: acc
+        (sign, { variables; operation; value }) :: acc
     in
     Extlib.product_fold aux [] vars1 vars2
 
@@ -456,6 +445,8 @@ module Diamond = struct
 
   let top = { add = Ival.top; sub = Ival.top }
 
+  let is_top diamond = Arith.is_top diamond.add && Arith.is_top diamond.sub
+
   let is_included x y =
     Ival.is_included x.add y.add && Ival.is_included x.sub y.sub
 
@@ -473,16 +464,6 @@ module Diamond = struct
      about (Y, X). *)
   let reverse_variables swap t =
     if swap then { t with sub = Arith.neg t.sub } else t
-
-  (* Normalizes a diamond for the pair of variables [pair]: replaces too large
-     ivals by Ival.top. Returns None if both ivals are meaningless. *)
-  let trim pair t =
-    let is_top = Arith.is_top_for_pair pair in
-    match is_top t.add, is_top t.sub with
-    | true, true -> None
-    | true, false -> Some { t with add = Ival.top }
-    | false, true -> Some { t with sub = Ival.top }
-    | false, false -> Some t
 end
 
 
@@ -538,31 +519,31 @@ module Octagons = struct
 
   let narrow x y = try `Value (narrow_exc x y) with EBottom -> `Bottom
 
+  let decide join = fun _pair x y ->
+    let d = join x y in
+    if Diamond.is_top d then None else Some d
+
   let simple_join =
     let cache = Hptmap_sig.PersistentCache "Octagons.Octagons.join" in
-    let decide pair x y = Diamond.trim pair (Diamond.join x y) in
-    inter ~cache ~symmetric:true ~idempotent:true ~decide
+    inter ~cache ~symmetric:true ~idempotent:true ~decide:(decide Diamond.join)
 
   let join ~decide_left ~decide_right =
     let cache = Hptmap_sig.NoCache in
     let decide_left = Traversing decide_left
     and decide_right = Traversing decide_right in
-    let decide_both pair x y = Diamond.trim pair (Diamond.join x y) in
     merge ~cache ~symmetric:false ~idempotent:true
-      ~decide_left ~decide_right ~decide_both
+      ~decide_left ~decide_right ~decide_both:(decide Diamond.join)
 
   let simple_widen =
     let cache = Hptmap_sig.PersistentCache "Octagons.Octagons.widen" in
-    let decide pair x y = Diamond.trim pair (Diamond.widen x y) in
-    inter ~cache ~symmetric:false ~idempotent:true ~decide
+    inter ~cache ~symmetric:false ~idempotent:true ~decide:(decide Diamond.widen)
 
   let widen ~decide_left ~decide_right =
     let cache = Hptmap_sig.NoCache in
     let decide_left = Traversing decide_left
     and decide_right = Traversing decide_right in
-    let decide_both pair x y = Diamond.trim pair (Diamond.widen x y) in
     merge ~cache ~symmetric:false ~idempotent:true
-      ~decide_left ~decide_right ~decide_both
+      ~decide_left ~decide_right ~decide_both:(decide Diamond.widen)
 
   let unsafe_add = add
 
@@ -783,6 +764,24 @@ module State = struct
           "Incorrect octagon state computed by function %s:@ %a"
           msg pretty_debug t
 
+  (* Is an octagon no more precise than the intervals inferred for the related
+     variables? If so, do not save the octagon in the domain. *)
+  let is_redundant intervals { variables; operation; value; } =
+    if infer_intervals
+    then
+      try
+        let v1, v2 = Pair.get variables in
+        let i1 = Intervals.find v1 intervals
+        and i2 = Intervals.find v2 intervals in
+        let i = Arith.apply operation v1.vtype i1 i2 in
+        Ival.is_included i value
+      with Not_found -> false
+    else false
+
+  let is_redundant_diamond intervals variables diamond =
+    is_redundant intervals {variables; operation = Add; value = diamond.add} &&
+    is_redundant intervals {variables; operation = Sub; value = diamond.sub}
+
   (* ------------------------------ Lattice --------------------------------- *)
 
   let top =
@@ -815,7 +814,7 @@ module State = struct
             let add = Arith.add v1.vtype i1 i2
             and sub = Arith.sub v1.vtype i1 i2 in
             let diamond = Diamond.join diamond { add; sub } in
-            Diamond.trim pair diamond
+            if Diamond.is_top diamond then None else Some diamond
           with Not_found -> None
         in
         let decide_left = decide_empty t2.intervals
@@ -851,7 +850,7 @@ module State = struct
               then Diamond.widen { add; sub } diamond
               else Diamond.widen diamond { add; sub }
             in
-            Diamond.trim pair diamond
+            if Diamond.is_top diamond then None else Some diamond
           with Not_found -> None
         in
         let decide_left = decide_empty false t2.intervals
@@ -883,12 +882,12 @@ module State = struct
     { vars: varinfo * varinfo;
       diamond: diamond; }
 
-  let add_diamond state pair diamond =
-    match Diamond.trim pair diamond with
-    | None -> `Value state
-    | Some diamond ->
-      Octagons.add pair diamond state.octagons >>-: fun octagons ->
-      let relations = Relations.relate pair state.relations in
+  let add_diamond state variables diamond =
+    if is_redundant_diamond state.intervals variables diamond
+    then `Value state
+    else
+      Octagons.add variables diamond state.octagons >>-: fun octagons ->
+      let relations = Relations.relate variables state.relations in
       { state with octagons; relations }
 
   let inverse { vars; diamond } =
@@ -938,7 +937,7 @@ module State = struct
     with Not_found -> `Value state
 
   let add_octagon state octagon =
-    if Arith.is_top_for_pair octagon.variables octagon.value
+    if is_redundant state.intervals octagon
     then `Value state
     else
       let state =
diff --git a/tests/value/octagons.c b/tests/value/octagons.c
index fc671127c64355d57993d2c1a0c8cd42d780bb4d..101dafb7febcfda4bf4d2d67b16d71a76e55aa50 100644
--- a/tests/value/octagons.c
+++ b/tests/value/octagons.c
@@ -20,21 +20,48 @@ void demo () {
 /* Same example as [demo] but with other integer types. */
 void integer_types () {
   unsigned int k, x, y, r, t;
-  y = undet;
+  y = Frama_C_interval(0, 65536);
+  k = Frama_C_interval(0, 10);
+  x = y + k;        // An octagon should be inferred despite unsigned types.
+  r = x + 3 - y;
+  if (y < 300) {
+    t = x;
+    Frama_C_show_each_reduced_unsigned(r, t);
+  }
+  y = Frama_C_interval(0, 65536);
   k = Frama_C_interval(0, 10);
   x = y - k;        // No octagon inferred as [y - k] may overflow.
   r = x + 3 - y;
-  if (y > 15)
+  if (y < 300) {
     t = x;
-  Frama_C_show_each_unreduced_unsigned(r, t);
+    Frama_C_show_each_unreduced_unsigned(r, t);
+  }
   char ck, cx, cy, cr, ct;
-  cy = undet;
+  cy = Frama_C_interval(-100, 100);
   ck = Frama_C_interval(0, 10);
   cx = cy - ck;    // An octagon should be inferred despite the casts to int.
   cr = cx + 3 - cy;
-  if (cy > 15)
+  if (cy > 15) {
+    ct = cx;
+    Frama_C_show_each_reduced_char(cr, ct);
+  }
+  cy = undet;
+  ck = Frama_C_interval(0, 10);
+  cx = cy - ck;    // No octagon should be inferred as the downcast may wrap.
+  cr = cx + 3 - cy;
+  if (cy > 15) {
     ct = cx;
-  Frama_C_show_each_reduced_char(cr, ct);
+    Frama_C_show_each_unreduced_char(cr, ct);
+  }
+  int ix, ir, it;
+  cy = undet;
+  ck = Frama_C_interval(0, 10);
+  ix = cy - ck;    // An octagon should be inferred as there is no downcast.
+  ir = ix + 3 - cy;
+  if (cy > 15) {
+    it = ix;
+    Frama_C_show_each_reduced_int(ir, it);
+  }
 }
 
 /* A test with multiple mathematical operations to complicate the inference
@@ -177,9 +204,9 @@ void interprocedural () {
 /* Prints the octagons state. */
 void dump () {
   char k = Frama_C_interval(0, 8);
-  char a = undet;
-  char b = a + k;
-  char c = b - k;
+  int a = Frama_C_interval(-128, 128);
+  int b = a + k;
+  int c = b - k;
   Frama_C_dump_each();
 }
 
diff --git a/tests/value/oracle/octagons.res.oracle b/tests/value/oracle/octagons.res.oracle
index 46d13556ee25de9a20e4a82ef9748e1f62039dc3..a9c79497b39c79c8da9cb93f806e2a809d81d266 100644
--- a/tests/value/oracle/octagons.res.oracle
+++ b/tests/value/oracle/octagons.res.oracle
@@ -5,7 +5,7 @@
 [eva:initial-state] Values of globals at initialization
   undet ∈ [--..--]
 [eva] computing for function demo <- main.
-  Called from tests/value/octagons.c:200.
+  Called from tests/value/octagons.c:227.
 [eva] computing for function Frama_C_interval <- demo <- main.
   Called from tests/value/octagons.c:12.
 [eva] using specification for function Frama_C_interval
@@ -19,201 +19,244 @@
 [eva] Recording results for demo
 [eva] Done for function demo
 [eva] computing for function integer_types <- main.
-  Called from tests/value/octagons.c:201.
+  Called from tests/value/octagons.c:228.
+[eva] computing for function Frama_C_interval <- integer_types <- main.
+  Called from tests/value/octagons.c:23.
+[eva] tests/value/octagons.c:23: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- integer_types <- main.
   Called from tests/value/octagons.c:24.
 [eva] tests/value/octagons.c:24: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] tests/value/octagons.c:29: 
-  Frama_C_show_each_unreduced_unsigned: [0..4294967295], [0..4294967295]
+  Frama_C_show_each_reduced_unsigned: [3..13], [0..309]
+[eva] computing for function Frama_C_interval <- integer_types <- main.
+  Called from tests/value/octagons.c:31.
+[eva] tests/value/octagons.c:31: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- integer_types <- main.
   Called from tests/value/octagons.c:32.
 [eva] tests/value/octagons.c:32: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] tests/value/octagons.c:37: 
-  Frama_C_show_each_reduced_char: [-7..3], [6..127]
+  Frama_C_show_each_unreduced_unsigned: [0..4294967295], [0..4294967295]
+[eva] computing for function Frama_C_interval <- integer_types <- main.
+  Called from tests/value/octagons.c:40.
+[eva] tests/value/octagons.c:40: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] computing for function Frama_C_interval <- integer_types <- main.
+  Called from tests/value/octagons.c:41.
+[eva] tests/value/octagons.c:41: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:46: 
+  Frama_C_show_each_reduced_char: [-7..3], [6..100]
+[eva] computing for function Frama_C_interval <- integer_types <- main.
+  Called from tests/value/octagons.c:49.
+[eva] tests/value/octagons.c:49: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:54: 
+  Frama_C_show_each_unreduced_char: [-128..127], [-128..127]
+[eva] computing for function Frama_C_interval <- integer_types <- main.
+  Called from tests/value/octagons.c:58.
+[eva] tests/value/octagons.c:58: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:63: 
+  Frama_C_show_each_reduced_int: [-7..3], [6..127]
 [eva] Recording results for integer_types
 [eva] Done for function integer_types
 [eva] computing for function arith <- main.
-  Called from tests/value/octagons.c:202.
+  Called from tests/value/octagons.c:229.
 [eva] computing for function Frama_C_interval <- arith <- main.
-  Called from tests/value/octagons.c:43.
-[eva] tests/value/octagons.c:43: 
+  Called from tests/value/octagons.c:70.
+[eva] tests/value/octagons.c:70: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- arith <- main.
-  Called from tests/value/octagons.c:46.
-[eva] tests/value/octagons.c:46: 
+  Called from tests/value/octagons.c:73.
+[eva] tests/value/octagons.c:73: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- arith <- main.
-  Called from tests/value/octagons.c:47.
-[eva] tests/value/octagons.c:47: 
+  Called from tests/value/octagons.c:74.
+[eva] tests/value/octagons.c:74: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/octagons.c:52: Frama_C_show_each_precise: [42..66],0%2
-[eva] tests/value/octagons.c:54: Frama_C_show_each_imprecise: [2..106],0%2
+[eva] tests/value/octagons.c:79: Frama_C_show_each_precise: [42..66],0%2
+[eva] tests/value/octagons.c:81: Frama_C_show_each_imprecise: [2..106],0%2
 [eva] computing for function Frama_C_interval <- arith <- main.
-  Called from tests/value/octagons.c:55.
-[eva] tests/value/octagons.c:55: 
+  Called from tests/value/octagons.c:82.
+[eva] tests/value/octagons.c:82: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/octagons.c:59: Frama_C_show_each: {50; 60; 70}
+[eva] tests/value/octagons.c:86: Frama_C_show_each: {50; 60; 70}
 [eva] computing for function Frama_C_interval <- arith <- main.
-  Called from tests/value/octagons.c:62.
-[eva] tests/value/octagons.c:62: 
+  Called from tests/value/octagons.c:89.
+[eva] tests/value/octagons.c:89: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- arith <- main.
-  Called from tests/value/octagons.c:63.
-[eva] tests/value/octagons.c:63: 
+  Called from tests/value/octagons.c:90.
+[eva] tests/value/octagons.c:90: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/octagons.c:67: Frama_C_show_each: [-29..29]
+[eva] tests/value/octagons.c:94: Frama_C_show_each: [-29..29]
 [eva] Recording results for arith
 [eva] Done for function arith
 [eva] computing for function join <- main.
-  Called from tests/value/octagons.c:203.
+  Called from tests/value/octagons.c:230.
 [eva] computing for function Frama_C_interval <- join <- main.
-  Called from tests/value/octagons.c:76.
-[eva] tests/value/octagons.c:76: 
+  Called from tests/value/octagons.c:103.
+[eva] tests/value/octagons.c:103: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva:alarm] tests/value/octagons.c:79: Warning: 
+[eva:alarm] tests/value/octagons.c:106: Warning: 
   signed overflow. assert -2147483648 ≤ a + k;
-[eva:alarm] tests/value/octagons.c:79: Warning: 
+[eva:alarm] tests/value/octagons.c:106: Warning: 
   signed overflow. assert a + k ≤ 2147483647;
 [eva] computing for function Frama_C_interval <- join <- main.
-  Called from tests/value/octagons.c:81.
-[eva] tests/value/octagons.c:81: 
+  Called from tests/value/octagons.c:108.
+[eva] tests/value/octagons.c:108: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/octagons.c:86: Frama_C_show_each_join_positive: [0..53]
-[eva:alarm] tests/value/octagons.c:89: Warning: 
+[eva] tests/value/octagons.c:113: Frama_C_show_each_join_positive: [0..53]
+[eva:alarm] tests/value/octagons.c:116: Warning: 
   signed overflow. assert -2147483648 ≤ a + k;
-[eva:alarm] tests/value/octagons.c:89: Warning: 
+[eva:alarm] tests/value/octagons.c:116: Warning: 
   signed overflow. assert a + k ≤ 2147483647;
-[eva:alarm] tests/value/octagons.c:89: Warning: 
+[eva:alarm] tests/value/octagons.c:116: Warning: 
   signed overflow. assert -((int)(a + k)) ≤ 2147483647;
 [eva] computing for function Frama_C_interval <- join <- main.
-  Called from tests/value/octagons.c:91.
-[eva] tests/value/octagons.c:91: 
+  Called from tests/value/octagons.c:118.
+[eva] tests/value/octagons.c:118: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/octagons.c:96: Frama_C_show_each_join_negative: [-47..0]
+[eva] tests/value/octagons.c:123: Frama_C_show_each_join_negative: [-47..0]
 [eva] Recording results for join
 [eva] Done for function join
 [eva] computing for function loop <- main.
-  Called from tests/value/octagons.c:204.
+  Called from tests/value/octagons.c:231.
 [eva] computing for function Frama_C_interval <- loop <- main.
-  Called from tests/value/octagons.c:101.
-[eva] tests/value/octagons.c:101: 
+  Called from tests/value/octagons.c:128.
+[eva] tests/value/octagons.c:128: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- loop <- main.
-  Called from tests/value/octagons.c:102.
-[eva] tests/value/octagons.c:102: 
+  Called from tests/value/octagons.c:129.
+[eva] tests/value/octagons.c:129: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/octagons.c:106: starting to merge loop iterations
-[eva:alarm] tests/value/octagons.c:107: Warning: 
+[eva] tests/value/octagons.c:133: starting to merge loop iterations
+[eva:alarm] tests/value/octagons.c:134: Warning: 
   signed overflow. assert a + 2 ≤ 2147483647;
-[eva:alarm] tests/value/octagons.c:108: Warning: 
+[eva:alarm] tests/value/octagons.c:135: Warning: 
   signed overflow. assert b + 2 ≤ 2147483647;
-[eva:alarm] tests/value/octagons.c:110: Warning: 
+[eva:alarm] tests/value/octagons.c:137: Warning: 
   signed overflow. assert a + k ≤ 2147483647;
-[eva:alarm] tests/value/octagons.c:113: Warning: 
+[eva:alarm] tests/value/octagons.c:140: Warning: 
   signed overflow. assert -2147483648 ≤ c - a;
-[eva] tests/value/octagons.c:115: Frama_C_show_each_singleton_1: {1}
-[eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2147483648..1]
-[eva] tests/value/octagons.c:117: Frama_C_show_each_precise: [-8..8]
+[eva] tests/value/octagons.c:142: Frama_C_show_each_singleton_1: {1}
+[eva] tests/value/octagons.c:143: Frama_C_show_each_imprecise: [-2147483648..1]
+[eva] tests/value/octagons.c:144: Frama_C_show_each_precise: [-8..8]
 [eva] Recording results for loop
 [eva] Done for function loop
 [eva] computing for function pointers <- main.
-  Called from tests/value/octagons.c:205.
+  Called from tests/value/octagons.c:232.
 [eva] computing for function Frama_C_interval <- pointers <- main.
-  Called from tests/value/octagons.c:124.
-[eva] tests/value/octagons.c:124: 
+  Called from tests/value/octagons.c:151.
+[eva] tests/value/octagons.c:151: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/octagons.c:127: Frama_C_show_each_singleton_1: {1}
+[eva] tests/value/octagons.c:154: Frama_C_show_each_singleton_1: {1}
 [eva] computing for function Frama_C_interval <- pointers <- main.
-  Called from tests/value/octagons.c:128.
-[eva] tests/value/octagons.c:128: 
+  Called from tests/value/octagons.c:155.
+[eva] tests/value/octagons.c:155: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/octagons.c:129: Frama_C_show_each_singleton_1: {1}
+[eva] tests/value/octagons.c:156: Frama_C_show_each_singleton_1: {1}
 [eva] computing for function Frama_C_interval <- pointers <- main.
-  Called from tests/value/octagons.c:130.
-[eva] tests/value/octagons.c:130: 
+  Called from tests/value/octagons.c:157.
+[eva] tests/value/octagons.c:157: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/octagons.c:131: Frama_C_show_each_unknown: [-1024..1024]
-[eva] tests/value/octagons.c:133: Frama_C_show_each_unknown: [-2047..2049]
-[eva] tests/value/octagons.c:136: Frama_C_show_each_singleton_2: {2}
+[eva] tests/value/octagons.c:158: Frama_C_show_each_unknown: [-1024..1024]
+[eva] tests/value/octagons.c:160: Frama_C_show_each_unknown: [-2047..2049]
+[eva] tests/value/octagons.c:163: Frama_C_show_each_singleton_2: {2}
 [eva] Recording results for pointers
 [eva] Done for function pointers
 [eva] computing for function saturate <- main.
-  Called from tests/value/octagons.c:206.
+  Called from tests/value/octagons.c:233.
 [eva] computing for function Frama_C_interval <- saturate <- main.
-  Called from tests/value/octagons.c:142.
-[eva] tests/value/octagons.c:142: 
+  Called from tests/value/octagons.c:169.
+[eva] tests/value/octagons.c:169: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- saturate <- main.
-  Called from tests/value/octagons.c:143.
-[eva] tests/value/octagons.c:143: 
+  Called from tests/value/octagons.c:170.
+[eva] tests/value/octagons.c:170: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/octagons.c:147: Frama_C_show_each_saturate: [-5..5]
+[eva] tests/value/octagons.c:174: Frama_C_show_each_saturate: [-5..5]
 [eva] Recording results for saturate
 [eva] Done for function saturate
 [eva] computing for function interprocedural <- main.
-  Called from tests/value/octagons.c:207.
+  Called from tests/value/octagons.c:234.
 [eva] computing for function Frama_C_interval <- interprocedural <- main.
-  Called from tests/value/octagons.c:155.
-[eva] tests/value/octagons.c:155: 
+  Called from tests/value/octagons.c:182.
+[eva] tests/value/octagons.c:182: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- interprocedural <- main.
-  Called from tests/value/octagons.c:156.
-[eva] tests/value/octagons.c:156: 
+  Called from tests/value/octagons.c:183.
+[eva] tests/value/octagons.c:183: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function neg <- interprocedural <- main.
-  Called from tests/value/octagons.c:157.
+  Called from tests/value/octagons.c:184.
 [eva] Recording results for neg
 [eva] Done for function neg
 [eva] computing for function neg <- interprocedural <- main.
-  Called from tests/value/octagons.c:158.
+  Called from tests/value/octagons.c:185.
 [eva] Recording results for neg
 [eva] Done for function neg
 [eva] computing for function diff <- interprocedural <- main.
-  Called from tests/value/octagons.c:167.
+  Called from tests/value/octagons.c:194.
 [eva] Recording results for diff
 [eva] Done for function diff
 [eva] computing for function diff <- interprocedural <- main.
-  Called from tests/value/octagons.c:171.
+  Called from tests/value/octagons.c:198.
 [eva] Recording results for diff
 [eva] Done for function diff
-[eva] tests/value/octagons.c:174: 
+[eva] tests/value/octagons.c:201: 
   Frama_C_show_each_equal: [0..16], [0..16], [0..16]
 [eva] Recording results for interprocedural
 [eva] Done for function interprocedural
 [eva] computing for function dump <- main.
-  Called from tests/value/octagons.c:208.
+  Called from tests/value/octagons.c:235.
 [eva] computing for function Frama_C_interval <- dump <- main.
-  Called from tests/value/octagons.c:179.
-[eva] tests/value/octagons.c:179: 
+  Called from tests/value/octagons.c:206.
+[eva] tests/value/octagons.c:206: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
-[eva] tests/value/octagons.c:183: 
+[eva] computing for function Frama_C_interval <- dump <- main.
+  Called from tests/value/octagons.c:207.
+[eva] tests/value/octagons.c:207: 
+  function Frama_C_interval: precondition 'order' got status valid.
+[eva] Done for function Frama_C_interval
+[eva] tests/value/octagons.c:210: 
   Frama_C_dump_each:
   # octagon:
   {[ k - tmp ∈ {0}
      a - b ∈ [-8..0]
+     k - b ∈ [-128..128]
+     tmp - b ∈ [-128..128]
      b - c ∈ [0..8]
      a - c ∈ [-8..8]
       ]}
@@ -221,15 +264,15 @@
 [eva] Recording results for dump
 [eva] Done for function dump
 [eva] computing for function pub301 <- main.
-  Called from tests/value/octagons.c:209.
+  Called from tests/value/octagons.c:236.
 [eva] computing for function Frama_C_interval <- pub301 <- main.
-  Called from tests/value/octagons.c:189.
-[eva] tests/value/octagons.c:189: 
+  Called from tests/value/octagons.c:216.
+[eva] tests/value/octagons.c:216: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] computing for function Frama_C_interval <- pub301 <- main.
-  Called from tests/value/octagons.c:190.
-[eva] tests/value/octagons.c:190: 
+  Called from tests/value/octagons.c:217.
+[eva] tests/value/octagons.c:217: 
   function Frama_C_interval: precondition 'order' got status valid.
 [eva] Done for function Frama_C_interval
 [eva] Recording results for pub301
@@ -257,21 +300,24 @@
 [eva:final-states] Values at end of function dump:
   Frama_C_entropy_source ∈ [--..--]
   k ∈ [0..8]
-  a ∈ [--..--]
-  b ∈ [--..--]
-  c ∈ [--..--]
+  a ∈ [-128..128]
+  b ∈ [-128..136]
+  c ∈ [-128..128]
 [eva:final-states] Values at end of function integer_types:
   Frama_C_entropy_source ∈ [--..--]
   k ∈ [0..10]
   x ∈ [--..--]
-  y ∈ [--..--]
+  y ∈ [0..65536]
   r ∈ [--..--]
   t ∈ [--..--] or UNINITIALIZED
   ck ∈ [0..10]
   cx ∈ [--..--]
   cy ∈ [--..--]
-  cr ∈ [-7..3]
-  ct ∈ [6..127] or UNINITIALIZED
+  cr ∈ [--..--]
+  ct ∈ [--..--] or UNINITIALIZED
+  ix ∈ [-138..127]
+  ir ∈ [-7..3]
+  it ∈ [6..127] or UNINITIALIZED
 [eva:final-states] Values at end of function join:
   Frama_C_entropy_source ∈ [--..--]
   a ∈ [--..--]
@@ -394,9 +440,10 @@
 [inout] Out (internal) for function dump:
     Frama_C_entropy_source; k; tmp; a; b; c
 [inout] Inputs for function dump:
-    Frama_C_entropy_source; undet
+    Frama_C_entropy_source
 [inout] Out (internal) for function integer_types:
-    Frama_C_entropy_source; k; x; y; r; t; tmp; ck; cx; cy; cr; ct; tmp_0
+    Frama_C_entropy_source; k; x; y; r; t; tmp; tmp_0; tmp_1; tmp_2; ck; 
+    cx; cy; cr; ct; tmp_3; tmp_4; tmp_5; ix; ir; it; tmp_6
 [inout] Inputs for function integer_types:
     Frama_C_entropy_source; undet
 [inout] Out (internal) for function join:
diff --git a/tests/value/oracle_apron/octagons.res.oracle b/tests/value/oracle_apron/octagons.res.oracle
index b2debaf8695f5a2c207525d7fdc6463d64bce544..a7a5ddf92717b9b2036bb958a36bb86305fe96cb 100644
--- a/tests/value/oracle_apron/octagons.res.oracle
+++ b/tests/value/oracle_apron/octagons.res.oracle
@@ -1,4 +1,4 @@
-284,287c284,287
+330,333c330,333
 <   a ∈ [-1024..2147483647]
 <   b ∈ [-1023..2147483647]
 <   c ∈ [-1023..2147483647]
diff --git a/tests/value/oracle_equality/octagons.res.oracle b/tests/value/oracle_equality/octagons.res.oracle
index 8e32fb27d1dae1fdc6f8a36f2913f5e370871108..ff1a18108c46f0f5e6f216ab5000d8582e6e1136 100644
--- a/tests/value/oracle_equality/octagons.res.oracle
+++ b/tests/value/oracle_equality/octagons.res.oracle
@@ -1,8 +1,8 @@
-29c29
-<   Frama_C_show_each_unreduced_unsigned: [0..4294967295], [0..4294967295]
+65c65
+<   Frama_C_show_each_unreduced_char: [-128..127], [-128..127]
 ---
->   Frama_C_show_each_unreduced_unsigned: [0..4294967295], [6..4294967295]
-269c269
-<   t ∈ [--..--] or UNINITIALIZED
+>   Frama_C_show_each_unreduced_char: [-118..114], [6..127]
+317c317
+<   ct ∈ [--..--] or UNINITIALIZED
 ---
->   t ∈ [6..4294967295] or UNINITIALIZED
+>   ct ∈ [6..127] or UNINITIALIZED
diff --git a/tests/value/oracle_gauges/octagons.res.oracle b/tests/value/oracle_gauges/octagons.res.oracle
index 49fefa1dc489947ad79cb8b973f9804fbb184331..6ab421492c6a84392089836cfc831578220b98da 100644
--- a/tests/value/oracle_gauges/octagons.res.oracle
+++ b/tests/value/oracle_gauges/octagons.res.oracle
@@ -1,17 +1,17 @@
-121,128d120
-< [eva:alarm] tests/value/octagons.c:107: Warning: 
+157,164d156
+< [eva:alarm] tests/value/octagons.c:134: Warning: 
 <   signed overflow. assert a + 2 ≤ 2147483647;
-< [eva:alarm] tests/value/octagons.c:108: Warning: 
+< [eva:alarm] tests/value/octagons.c:135: Warning: 
 <   signed overflow. assert b + 2 ≤ 2147483647;
-< [eva:alarm] tests/value/octagons.c:110: Warning: 
+< [eva:alarm] tests/value/octagons.c:137: Warning: 
 <   signed overflow. assert a + k ≤ 2147483647;
-< [eva:alarm] tests/value/octagons.c:113: Warning: 
+< [eva:alarm] tests/value/octagons.c:140: Warning: 
 <   signed overflow. assert -2147483648 ≤ c - a;
-130c122
-< [eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2147483648..1]
+166c158
+< [eva] tests/value/octagons.c:143: Frama_C_show_each_imprecise: [-2147483648..1]
 ---
-> [eva] tests/value/octagons.c:116: Frama_C_show_each_imprecise: [-2468..1]
-284,287c276,279
+> [eva] tests/value/octagons.c:143: Frama_C_show_each_imprecise: [-2468..1]
+330,333c322,325
 <   a ∈ [-1024..2147483647]
 <   b ∈ [-1023..2147483647]
 <   c ∈ [-1023..2147483647]
@@ -21,7 +21,7 @@
 >   b ∈ [-181..1867]
 >   c ∈ [-602..1446]
 >   d ∈ [-190..1874]
-289c281
+335c327
 <   d2 ∈ [-2147483648..1]
 ---
 >   d2 ∈ [-2468..1]
diff --git a/tests/value/oracle_octagon/relations2.res.oracle b/tests/value/oracle_octagon/relations2.res.oracle
index 336fb1286049a2c995114562728531fdeaa60258..c1f57d34be28dd2a1af3ffc69c5bbf580b11c01b 100644
--- a/tests/value/oracle_octagon/relations2.res.oracle
+++ b/tests/value/oracle_octagon/relations2.res.oracle
@@ -23,6 +23,10 @@
 <   n ∈ [0..512]
 ---
 >   n ∈ [1..512]
+114c110
+<   n ∈ [0..512]
+---
+>   n ∈ [1..512]
 140c136
 <   len ∈ [--..--]
 ---