diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 36d9c24d..82c1b036 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -1493,6 +1493,7 @@ module Make(Plugin : PLUGIN)
           enqueue_bool st fuip ~level:cr.cr_backtrack_lvl (Bcp lclause)
         ) else (
           assert Plugin.mcsat;
+          assert (st.next_decisions = []);
           st.next_decisions <- [fuip.neg];
         )
     end;
@@ -1929,7 +1930,6 @@ module Make(Plugin : PLUGIN)
   and pick_branch_lit st =
     match st.next_decisions with
     | atom :: tl ->
-      assert Plugin.mcsat;
       st.next_decisions <- tl;
       pick_branch_aux st atom
     | [] when decision_level st < Vec.size st.assumptions ->
diff --git a/src/core/Solver_intf.ml b/src/core/Solver_intf.ml
index cbf909c0..5f1b7d44 100644
--- a/src/core/Solver_intf.ml
+++ b/src/core/Solver_intf.ml
@@ -134,7 +134,7 @@ type ('term, 'formula, 'value, 'proof) acts = {
 
   acts_add_decision_lit: 'formula -> unit;
   (** Ask the SAT solver to decide on the given formula before it can
-      answer [SAT]. This will be removed on backtrack.
+      answer [SAT]. The order of decisions is still unspecified.
       Useful for theory combination. *)
 }
 (** The type for a slice of assertions to assume/propagate in the theory. *)