From e4faff970cd3e6090d373cc84e179c7c2164e2ed Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Wed, 13 Apr 2016 23:43:58 +0200
Subject: [PATCH] Do a final propagation round at the end
---
src/lib/CoAlgReasoner.ml | 1 +
1 file changed, 1 insertion(+)
diff --git a/src/lib/CoAlgReasoner.ml b/src/lib/CoAlgReasoner.ml
index 690814e..f24844e 100644
--- a/src/lib/CoAlgReasoner.ml
+++ b/src/lib/CoAlgReasoner.ml
@@ -1080,6 +1080,7 @@ let isSat ?(verbose = false) sorts nomTable tbox sf =
let sat =
try
buildGraphLoop ();
+ propagateUnsatMu ();
(* get whether the root is satisfiable *)
(* we know that the reasoner finished, so the value is there, *)
(* i.e. isRootSat() will give a "Some x" and not "None" *)
--
GitLab