diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml index b21350b9489b69323ae609a2c0c7230dcfb4514e..9534330cd981a9e2ef453bae1ee559b0022cb956 100644 --- a/src/lib/CoAlgReasoner.ml +++ b/src/lib/CoAlgReasoner.ml @@ -511,7 +511,7 @@ let propateUnsatMu () = let ruleiter (dependencies, corelist) : bool = List.for_all (fun (core : core) -> coreGetStatus core == Unsat || setMemCore setPrevUnsatCores core) corelist in - if not (List.exists ruleiter (stateGetRules state)) then begin + if not (List.exists ruleiter (stateGetRules state)) || stateGetStatus state == Expandable then begin visitParentCores state end @@ -520,7 +520,8 @@ let propateUnsatMu () = *) and checkFinishingCore (core : core) = if not (List.for_all (fun (state : state) -> stateGetStatus state == Unsat || setMemState setPrevUnsatStates state) - (coreGetChildren core)) + (coreGetChildren core)) || + coreGetStatus core == Expandable then begin visitParentStates core end