diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml index facbe456e79da3a73da02dbf47c5c56c685bd562..46286bd09714b446d2f0dd4cac74b94839379d54 100644 --- a/src/lib/CoAlgReasoner.ml +++ b/src/lib/CoAlgReasoner.ml @@ -244,7 +244,7 @@ let propagateSatMu () = (setLengthCore setCores) = (setLengthCore allowedCores) then begin setIterState (fun state -> stateSetStatus state Sat) setStates; - setIterCore (fun core -> coreSetStatus core Sat) setCores; + setIterCore (fun core -> coreSetStatus core Sat; if core == graphGetRoot () then raise (CoAlg_finished true) else ()) setCores; end else fixpointstep allowedStates allowedCores in @@ -908,8 +908,8 @@ let isRootSat () = match coreGetStatus (graphGetRoot ()) with | Expandable -> None | Unsat -> Some false - | Sat - | Open -> if (queueIsEmpty()) then Some true else None + | Sat -> if (queueIsEmpty()) then Some true else None + | Open -> if (queueIsEmpty()) then Some false else None let reasonerFinished () = match coreGetStatus (graphGetRoot ()) with