Treat Sat states like finishing states

With Sat states only treated like other states in the second fixpoint
iteration, the outer fixpoint was not ncessarily monononously decreasing
causing wrong results when in the first round the same number of nodes
got removed as added due to sat states.

src/lib/CoAlgReasoner.ml

@@ -118,20 +118,18 @@ let propagateSatMu () =
   let setFinishingCores = setEmptyCore () in
   let setStates = setEmptyState () in
   let setCores = setEmptyCore () in
-  let setSatStates = setEmptyState () in
-  let setSatCores = setEmptyCore () in
   let emptySet = bsetMakeRealEmpty () in
 
   let stateCollector state =
     match stateGetStatus state with
     | Unsat -> ()
     | Sat ->
-       setAddState setSatStates state
+       setAddState setFinishingStates state
     | Expandable -> ()
     | Open ->
        if stateGetStatus state == Open && List.length (stateGetRules state) == 0 || bsetCompare (bsetMake ()) (stateGetBs state) == 0
        then begin
-         setAddState setSatStates state;
+         setAddState setFinishingStates state;
          stateSetStatus state Sat
        end else begin
          setAddState setStates state;
@@ -147,7 +145,7 @@ let propagateSatMu () =
     match coreGetStatus core with
     | Unsat -> ()
     | Sat ->
-       setAddCore setSatCores core
+       setAddCore setFinishingCores core
     | Expandable
     | Open ->
        setAddCore setCores core;
@@ -240,8 +238,6 @@ let propagateSatMu () =
     in
     setIterState checkFinishingState setFinishingStates;
     setIterCore checkFinishingCore setFinishingCores;
-    setIterState visitParentCores setSatStates;
-    setIterCore visitParentStates setSatCores;
 
 
     if (setLengthState setStates) = (setLengthState allowedStates) &&