diff --git a/src/plugins/eva/domains/cvalue/builtins_misc.ml b/src/plugins/eva/domains/cvalue/builtins_misc.ml
index 93fbcf970dc1d94407aa23aed067188751b4f5b3..47d8da9c980db7c8e0dad4beb6625dd7aef98d90 100644
--- a/src/plugins/eva/domains/cvalue/builtins_misc.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_misc.ml
@@ -22,6 +22,7 @@
 
 open Eva_utils
 
+open Lattice_bounds.Bottom.Operators
 
 let frama_C_assert state actuals =
   let do_bottom () =
@@ -35,10 +36,14 @@ let frama_C_assert state actuals =
       then do_bottom ()
       else if Cvalue.V.contains_zero arg
       then begin
-        let state = !Db.Value.reduce_by_cond state arg_exp true in
-        if Cvalue.Model.is_reachable state
-        then (warning_once_current "Frama_C_assert: unknown"; state)
-        else do_bottom ()
+        let state =
+          let* valuation = fst (Cvalue_queries.reduce state arg_exp true) in
+          let valuation = Cvalue_queries.to_domain_valuation valuation in
+          Cvalue_transfer.update valuation state
+        in
+        match state with
+        | `Value state -> warning_once_current "Frama_C_assert: unknown"; state
+        | `Bottom -> do_bottom ()
       end
       else begin
         warning_once_current "Frama_C_assert: true";
diff --git a/src/plugins/eva/domains/cvalue/builtins_split.ml b/src/plugins/eva/domains/cvalue/builtins_split.ml
index 5d6721b188a2ca2c2efc6d93ea2834e83db29bb5..a6a2cf2812a911993cd1ed76bfefdec413ca2933 100644
--- a/src/plugins/eva/domains/cvalue/builtins_split.ml
+++ b/src/plugins/eva/domains/cvalue/builtins_split.ml
@@ -74,7 +74,7 @@ let warning warn s =
    [max_card] elements. *)
 let split_v ~warn lv state max_card =
   if Cil.isArithmeticOrPointerType (Cil.typeOfLval lv) then
-    let loc = !Db.Value.lval_to_loc_state state lv in
+    let loc = Cvalue_queries.lval_to_loc state lv in
     if Locations.Location_Bits.cardinal_zero_or_one loc.Locations.loc then
       let v_indet = Cvalue.Model.find_indeterminate state loc in
       let v = Cvalue.V_Or_Uninitialized.get_v v_indet in
diff --git a/src/plugins/eva/utils/widen.ml b/src/plugins/eva/utils/widen.ml
index 2e4564b4ef0045ac2a79a43c30aacd65a2b2687f..b26bb71371f86aef95114f2fda4217a5348188b6 100644
--- a/src/plugins/eva/utils/widen.ml
+++ b/src/plugins/eva/utils/widen.ml
@@ -499,7 +499,7 @@ module Parsed_Dynamic_Hints =
 let dynamic_bases_of_lval states e offset =
   let lv = (Mem e, offset) in
   List.fold_left (fun acc' state ->
-      let location = !Db.Value.lval_to_loc_state state lv in
+      let location = Cvalue_queries.lval_to_loc state lv in
       Locations.Location_Bits.fold_bases
         (fun base acc'' -> Base.Hptset.add base acc'')
         location.Locations.loc acc'