diff --git a/src/plugins/value/domains/abstract_domain.mli b/src/plugins/value/domains/abstract_domain.mli
index d45f5d4a2dbeeafe55f6acadc9af88fd7dee4a24..26ec10de0c74bb44fb033c0b895716ac1e2f6c32 100644
--- a/src/plugins/value/domains/abstract_domain.mli
+++ b/src/plugins/value/domains/abstract_domain.mli
@@ -112,6 +112,17 @@ module type Lattice = sig
       without impeding the analysis: [meet x y = `Value x] is always sound. *)
 end
 
+(** Context from the engine evaluation about a domain query. *)
+type evaluation_context = {
+  root: bool;
+  (** Is the queried expression the "root" expression being evaluated, or is it
+      a sub-expression? *)
+  subdivision: int;
+  (** Maximum number of subdivisions for the current evaluation.
+      See {!Subdivided_evaluation} for more details. *)
+  subdivided: bool;
+  (** Is the current evaluation a subdivision of the complete evaluation? *)
+}
 
 (** Extraction of information: queries for values or locations inferred by a
     domain about expressions and lvalues.
@@ -137,20 +148,29 @@ module type Queries = sig
            value of the expression [exp], and [o] is the origin of the value,
            which can be None. *)
 
+  (** When evaluating an expression, the evaluation engine asks the domains
+      for abstract values and alarms at each lvalue (via [extract_lval]) and
+      each sub-expressions (via [extract_expr]).
+      In these queries:
+      - [oracle] is an evaluation function and can be used to find the answer
+        by evaluating some others expressions, especially by relational domain.
+        No recursive evaluation should be done by this function.
+      - [context] record gives some information about
+        the current evaluation. *)
+
   (** Query function for compound expressions:
-      [eval oracle t exp] returns the known value of [exp] by the state [t].
-      [oracle] is an evaluation function and can be used to find the answer
-      by evaluating some others expressions, especially by relational domain.
-      No recursive evaluation should be done by this function. *)
+      [extract_expr ~oracle context t exp] returns the known value of [exp]
+      by the state [t]. See above for more details on queries. *)
   val extract_expr :
-    (exp -> value evaluated) ->
+    oracle:(exp -> value evaluated) -> evaluation_context ->
     state -> exp -> (value * origin option) evaluated
 
   (** Query function for lvalues:
-      [find oracle t lval typ loc] returns the known value stored at
-      the location [loc] of the left value [lval] of type [typ]. *)
+      [extract_lval ~oracle context t lval typ loc] returns the known value
+      stored at the location [loc] of the left value [lval] of type [typ].
+      See above for more details on queries. *)
   val extract_lval :
-    (exp -> value evaluated) ->
+    oracle:(exp -> value evaluated) -> evaluation_context ->
     state -> lval -> typ -> location -> (value * origin option) evaluated
 
   (** [backward_location state lval typ loc v] reduces the location [loc] of the
diff --git a/src/plugins/value/domains/apron/apron_domain.ml b/src/plugins/value/domains/apron/apron_domain.ml
index 3e3fb679f2888aeaa05d88ff27636c648b649703..9c2d3e85184dd5ab65a9e17762df7bb46f081255 100644
--- a/src/plugins/value/domains/apron/apron_domain.ml
+++ b/src/plugins/value/domains/apron/apron_domain.ml
@@ -487,10 +487,10 @@ module Make (Man : Input) = struct
          apron state, whose environment raises the Failure exception. *)
       | Z.Overflow | Failure _ -> top
 
-  let extract_expr _oracle state expr =
+  let extract_expr ~oracle:_ _context state expr =
     compute state expr (Cil.typeOf expr)
 
-  let extract_lval _oracle state lval typ _loc =
+  let extract_lval ~oracle:_ _context state lval typ _loc =
     let expr = Value_util.lval_to_exp lval in
     compute state expr typ
 
diff --git a/src/plugins/value/domains/cvalue/cvalue_domain.ml b/src/plugins/value/domains/cvalue/cvalue_domain.ml
index bc7868a1f805d6190468624a1ef56e91f041df07..efcf6121cb5254553ad56895acf5618d3143ffd3 100644
--- a/src/plugins/value/domains/cvalue/cvalue_domain.ml
+++ b/src/plugins/value/domains/cvalue/cvalue_domain.ml
@@ -40,7 +40,7 @@ module Model = struct
      function in cvalue_transfer. *)
   type origin = value
 
-  let extract_expr _ _ _ = `Value (Cvalue.V.top, None), Alarmset.all
+  let extract_expr _state _expr = `Value (Cvalue.V.top, None), Alarmset.all
 
   let indeterminate_alarms lval v =
     let open Cvalue.V_Or_Uninitialized in
@@ -112,7 +112,7 @@ module Model = struct
         let v = if Cvalue.V.is_bottom v then `Bottom else `Value (v, None) in
         v, alarms
 
-  let extract_lval _oracle state lval typ loc =
+  let extract_lval state lval typ loc =
     if Cil.isArithmeticOrPointerType typ
     then extract_scalar_lval state lval typ loc
     else extract_aggregate_lval state lval typ loc
@@ -201,9 +201,10 @@ module State = struct
 
   type origin = Model.origin
 
-  let extract_expr evaluate (s, _) expr = Model.extract_expr evaluate s expr
-  let extract_lval oracle (s, _) lval typ loc =
-    Model.extract_lval oracle s lval typ loc
+  let extract_expr ~oracle:_ _context (s, _) expr =
+    Model.extract_expr s expr
+  let extract_lval ~oracle:_ _context (s, _) lval typ loc =
+    Model.extract_lval s lval typ loc
   let backward_location (state, _) lval typ precise_loc value =
     Model.backward_location state lval typ precise_loc value
   let reduce_further _ _ _ = []
diff --git a/src/plugins/value/domains/domain_builder.ml b/src/plugins/value/domains/domain_builder.ml
index 090ec84a602a7c9abc8082d368c70d16c1738105..f19b48efa1217c95f8d54bc13b5930e2a7e4e2f0 100644
--- a/src/plugins/value/domains/domain_builder.ml
+++ b/src/plugins/value/domains/domain_builder.ml
@@ -69,8 +69,8 @@ module Make_Minimal
   let narrow x _y = `Value x
 
   let top_answer = `Value (Value.top, None), Alarmset.all
-  let extract_expr _oracle _state _expr = top_answer
-  let extract_lval _oracle _state _lval _typ _location = top_answer
+  let extract_expr ~oracle:_ _context _state _expr = top_answer
+  let extract_lval ~oracle:_ _context _state _lval _typ _location = top_answer
   let backward_location _state _lval _typ location value = `Value (location, value)
   let reduce_further _state _expr _value = []
 
@@ -187,15 +187,12 @@ module Complete_Simple_Cvalue (Domain: Simpler_domains.Simple_Cvalue)
 
     let narrow x _y = `Value x
 
-    let extract_expr _oracle state expr =
+    let extract_expr ~oracle:_ _context state expr =
       let v = Domain.extract_expr state expr >>-: fun v -> v, None in
       v, Alarmset.all
 
-    let extract_lval _oracle state lval typ location =
-      let v =
-        Domain.extract_lval state lval typ location >>-: fun v ->
-        v, None
-      in
+    let extract_lval ~oracle:_ _context state lval typ location =
+      let v = Domain.extract_lval state lval typ location >>-: fun v -> v, None in
       v, Alarmset.all
 
     let backward_location _state _lval _typ location value =
@@ -372,13 +369,14 @@ module Restrict
 
   let default_query = `Value (Value.top, None), Alarmset.all
 
-  let extract_expr oracle state expr =
-    make_query default_query (fun s -> Domain.extract_expr oracle s expr) state
+  let extract_expr ~oracle context state expr =
+    make_query default_query
+      (fun s -> Domain.extract_expr ~oracle context s expr) state
 
-  let extract_lval oracle state lval typ location =
+  let extract_lval ~oracle context state lval typ location =
     make_query
       default_query
-      (fun s -> Domain.extract_lval oracle s lval typ location)
+      (fun s -> Domain.extract_lval ~oracle context s lval typ location)
       state
 
   let backward_location state lval typ location value =
diff --git a/src/plugins/value/domains/domain_lift.ml b/src/plugins/value/domains/domain_lift.ml
index 1b0b7938ca82df8cea92695051efbf27b1d3babd..e93db09c859d1318841c5ef1a7fe69aa77b06b80 100644
--- a/src/plugins/value/domains/domain_lift.ml
+++ b/src/plugins/value/domains/domain_lift.ml
@@ -53,15 +53,16 @@ module Make
   type location = Convert.extended_location
   type origin = Domain.origin
 
-  let extract_expr oracle state exp =
+  let extract_expr ~oracle context state exp =
     let oracle exp = oracle exp >>=: Convert.restrict_val in
-    Domain.extract_expr oracle state exp >>=: fun (value, origin) ->
+    Domain.extract_expr ~oracle context state exp >>=: fun (value, origin) ->
     Convert.extend_val value, origin
 
-  let extract_lval oracle state lval typ loc =
+  let extract_lval ~oracle context state lval typ loc =
     let oracle exp = oracle exp >>=: Convert.restrict_val in
     let loc = Convert.restrict_loc loc in
-    Domain.extract_lval oracle state lval typ loc >>=: fun (value, origin) ->
+    Domain.extract_lval ~oracle context state lval typ loc
+    >>=: fun (value, origin) ->
     Convert.extend_val value, origin
 
   let backward_location state lval typ loc value =
diff --git a/src/plugins/value/domains/domain_product.ml b/src/plugins/value/domains/domain_product.ml
index 875cf9c4b655252059f607be6aed23572e7388e7..683892ef2dcc07bd5da22c1a3834d06a3437447a 100644
--- a/src/plugins/value/domains/domain_product.ml
+++ b/src/plugins/value/domains/domain_product.ml
@@ -89,15 +89,15 @@ module Make
       in
       value, alarms
 
-  let extract_expr oracle (left, right) expr =
+  let extract_expr ~oracle context (left, right) expr =
     merge
-      (Left.extract_expr oracle left expr)
-      (Right.extract_expr oracle right expr)
+      (Left.extract_expr ~oracle context left expr)
+      (Right.extract_expr ~oracle context right expr)
 
-  let extract_lval oracle (left, right) lval typ location =
+  let extract_lval ~oracle context (left, right) lval typ location =
     merge
-      (Left.extract_lval oracle left lval typ location)
-      (Right.extract_lval oracle right lval typ location)
+      (Left.extract_lval ~oracle context left lval typ location)
+      (Right.extract_lval ~oracle context right lval typ location)
 
   let backward_location (left, right) lval typ loc value =
     (* TODO: Loc.narrow *)
diff --git a/src/plugins/value/domains/equality/equality_domain.ml b/src/plugins/value/domains/equality/equality_domain.ml
index 45d2dd6562d0c784db4f6980fae40aae866ea40c..2849ec1f6f3181dc30a8be6536f26c0df68c57c9 100644
--- a/src/plugins/value/domains/equality/equality_domain.ml
+++ b/src/plugins/value/domains/equality/equality_domain.ml
@@ -239,12 +239,12 @@ module Make
       v, Alarmset.none
     | None -> `Value (Value.top, None), Alarmset.all
 
-  let extract_expr (oracle: exp -> Value.t evaluated) (equalities, _, _) expr =
+  let extract_expr ~oracle _context (equalities, _, _) expr =
     let expr = Cil.constFold true expr in
     let atom_e = HCE.of_exp expr in
     coop_eval oracle equalities atom_e
 
-  let extract_lval oracle (equalities, _, _) lval _typ _location =
+  let extract_lval ~oracle _context (equalities, _, _) lval _typ _location =
     let atom_lv = HCE.of_lval lval in
     coop_eval oracle equalities atom_lv
 
diff --git a/src/plugins/value/domains/gauges/gauges_domain.ml b/src/plugins/value/domains/gauges/gauges_domain.ml
index 2617cd55e4d2209f8ba7f71db8b619a5832baf30..0e41b58d91d365f7ca424a4da18bcda531159f6f 100644
--- a/src/plugins/value/domains/gauges/gauges_domain.ml
+++ b/src/plugins/value/domains/gauges/gauges_domain.ml
@@ -1259,10 +1259,10 @@ module D_Impl : Abstract_domain.S
 
   (* TODO: it would be interesting to return something here, but we
      currently need a valuation to perform the translation. *)
-  let extract_expr _oracle _state _exp =
+  let extract_expr ~oracle:_ _context _state _exp =
     `Value (Cvalue.V.top, None), Alarmset.all
 
-  let extract_lval _oracle state _lv typ loc =
+  let extract_lval ~oracle:_ _context state _lv typ loc =
     let v =
       try
         let b = loc_to_base (Precise_locs.imprecise_location loc) typ in
diff --git a/src/plugins/value/domains/inout_domain.ml b/src/plugins/value/domains/inout_domain.ml
index 15e5f00ee7c0766b97dfdb24037f082111de299c..a51098e16eb63723b7d82f5449f5e835ad5cf58f 100644
--- a/src/plugins/value/domains/inout_domain.ml
+++ b/src/plugins/value/domains/inout_domain.ml
@@ -271,8 +271,8 @@ module Internal
 
   let top_query = `Value (Cvalue.V.top, None), Alarmset.all
 
-  let extract_expr _oracle _state _expr = top_query
-  let extract_lval _oracle _state _lv _typ _locs = top_query
+  let extract_expr ~oracle:_ _context _state _expr = top_query
+  let extract_lval ~oracle:_ _context _state _lv _typ _locs = top_query
 
   let backward_location _state _lval _typ loc value =
     `Value (loc, value)
diff --git a/src/plugins/value/domains/octagons.ml b/src/plugins/value/domains/octagons.ml
index efce9ddb734dfa03ed131be2f42a91678b8b9243..2be0ff0dfa9e97bd2e36809c8ff2c47a932fa51b 100644
--- a/src/plugins/value/domains/octagons.ml
+++ b/src/plugins/value/domains/octagons.ml
@@ -1041,7 +1041,7 @@ module Domain = struct
 
   let top_value = `Value (Cvalue.V.top, None), Alarmset.all
 
-  let extract_expr oracle state expr =
+  let extract_expr ~oracle _context state expr =
     let evaluate_expr expr =
       match fst (oracle expr) with
       | `Bottom -> `Top (* should not happen *)
@@ -1059,7 +1059,7 @@ module Domain = struct
     then `Bottom, Alarmset.all
     else `Value (Cvalue.V.inject_ival ival, None), alarms
 
-  let extract_lval _oracle _t _lval _typ _loc = top_value
+  let extract_lval ~oracle:_ _context _t _lval _typ _loc = top_value
 
   let backward_location _t _lval _typ loc value = `Value (loc, value)
 
diff --git a/src/plugins/value/domains/offsm_domain.ml b/src/plugins/value/domains/offsm_domain.ml
index 2a4d4854be35e24a2e61f2971f7871f7c3996e9e..a2d8355c3e27b361b452e9898deb331a9b9d2d0c 100644
--- a/src/plugins/value/domains/offsm_domain.ml
+++ b/src/plugins/value/domains/offsm_domain.ml
@@ -163,7 +163,7 @@ module Internal  : Domain_builder.InputDomain
 
   let show_expr _valuation _state _fmt _expr = ()
 
-  let extract_expr _oracle _state _exp =
+  let extract_expr ~oracle:_ _context _state _exp =
     `Value (Offsm_value.Offsm.top, None), Alarmset.all
 
   (* Basic 'find' on a location *)
@@ -176,7 +176,7 @@ module Internal  : Domain_builder.InputDomain
     then Offsm_value.Offsm.top
     else O o
 
-  let extract_lval _oracle state _lv typ locs =
+  let extract_lval ~oracle:_ _context state _lv typ locs =
     let o =
       if Cil.typeHasQualifier "volatile" typ ||
          not (Cil.isArithmeticOrPointerType typ)
diff --git a/src/plugins/value/domains/simple_memory.ml b/src/plugins/value/domains/simple_memory.ml
index 6cabd4da3f2b5a85ee3fc9759ee9b3e4bae2ba1c..94a2f4c5f6ce72aa1a962f391fe0a76ef151b060 100644
--- a/src/plugins/value/domains/simple_memory.ml
+++ b/src/plugins/value/domains/simple_memory.ml
@@ -196,11 +196,12 @@ module Make_Internal (Info: sig val name: string end) (Value: Value) = struct
   (* This function returns the information known about the location
      corresponding to [_lv], so that it may be used by the engine during
      evaluation. *)
-  let extract_lval _oracle state _lv typ loc =
+  let extract_lval ~oracle:_ _context state _lv typ loc =
     let v = find loc typ state in
     `Value (v, None), Alarmset.all
 
-  let extract_expr _oracle _state _expr = `Value (Value.top, None), Alarmset.all
+  let extract_expr ~oracle:_ _context _state _expr =
+    `Value (Value.top, None), Alarmset.all
 
   let backward_location state _lval typ loc _value =
     let new_value = find loc typ state in
diff --git a/src/plugins/value/domains/symbolic_locs.ml b/src/plugins/value/domains/symbolic_locs.ml
index 61a33252c51d31025f65854ce43d425e7979d5cd..2c2f51d88a24600c8c1640d4496547dc9926f048 100644
--- a/src/plugins/value/domains/symbolic_locs.ml
+++ b/src/plugins/value/domains/symbolic_locs.ml
@@ -576,12 +576,12 @@ module Internal : Domain_builder.InputDomain
      this point. Hence, the alarms have already been emitted, and we can
      return [Alarmset.none]. *)
 
-  let extract_expr _oracle state expr =
+  let extract_expr ~oracle:_ _context state expr =
     match Memory.find_expr expr state with
     | None -> top_query
     | Some v -> `Value (v, None), Alarmset.none
 
-  let extract_lval _oracle state lv _typ _locs =
+  let extract_lval ~oracle:_ _context state lv _typ _locs =
     match Memory.find_lval lv state with
     | None -> top_query
     | Some v -> `Value (v, None), Alarmset.none
diff --git a/src/plugins/value/domains/traces_domain.ml b/src/plugins/value/domains/traces_domain.ml
index 5dd2ac5bb9d925a853d14ac89d3c1fdb904bed86..ce718b03ee17ad5b2c30afd9a4d08658f3b5f7ee 100644
--- a/src/plugins/value/domains/traces_domain.ml
+++ b/src/plugins/value/domains/traces_domain.ml
@@ -942,8 +942,8 @@ module Internal = struct
 
   let top_query = `Value (Cvalue.V.top, None), Alarmset.all
 
-  let extract_expr _oracle _state _expr = top_query
-  let extract_lval _oracle _state _lv _typ _locs = top_query
+  let extract_expr ~oracle:_ _context _state _expr = top_query
+  let extract_lval ~oracle:_ _context _state _lv _typ _locs = top_query
 
   let backward_location _state _lval _typ loc value =
     `Value (loc, value)
diff --git a/src/plugins/value/domains/unit_domain.ml b/src/plugins/value/domains/unit_domain.ml
index 75a3db212865817be796939c17f668328012e533..5633d599dd564bf5884cb63af702ffe887c5eac9 100644
--- a/src/plugins/value/domains/unit_domain.ml
+++ b/src/plugins/value/domains/unit_domain.ml
@@ -55,8 +55,8 @@ module Make
   type origin
 
   let eval_top = `Value (Value.top, None), Alarmset.all
-  let extract_expr _ _ _ = eval_top
-  let extract_lval _ _ _ _ _ = eval_top
+  let extract_expr ~oracle:_ _ _ _ = eval_top
+  let extract_lval ~oracle:_ _ _ _ _ _ = eval_top
   let backward_location _ _ _ loc value = `Value (loc, value)
   let reduce_further _ _ _  = []
 
diff --git a/src/plugins/value/engine/evaluation.ml b/src/plugins/value/engine/evaluation.ml
index 5e0eee53d7c87d3dd5bdff036883af2071653046..0e2a13fd90ec36d6cc41ae61740b9c272e18229d 100644
--- a/src/plugins/value/engine/evaluation.ml
+++ b/src/plugins/value/engine/evaluation.ml
@@ -764,9 +764,14 @@ module Make
   type context =
     { (* The abstract domain state in which the evaluation takes place. *)
       state: Domain.t;
+      (* Is the expression currently processed the "root" expression being
+         evaluated, or is it a sub-expression? Useful for domain queries. *)
+      root: bool;
       (* Maximum number of subdivisions. See {!Subdivided_evaluation} for
          more details. *)
       subdivision: int;
+      (* Is the current evaluation subdivided? *)
+      subdivided: bool;
       (* The remaining fuel: maximum number of nested oracle uses, decremented
          at each call to the oracle. *)
       remaining_fuel: int;
@@ -775,8 +780,12 @@ module Make
       oracle: context -> exp -> Value.t evaluated;
     }
 
-  (* Builds the oracle from the context. *)
-  let make_oracle context = context.oracle context
+  (* Builds the query to the domain from the context. *)
+  let make_domain_query query context =
+    let { state; oracle; root; subdivision; subdivided; } = context in
+    let oracle = oracle context in
+    let domain_context = Abstract_domain.{ root; subdivision; subdivided; } in
+    query ~oracle domain_context state
 
   (* Returns the cached value and alarms for the evaluation if it exists;
      call [coop_forward_eval] and caches its result otherwise.
@@ -831,10 +840,10 @@ module Make
     match expr.enode with
     | Lval lval -> eval_lval context lval
     | BinOp _ | UnOp _ | CastE _ -> begin
+        let domain_query = make_domain_query Domain.extract_expr context in
+        let context = { context with root = false } in
         let intern_value, alarms = internal_forward_eval context expr in
-        let state = context.state in
-        let oracle = make_oracle context in
-        let domain_value, alarms' = Domain.extract_expr oracle state expr in
+        let domain_value, alarms' = domain_query expr in
         (* Intersection of alarms, as each sets of alarms are correct
            and "complete" for the evaluation of [expr]. *)
         match Alarmset.inter alarms alarms' with
@@ -1061,6 +1070,8 @@ module Make
       off, typ_res, volatile
 
   and eval_lval ?(indeterminate=false) context lval =
+    let domain_query = make_domain_query Domain.extract_lval context in
+    let context = { context with root = false } in
     (* Computes the location of [lval]. *)
     lval_to_loc context ~for_writing:false ~reduction:true lval
     >>= fun (loc, typ_lv, volatile_expr) ->
@@ -1072,8 +1083,7 @@ module Make
     *)
     let volatile = volatile_expr || Cil.typeHasQualifier "volatile" typ_lv in
     (* Find the value of the location, if not bottom. *)
-    let oracle = make_oracle context in
-    let v, alarms = Domain.extract_lval oracle context.state lval typ_lv loc in
+    let v, alarms = domain_query lval typ_lv loc in
     let alarms = close_dereference_alarms lval alarms in
     if indeterminate
     then
@@ -1098,8 +1108,13 @@ module Make
      the reference for the oracle given to the domains. *)
   module Forward_Evaluation = struct
     type nonrec context = context
-    let evaluate context valuation expr =
+    let evaluate ~subdivided context valuation expr =
       cache := valuation;
+      let context =
+        if subdivided
+        then { context with root = false; subdivided }
+        else context
+      in
       root_forward_eval context expr >>=: fun (value, _) ->
       !cache, value
   end
@@ -1133,14 +1148,17 @@ module Make
       | None -> Value_parameters.LinearLevel.get ()
       | Some n -> n
     in
-    { state; subdivision; remaining_fuel; oracle }
+    let subdivided = false in
+    { state; root = true; subdivision; subdivided; remaining_fuel; oracle }
 
   (* Context for a fast forward evaluation with minimal precision:
-     no subdivisions and no calls to the oracle. *)
+     no subdivisions, no calls to the oracle, and the expression is not
+     considered as a "root" expression. *)
   let fast_eval_context state =
     let remaining_fuel = no_fuel in
     let subdivision = 0 in
-    { state; subdivision; remaining_fuel; oracle }
+    let subdivided = false in
+    { state; root = false; subdivision; subdivided; remaining_fuel; oracle }
 
   let subdivided_forward_eval valuation ?subdivnb state expr =
     let context = root_context ?subdivnb state in
diff --git a/src/plugins/value/engine/subdivided_evaluation.ml b/src/plugins/value/engine/subdivided_evaluation.ml
index 5add03da573e8305fdd83712ab66e1b276f5c563..ac6f7ec43022ebb5850cf0e972d2d616a3b097f6 100644
--- a/src/plugins/value/engine/subdivided_evaluation.ml
+++ b/src/plugins/value/engine/subdivided_evaluation.ml
@@ -360,7 +360,8 @@ module type Forward_Evaluation = sig
   type value
   type valuation
   type context
-  val evaluate: context -> valuation -> exp -> (valuation * value) evaluated
+  val evaluate: subdivided:bool -> context -> valuation ->
+    exp -> (valuation * value) evaluated
 end
 
 module Make
@@ -663,7 +664,7 @@ module Make
       (* Updates [variables] with their new [subvalues]. *)
       let valuation = update_variables cleared_valuation variables subvalues in
       (* Evaluates [expr] with this new valuation. *)
-      let eval, alarms = Eva.evaluate context valuation expr in
+      let eval, alarms = Eva.evaluate ~subdivided:true context valuation expr in
       let result = eval >>-: snd in
       (* Optimization if [subexpr] = [expr]. *)
       if eq_equal_subexpr
@@ -711,7 +712,8 @@ module Make
     (* Reevaluates the lvalue in the initial state, as its value could have
        been reduced in the evaluation of the complete expression, and we cannot
        omit the alarms for the removed values. *)
-    fst (Eva.evaluate context valuation lv_expr) >>- fun (valuation, _) ->
+    fst (Eva.evaluate ~subdivided:true context valuation lv_expr)
+    >>- fun (valuation, _) ->
     let lv_record = find_val valuation lv_expr in
     lv_record.value.v >>-: fun lv_value ->
     { lval; lv_expr; lv_record; lv_value }
@@ -736,7 +738,8 @@ module Make
   (* Subdivided evaluation of [expr] in state [state]. *)
   let subdivide_evaluation context initial_valuation subdivnb expr =
     (* Evaluation of [expr] without subdivision. *)
-    let default = Eva.evaluate context initial_valuation expr in
+    let subdivided = false in
+    let default = Eva.evaluate ~subdivided context initial_valuation expr in
     default >>> fun valuation result alarms ->
     (* Do not try to subdivide if the result is singleton or contains some
        pointers: the better_bound heuristic only works on numerical values. *)
@@ -792,14 +795,14 @@ module Make
               let valuation =
                 Clear.clear_englobing_exprs valuation ~expr ~subexpr
               in
-              Eva.evaluate context valuation expr >>>
+              Eva.evaluate ~subdivided:true context valuation expr >>>
               subdivide_subexpr tail
       in
       subdivide_subexpr vars_info valuation result alarms
 
   let evaluate context valuation ~subdivnb expr =
     if subdivnb = 0 || not activated
-    then Eva.evaluate context valuation expr
+    then Eva.evaluate ~subdivided:false context valuation expr
     else subdivide_evaluation context valuation subdivnb expr
 
 
@@ -895,7 +898,7 @@ module Make
     let condition_may_still_be_true valuation expr record value =
       let value = { record.value with v = `Value value } in
       let valuation = Valuation.add valuation expr { record with value } in
-      let eval, _alarms = Eva.evaluate context valuation cond in
+      let eval = fst (Eva.evaluate ~subdivided:true context valuation cond) in
       match eval with
       | `Bottom -> false
       | `Value (_valuation, value) ->
diff --git a/src/plugins/value/engine/subdivided_evaluation.mli b/src/plugins/value/engine/subdivided_evaluation.mli
index 490832670d52a3fbd60822e8f1a7256a6da5bc03..be28558034c513c950bd34e8931bd11bae4d7197 100644
--- a/src/plugins/value/engine/subdivided_evaluation.mli
+++ b/src/plugins/value/engine/subdivided_evaluation.mli
@@ -31,7 +31,8 @@ module type Forward_Evaluation = sig
   type value
   type valuation
   type context
-  val evaluate: context -> valuation -> exp -> (valuation * value) evaluated
+  val evaluate: subdivided:bool -> context -> valuation ->
+    exp -> (valuation * value) evaluated
 end
 
 module Make