From e6f3e79acc3e44af4b2fd4daba7e22830fbc13ad Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Wed, 19 Oct 2016 17:07:19 +0200
Subject: [PATCH] [bugfix] Grow heap when adding local hyps

Previously, the heap was not grown when adding local assumptions. This
lead to a bug whne backtracking: indeed when a local assumption was
backtracked, it was added to the (too small) heap, which then raised a
Sparse_vec exception.
---
 src/core/internal.ml | 3 +++
 1 file changed, 3 insertions(+)

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);