From 92102c11a392982ae44d1d41b03b68f062826e92 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Sun, 10 Apr 2016 23:23:22 +0200
Subject: [PATCH] Don't assume Open means Sat when finished
Assumption doesn't hold true currently
---
src/lib/CoAlgReasoner.ml | 6 +++---
1 file changed, 3 insertions(+), 3 deletions(-)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index facbe45..46286bd 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
--
GitLab