diff --git a/src/plugins/reduc/hyp.ml b/src/plugins/reduc/hyp.ml
index fc4fabf2763c7db2b26efafaf8ff26481de7d763..882e9a63c23a6ced23e34a1659c72bf432903e9d 100644
--- a/src/plugins/reduc/hyp.ml
+++ b/src/plugins/reduc/hyp.ml
@@ -36,12 +36,11 @@ class hypotheses_visitor (env: Collect.env) = object(self)
 
   method! vstmt_aux stmt =
     let kf = Option.get (self#current_kf) in
-    let state = Db.Value.get_stmt_state stmt in
     if Collect.should_annotate_stmt env stmt then begin
       let vars = Collect.get_relevant_vars_stmt env kf stmt in
       List.iter
         (fun e ->
-           let p_opt = pred_opt_from_expr_state state e in
+           let p_opt = pred_opt_from_expr_state stmt e in
            Option.iter (Misc.assert_and_validate ~kf stmt) p_opt)
         vars
     end;
diff --git a/src/plugins/reduc/value2acsl.ml b/src/plugins/reduc/value2acsl.ml
index c91d1ba6992418ffebcea1371b2b587aa9d5ea36..e5201a791ccb73bde0919c6831745d8c63026293 100644
--- a/src/plugins/reduc/value2acsl.ml
+++ b/src/plugins/reduc/value2acsl.ml
@@ -165,15 +165,13 @@ let value_to_predicate_opt ?(loc=Location.unknown) t v =
     with
     | Not_based_on_null -> (* base_offsets_to_predicate ~loc t m *) None
 
-let exp_to_predicate ?(loc=Location.unknown) state e =
-  let value = !Db.Value.eval_expr ~with_alarms:CilE.warn_none_mode state e in
+let exp_to_predicate ?(loc=Location.unknown) stmt e =
+  let value = Eva.Results.(before stmt |> eval_exp e |> as_ival) in
   let te = Logic_utils.expr_to_term ~coerce:false e in
-  value_to_predicate_opt ~loc te value
+  Option.bind (Result.to_option value) (ival_to_predicate_opt ~loc te)
 
-let lval_to_predicate ?(loc=Location.unknown) state lv =
-  let value = snd(!Db.Value.eval_lval
-                    ~with_alarms:CilE.warn_none_mode None state lv)
-  in
+let lval_to_predicate ?(loc=Location.unknown) stmt lv =
+  let value = Eva.Results.(before stmt |> eval_lval lv |> as_ival) in
   let e = Cil.new_exp ~loc (Lval lv) in
   let te = Logic_utils.expr_to_term ~coerce:false e in
-  value_to_predicate_opt ~loc te value
+  Option.bind (Result.to_option value) (ival_to_predicate_opt ~loc te)
diff --git a/src/plugins/reduc/value2acsl.mli b/src/plugins/reduc/value2acsl.mli
index 17546299c2191a9c2c5ea076b463904ccd48ed60..4d1aacea7b09d36abda69936d9016a77a3150b6a 100644
--- a/src/plugins/reduc/value2acsl.mli
+++ b/src/plugins/reduc/value2acsl.mli
@@ -27,5 +27,5 @@ open Cil_types
    @return None if no such predicate can be created. *)
 val value_to_predicate_opt: ?loc:location -> term -> Cvalue.V.t -> predicate option
 
-val lval_to_predicate: ?loc:location -> Cvalue.Model.t -> lval -> predicate option
-val exp_to_predicate: ?loc:location -> Cvalue.Model.t -> exp -> predicate option
+val lval_to_predicate: ?loc:location -> Cil_types.stmt -> lval -> predicate option
+val exp_to_predicate: ?loc:location -> Cil_types.stmt -> exp -> predicate option