diff --git a/src/kernel_services/abstract_interp/abstract_memory.ml b/src/kernel_services/abstract_interp/abstract_memory.ml
index cbe6c0290882f4b68d2036bcce074358e61f93f5..74ef1091b7a0b7f18d17f1d7592547491ca89b7e 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.ml
+++ b/src/kernel_services/abstract_interp/abstract_memory.ml
@@ -285,11 +285,11 @@ end
 (* ------------------------------------------------------------------------ *)
 
 type side = Left | Right
-type oracle = Cil_types.exp -> Ival.t
+type oracle = Cil_types.exp -> Int_val.t
 type bioracle = side -> oracle
 type strength = Strong | Weak | Reinforce (* update strength *)
 
-let no_oracle = fun _exp -> Ival.top
+let no_oracle = fun _exp -> Int_val.top
 
 module type ProtoMemory =
 sig
@@ -810,17 +810,17 @@ struct
     | Const _ -> assert false (* should not happen ? even with absolute adresses ? *)
     | Ptroffset _ -> assert false (* Not produced by of_exp *)
 
-  (* Stupid oracle built from an Ival oracle *)
-  let to_ival ~oracle = function
-    | Const i -> Ival.inject_singleton i
-    | Exp (e, i) -> Ival.add_singleton_int i (oracle e)
+  (* Convert bound to interval using oracle *)
+  let to_int_val ~oracle = function
+    | Const i -> Int_val.inject_singleton i
+    | Exp (e, i) -> Int_val.add_singleton i (oracle e)
     | Ptroffset _ -> raise Not_implemented
 
   let to_integer ~oracle = function
     | Const i -> Some i
     | Exp (e, i) ->
       begin try
-          Some (Integer.add (Ival.project_int (oracle e)) i)
+          Some (Integer.add (Int_val.project_int (oracle e)) i)
         with Ival.Not_Singleton_Int ->
           None
       end
@@ -872,8 +872,8 @@ struct
       | Exp (e1, i1), Exp (e2, i2) when Exp.equal e1 e2 -> cmp_int i1 i2
       | Ptroffset _, _ | _, Ptroffset _ -> raise Not_implemented
       | _, _ ->
-        let r = Ival.sub_int (to_ival ~oracle b1) (to_ival ~oracle b2) in
-        match Ival.min_and_max r with
+        let r = Int_val.(add (to_int_val ~oracle b1) (neg (to_int_val ~oracle b2))) in
+        match Int_val.min_and_max r with
         | Some min, Some max when Integer.is_zero min && Integer.is_zero max ->
           Equal
         | Some l, _ when Integer.(ge l zero) ->
@@ -886,7 +886,7 @@ struct
     cmp ~oracle b1 b2 = Equal
 
   let lower_integer ~oracle b =
-    match Ival.min_int (to_ival ~oracle b) with
+    match Int_val.min_int (to_int_val ~oracle b) with
     | Some l -> `Value l
     | None ->
       Kernel.warning ~current:true "cannot retrieve lower bound for %a"
@@ -894,7 +894,7 @@ struct
       `Top
 
   let upper_integer ~oracle b =
-    match Ival.max_int (to_ival ~oracle b) with
+    match Int_val.max_int (to_int_val ~oracle b) with
     | Some u -> `Value u
     | None ->
       Kernel.warning ~current:true "cannot retrieve upper bound for %a"
@@ -945,7 +945,6 @@ struct
   let _incr vi i (b,a) = Bound.incr vi i b |> Option.map (fun b -> b,a)
   let incr_or_constantify ~oracle vi i (b,a) =
     Bound.incr_or_constantify ~oracle vi i b |> Option.map (fun b -> b,a)
-  let _to_ival ~oracle (b,_a) = Bound.to_ival ~oracle b
   let cmp ~oracle (b1,_a1) (b2,_a2) = Bound.cmp ~oracle b1 b2
   let eq ?oracle (b1,_a1) (b2,_a2) = Bound.eq ?oracle b1 b2
   let lower_bound ~oracle (b1,a1) (b2,a2) =
diff --git a/src/kernel_services/abstract_interp/abstract_memory.mli b/src/kernel_services/abstract_interp/abstract_memory.mli
index 3100daa6bbf1ac5faa13b742e5eca5e7d659947a..8586dcb9bb60e45407d35755e751f2a275de3f23 100644
--- a/src/kernel_services/abstract_interp/abstract_memory.mli
+++ b/src/kernel_services/abstract_interp/abstract_memory.mli
@@ -81,7 +81,7 @@ end
 
 
 type side = Left | Right
-type oracle = Cil_types.exp -> Ival.t
+type oracle = Cil_types.exp -> Int_val.t
 type bioracle = side -> oracle
 type strength = Strong | Weak | Reinforce (* update strength *)
 
diff --git a/src/plugins/value/domains/multidim_domain.ml b/src/plugins/value/domains/multidim_domain.ml
index 75473ca8fc09bb3fde3946ec72fa96e4ce6705ea..bb66be5a3218aa29210b243cc1fb70f30373d753 100644
--- a/src/plugins/value/domains/multidim_domain.ml
+++ b/src/plugins/value/domains/multidim_domain.ml
@@ -410,17 +410,6 @@ struct
     | Some s1, Some s2 -> Some (TrackedBases.union s1 s2)
 
 
-  (* Oracle conversion for Abstract_memory *)
-
-  let convert_oracle (oracle : Cil_types.exp -> value)
-    : Abstract_memory.oracle =
-    fun exp ->
-    try
-      Value.project_ival (oracle exp)
-    with Value.Not_based_on_null ->
-      Ival.top (* TODO: should it just not happen ? *)
-
-
   (* Accesses *)
 
   let read :
@@ -918,8 +907,8 @@ let multidim_hook (module Abstract: Abstractions.S) : (module Abstractions.S) =
           | `Value (_valuation,v) -> get_cval v
         in
         let oracle = function
-          | Abstract_memory.Left ->  Domain.convert_oracle (oracle a)
-          | Abstract_memory.Right -> Domain.convert_oracle (oracle b)
+          | Abstract_memory.Left ->  convert_oracle (oracle a)
+          | Abstract_memory.Right -> convert_oracle (oracle b)
         in
         let multidim = Domain.join' ~oracle (get_multidim a) (get_multidim b) in
         set key multidim r