From a5eeaa0edc83cf1dfddb3b7391bdbd75d4186c2d Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Tue, 24 Jul 2018 21:57:12 +0200
Subject: [PATCH] Propagate consequences at the lowest level possible

---
 src/core/internal.ml | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/src/core/internal.ml b/src/core/internal.ml
index 2a5fe8b4..0409fb19 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -968,7 +968,8 @@ module Make
         else begin
           Iheap.grow_to_at_least env.order (St.nb_elt ());
           insert_subterms_order p.var;
-          enqueue_bool p (decision_level ()) (Bcp c)
+          let lvl = List.fold_left (fun acc a -> max acc a.var.v_level) 0 l in
+          enqueue_bool p lvl (Bcp c)
         end
       else
         raise (Invalid_argument "Msat.Internal.slice_propagate")