diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml index 5f5653d7206175d117b335ac5f5043222d06dcd9..cf35e057c4bc20b382cfa7d2f9a1f35d11f25782 100644 --- a/src/lib/CoAlgReasoner.ml +++ b/src/lib/CoAlgReasoner.ml @@ -129,13 +129,19 @@ let propagateSatMu () = setAddState setSatStates state | Expandable | Open -> - setAddState setStates state; - if bsetCompare (stateGetDeferral state) emptySet == 0 + if stateGetStatus state == Open && List.length (stateGetRules state) == 0 then begin + setAddState setSatStates state; + stateSetStatus state Sat + end else begin + setAddState setStates state; + if bsetCompare (stateGetDeferral state) emptySet == 0 + then begin print_endline (stateToString state); setAddState setFinishingStates state end - else () + else () + end in let coreCollector core = match coreGetStatus core with