diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml index efb958d41148f8f3f082b61ec99758bb07358af4..b21350b9489b69323ae609a2c0c7230dcfb4514e 100644 --- a/src/lib/CoAlgReasoner.ml +++ b/src/lib/CoAlgReasoner.ml @@ -994,7 +994,7 @@ let expandNodesLoop (recursiveAction: unit -> unit) = expandState state; if doNominalPropagation () then begin propagateNominals (); - if doSatPropagation () then propagateSatMu () + if doSatPropagation () then propagateUnsatMu () end else () end else (); recursiveAction () @@ -1003,7 +1003,7 @@ let expandNodesLoop (recursiveAction: unit -> unit) = expandCore core; if doNominalPropagation () then begin propagateNominals (); - if doSatPropagation () then propagateSatMu () + if doSatPropagation () then propagateUnsatMu () end else () end else (); recursiveAction () @@ -1050,7 +1050,7 @@ let isRootSat () = | Expandable -> None | Unsat -> Some false | Sat -> Some true - | Open -> if (queueIsEmpty()) then Some false else None + | Open -> if (queueIsEmpty()) then Some true else None let reasonerFinished () = match coreGetStatus (graphGetRoot ()) with