diff --git a/src/plugins/eva/engine/compute_functions.ml b/src/plugins/eva/engine/compute_functions.ml
index 90a70b081ad5d1f6cfe4b9528a9c50647ef4c3f7..63265847a27f0bd79dc3af7c784c4d61f69777b9 100644
--- a/src/plugins/eva/engine/compute_functions.ml
+++ b/src/plugins/eva/engine/compute_functions.ml
@@ -220,7 +220,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
       end;
       apply_call_results_hooks call init_state (`Reuse i);
       (* call can be cached since it was cached once *)
-      Transfer.{states; cacheable = Cacheable; builtin=false}
+      Transfer.{ states; cacheable = Cacheable; }
 
   (* ----- Body or specification analysis ----------------------------------- *)
 
@@ -273,7 +273,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
     if Parameters.ValShowProgress.get () then
       Self.feedback
         "Done for function %a" Kernel_function.pretty call.kf;
-    Transfer.{ states = resulting_states; cacheable; builtin=false }
+    Transfer.{ states = resulting_states; cacheable; }
 
   (* ----- Use of cvalue builtins ------------------------------------------- *)
 
@@ -310,8 +310,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
     match final_state with
     | `Bottom ->
       apply_call_results_hooks call state (`Builtin ([], None));
-      let cacheable = Eval.Cacheable in
-      Transfer.{states; cacheable; builtin=true}
+      Transfer.{ states; cacheable = Eval.Cacheable; }
     | `Value final_state ->
       let cvalue_call = get_cvalue_call call in
       let post = get_cvalue_or_top final_state in
@@ -324,7 +323,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
         Abstract.Dom.set Cvalue_domain.State.key cvalue_state final_state
       in
       let states = List.map insert cvalue_states in
-      Transfer.{states; cacheable; builtin=true}
+      Transfer.{ states; cacheable; }
 
   (* Uses cvalue builtin only if the cvalue domain is available. Otherwise, only
      use the called function specification. *)
diff --git a/src/plugins/eva/engine/transfer_stmt.ml b/src/plugins/eva/engine/transfer_stmt.ml
index 2579ca24f8ae0dd9644b455e45ec8a18232cdb4b..bc4fc022505ea84a9461d0507229715fd5c467fa 100644
--- a/src/plugins/eva/engine/transfer_stmt.ml
+++ b/src/plugins/eva/engine/transfer_stmt.ml
@@ -41,7 +41,6 @@ module type S = sig
   type call_result = {
     states: (Partition.key * state) list;
     cacheable: Eval.cacheable;
-    builtin: bool;
   }
   val compute_call_ref:
     (stmt -> (loc, value) call -> recursion option -> state -> call_result) ref
@@ -295,7 +294,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
   type call_result = {
     states: (Partition.key * state) list;
     cacheable: cacheable;
-    builtin: bool;
   }
 
   (* Forward reference to [Eval_funs.compute_call] *)
@@ -304,8 +302,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
      call_result) ref
     = ref (fun _ -> assert false)
 
-  (* Returns the result of a call, and a boolean that indicates whether a
-     builtin has been used to interpret the call. *)
+  (* Returns the result of a call. *)
   let process_call stmt call recursion valuation state =
     Eva_utils.push_call_stack call.kf stmt;
     let cleanup () =
@@ -323,7 +320,7 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
           Domain.Store.register_initial_state callstack call.kf state;
           !compute_call_ref stmt call recursion state
         | `Bottom ->
-          { states = []; cacheable = Cacheable; builtin=false }
+          { states = []; cacheable = Cacheable; }
       in
       cleanup ();
       res
@@ -460,12 +457,6 @@ module Make (Abstract: Abstractions.S_with_evaluation) = struct
     (* Process the call according to the domain decision. *)
     let call_result = process_call stmt call recursion valuation state in
     let leaving_vars = leaving_vars kf_callee in
-    (* Do not try to reduce concrete arguments if a builtin was used. *)
-    let gather_reduced_arguments =
-      if call_result.builtin
-      then fun _ _ _ -> `Value []
-      else gather_reduced_arguments
-    in
     (* Treat each result one by one. *)
     let process state =
       (* Gathers the possible reductions on the value of the concrete arguments
diff --git a/src/plugins/eva/engine/transfer_stmt.mli b/src/plugins/eva/engine/transfer_stmt.mli
index 7da3e2be794787a059471923e14b7d7bdacf7260..8f5c2527e0cc2fce3e143a4bc011bb38df745c80 100644
--- a/src/plugins/eva/engine/transfer_stmt.mli
+++ b/src/plugins/eva/engine/transfer_stmt.mli
@@ -51,7 +51,6 @@ module type S = sig
   type call_result = {
     states: (Partition.key * state) list;
     cacheable: Eval.cacheable;
-    builtin: bool;
   }
 
   val compute_call_ref: