Skip to content
Snippets Groups Projects
Commit 92102c11 authored by Christoph's avatar Christoph
Browse files

Don't assume Open means Sat when finished

Assumption doesn't hold true currently
parent 3f073372
No related branches found
No related tags found
No related merge requests found
......@@ -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
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Please register or to comment