[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.
This commit is contained in:
Guillaume Bury 2016-10-19 17:07:19 +02:00
parent 9baa3f0716
commit e6f3e79acc

View file

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