From 653eaa4be84a10b0dbf335b213739311bf6811f8 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 16 Feb 2016 14:32:08 +0100
Subject: [PATCH] Update deferral when revisiting formula
---
src/lib/CoAlgMisc.ml | 3 ++-
1 file changed, 2 insertions(+), 1 deletion(-)
diff --git a/src/lib/CoAlgMisc.ml b/src/lib/CoAlgMisc.ml
index 9718617..c465ec0 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -863,7 +863,8 @@ let rec detClosure vars nomTbl hcF fset vset atset nomset s f =
let sstr = string_of_int s in
raise (C.CoAlgException ("Invalid sort (i.e. sort out of range): " ^ sstr))
else ();
- if C.HcFHt.mem fset.(s) f then ()
+ if C.HcFHt.mem vset.(s) f &&
+ compare (C.HcFHt.find vset.(s) f) deferral = 0 then ()
else
let () = C.HcFHt.add vset.(s) f deferral in
let () = C.HcFHt.add fset.(s) f () in
--
GitLab