From 2286a72437de8f59426bb802c0da1194a1212cfd Mon Sep 17 00:00:00 2001
From: Simon Cruanes <simon.cruanes.2007@m4x.org>
Date: Tue, 29 Oct 2019 14:34:13 -0500
Subject: [PATCH] fix: in final-check, resume if there are new decisions to do

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

diff --git a/src/core/Internal.ml b/src/core/Internal.ml
index 6f71d5e3..749626d2 100644
--- a/src/core/Internal.ml
+++ b/src/core/Internal.ml
@@ -2041,7 +2041,9 @@ module Make(Plugin : PLUGIN)
             begin match Plugin.final_check st.th (full_slice st) with
               | () ->
                 if st.elt_head = Vec.size st.trail &&
-                   Vec.is_empty st.clauses_to_add then (
+                   Vec.is_empty st.clauses_to_add &&
+                   st.next_decisions = []
+                then (
                   raise_notrace E_sat
                 );
                 (* otherwise, keep on *)