From f80c3b3df794691a4a6a33db2189ddca3cbb9c90 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Mon, 19 Dec 2016 15:58:48 +0100
Subject: [PATCH] [bugfix] Allow semantic propagation of already true lits

---
 src/core/internal.ml | 13 ++++++++-----
 1 file changed, 8 insertions(+), 5 deletions(-)

diff --git a/src/core/internal.ml b/src/core/internal.ml
index 932f236e..e37132dc 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -499,11 +499,14 @@ module Make
       (fun k->k (Vec.size env.elt_queue) pp_atom a)
 
   let enqueue_semantic a terms =
-    let l = List.map St.add_term terms in
-    let lvl = List.fold_left (fun acc {l_level; _} ->
-        assert (l_level > 0); max acc l_level) 0 l in
-    Iheap.grow_to_at_least env.order (St.nb_elt ());
-    enqueue_bool a lvl Semantic
+    if a.is_true then ()
+    else begin
+      let l = List.map St.add_term terms in
+      let lvl = List.fold_left (fun acc {l_level; _} ->
+          assert (l_level > 0); max acc l_level) 0 l in
+      Iheap.grow_to_at_least env.order (St.nb_elt ());
+      enqueue_bool a lvl Semantic
+    end
 
   (* MCsat semantic assignment *)
   let enqueue_assign l value lvl =