From 01d0668fc6ed861564d471c3b6b0ba063e48e899 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 27 Aug 2022 23:08:58 -0400 Subject: [PATCH] fix(sat): check for new atoms in termination check in final_check --- src/sat/solver.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/solver.ml b/src/sat/solver.ml index c751536e..5fc1110b 100644 --- a/src/sat/solver.ml +++ b/src/sat/solver.ml @@ -1734,7 +1734,7 @@ let solve_ ~on_progress (self : t) : unit = if self.elt_head = AVec.size self.trail && has_no_delayed_actions self - && self.next_decisions = [] + && self.next_decisions = [] && H.is_empty self.order then (* nothing more to do, that means the plugin is satisfied with the trail *)