diff --git a/src/core/internal.ml b/src/core/internal.ml
index 87084022..0f16f57b 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -1172,6 +1172,9 @@ module Make
           (* conflict between assumptions: UNSAT *)
           report_unsat c;
         end else begin
+          (* Grow the heap, because when the lit is backtracked,
+             it will be added to the heap. *)
+          Iheap.grow_to_by_double env.order (St.nb_elt ());
           (* make a decision, propagate *)
           let level = decision_level() in
           enqueue_bool a ~level (Bcp c);