diff --git a/src/core/external.ml b/src/core/external.ml
index 20cc419a..9b16feef 100644
--- a/src/core/external.ml
+++ b/src/core/external.ml
@@ -68,10 +68,7 @@ module Make
     { unsat_conflict; get_proof; }
 
   (* Wrappers around internal functions*)
-  let assume ?tag l =
-    try
-      S.assume ?tag l
-    with S.Unsat -> ()
+  let assume = S.assume
 
   let solve ?(assumptions=[]) () =
     try
diff --git a/src/core/internal.mli b/src/core/internal.mli
index 1f9a50ac..b9b1f81b 100644
--- a/src/core/internal.mli
+++ b/src/core/internal.mli
@@ -25,8 +25,7 @@ module Make
 
   val assume : ?tag:int -> St.formula list list -> unit
   (** Add the list of clauses to the current set of assumptions.
-      Modifies the sat solver state in place.
-      @raise Unsat if a conflict is detect when adding the clauses *)
+      Modifies the sat solver state in place. *)
 
   val push : unit -> unit
   (** Create a decision level for local assumptions.
@@ -36,7 +35,7 @@ module Make
   (** Pop a decision level for local assumptions. *)
 
   val local : St.formula list -> unit
-    (** Add local assumptions
+  (** Add local assumptions
       @param assumptions list of additional local assumptions to make,
         removed after the callback returns a value *)