diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 16bf0300..ca61e3f9 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -1988,13 +1988,19 @@ module Make(Plugin : PLUGIN)
     with E_sat -> ()
 
   let assume st cnf lemma =
-    List.iter
-      (fun l ->
-         let atoms = List.rev_map (mk_atom st) l in
-         let c = Clause.make_permanent atoms (Hyp lemma) in
-         Log.debugf debug (fun k -> k "(@[sat.assume-clause@ @[<hov 2>%a@]@])" Clause.debug c);
-         Vec.push st.clauses_to_add c)
-      cnf
+    try
+      List.iter
+        (fun l ->
+           let atoms = List.rev_map (mk_atom st) l in
+           let c = Clause.make_permanent atoms (Hyp lemma) in
+           Log.debugf debug (fun k -> k "(@[sat.assume-clause@ @[<hov 2>%a@]@])" Clause.debug c);
+           Vec.push st.clauses_to_add c)
+        cnf
+    with
+    | E_unsat (US_false c) ->
+      st.unsat_at_0 <- Some c
+    | E_unsat (US_local _) ->
+      assert false (* assumptions should only be present in [solve] *)
 
   (* Check satisfiability *)
   let check_clause c =