From 7e95911dd8d44b01b0ea4bdab6e77573cc6c6798 Mon Sep 17 00:00:00 2001
From: Guillaume Bury <guillaume.bury@gmail.com>
Date: Fri, 7 Apr 2017 15:13:27 +0200
Subject: [PATCH] [bugfix] Allow late mcsat conflicts (wrt assigns)

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

diff --git a/src/core/internal.ml b/src/core/internal.ml
index 0ffde72c..1129fed9 100644
--- a/src/core/internal.ml
+++ b/src/core/internal.ml
@@ -657,9 +657,11 @@ module Make
 
       (* look for the next node to expand *)
       while
-        let q = get_atom !tr_ind in
-        (not (q.var.seen = Both)) ||
-        (q.var.v_level < conflict_level)
+        match Vec.get env.elt_queue !tr_ind with
+        | Atom q ->
+          (not (q.var.seen = Both)) ||
+          (q.var.v_level < conflict_level)
+        | Lit _ -> true
       do
         decr tr_ind;
       done;