diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml index cae46fbfefca2c63cda9314d0fed84e72628d9d0..4049c1cab50738f1f53ae05ce545381e578973bc 100644 --- a/src/lib/CoAlgReasoner.ml +++ b/src/lib/CoAlgReasoner.ml @@ -1114,14 +1114,22 @@ let rec insertAllRules state rules = List.mem true (List.map (fun (dep, children) -> insertRule state dep children) rules) let expandState state = + let setSatOrOpen () = + if CU.TList.empty (stateGetRules state) then + stateSetStatus state Sat + else + stateSetStatus state Open + in + match stateNextRule state with | MultipleElements rules -> let unsat = insertAllRules state rules in - if not unsat then stateSetStatus state Open + if not unsat then setSatOrOpen () | SingleElement (dep, chldrn) -> let unsat = insertRule state dep chldrn in if not unsat then queueInsertState state else () - | NoMoreElements -> stateSetStatus state Open + | NoMoreElements -> + setSatOrOpen () let expandCnstr cset =