diff --git a/src/plugins/value/engine/analysis.ml b/src/plugins/value/engine/analysis.ml
index 06c72bf50993d410b025682e5ee4f2ab914a45a9..256e3db49ab2a6777e173761dc06633b9cb20204 100644
--- a/src/plugins/value/engine/analysis.ml
+++ b/src/plugins/value/engine/analysis.ml
@@ -40,10 +40,11 @@ module type Results = sig
   val eval_lval_to_loc: state -> lval -> location evaluated
   val eval_function_exp:
     state -> ?args:exp list -> exp ->  kernel_function list evaluated
+  val assume_cond : stmt -> state -> exp -> bool -> state or_bottom
 end
 
 module type S = sig
-  include Abstractions.S
+  include Abstractions.Eva
   include Results with type state := Dom.state
                    and type value := Val.t
                    and type location := Loc.location
@@ -95,6 +96,11 @@ module Make (Abstract: Abstractions.S) = struct
   let eval_function_exp state ?args e =
     Eval.eval_function_exp e ?args state >>=: (List.map fst)
 
+  let assume_cond stmt state cond positive =
+    fst (Eval.reduce state cond positive) >>- fun valuation ->
+    let dval = Eval.to_domain_valuation valuation in
+    Dom.assume stmt cond positive dval state
+
 end
 
 
diff --git a/src/plugins/value/engine/analysis.mli b/src/plugins/value/engine/analysis.mli
index e96f3ed5ea11ade74b0b3a80210df1757d26e5db..6f85061797c199d610235ce9328d34203f91b6ae 100644
--- a/src/plugins/value/engine/analysis.mli
+++ b/src/plugins/value/engine/analysis.mli
@@ -40,6 +40,7 @@ module type Results = sig
   val eval_lval_to_loc: state -> lval -> location evaluated
   val eval_function_exp:
     state -> ?args:exp list -> exp -> kernel_function list evaluated
+  val assume_cond : stmt -> state -> exp -> bool -> state or_bottom
 end
 
 
@@ -55,7 +56,7 @@ end
 
 
 module type S = sig
-  include Abstractions.S
+  include Abstractions.Eva
   include Results with type state := Dom.state
                    and type value := Val.t
                    and type location := Loc.location