From 43194ed2e6c40e8384f3622adf2fd6f14623ef93 Mon Sep 17 00:00:00 2001
From: Christoph Egger <Christoph.Egger@fau.de>
Date: Tue, 1 Dec 2015 17:07:56 +0100
Subject: [PATCH] Add Closure for plain Variables
As there should never be free variables in formulas within the
FL-Closure maybe we should rather signal an error here?
---
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 6b1e98e..8c062fe 100644
--- a/src/lib/CoAlgMisc.ml
+++ b/src/lib/CoAlgMisc.ml
@@ -792,7 +792,8 @@ let rec detClosure nomTbl hcF fset atset nomset s f =
let (func, sortlst) = !sortTable.(s) in
match f.HC.node with
| C.HCTRUE
- | C.HCFALSE -> ()
+ | C.HCFALSE
+ | C.HCVAR _ -> ()
| C.HCAP name ->
if C.isNominal name then begin
Hashtbl.replace nomset name s;
--
GitLab