From 66e2acc714f06b69c37aac4bc1c70a00b5eab34a Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Fri, 23 Aug 2024 11:32:10 -0500
Subject: [PATCH] Add logics from free constant types and constraints

---
 src/transSys.ml                         | 14 ++++++++++++++
 tests/regression/success/issue_1043.lus | 13 +++++++++++++
 2 files changed, 27 insertions(+)
 create mode 100644 tests/regression/success/issue_1043.lus

diff --git a/src/transSys.ml b/src/transSys.ml
index 21e3e2ada..ea476cd1a 100644
--- a/src/transSys.ml
+++ b/src/transSys.ml
@@ -1809,6 +1809,13 @@ let mk_trans_sys
              (* Logic of transition relation *)
                TermLib.logic_of_term fun_symbols trans ::
              
+             (* Logic of global constraints *)
+             List.map
+               (fun t -> TermLib.logic_of_term fun_symbols t)
+               global_constraints
+
+             @
+
              (* Logics of subsystems *)
              List.map
                (fun (t, _) -> match t.logic with
@@ -1831,6 +1838,13 @@ let mk_trans_sys
                 StateVar.type_of_state_var sv
                 |> TermLib.logic_of_sort
               ) state_vars)
+
+         (* Add logics from types of global constants *)
+         |> List.rev_append
+           (List.rev_map (fun v ->
+                Var.type_of_var v
+                |> TermLib.logic_of_sort
+              ) global_consts)
            
          (* Join logics to the logic required for this system *)
          |> TermLib.sup_logics)
diff --git a/tests/regression/success/issue_1043.lus b/tests/regression/success/issue_1043.lus
new file mode 100644
index 000000000..e7b673e2e
--- /dev/null
+++ b/tests/regression/success/issue_1043.lus
@@ -0,0 +1,13 @@
+type T = enum { A };
+
+const config_const_array: T ^ 1;
+
+node rising_edge(
+  i: bool;
+) returns (
+  b: bool;
+)
+let
+  b = i and (false -> pre (not i));
+  --%PROPERTY not b -> true;
+tel
\ No newline at end of file