From 439da034c14a2521f933bffaecd67db2040be902 Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Thu, 3 Oct 2024 18:55:56 -0500
Subject: [PATCH] Fixed incorrect variable renaming in bcccc88

This issue caused the step counter to not be introduced when
the history constructor was used in a contract.
---
 src/lustre/lustreAstNormalizer.ml     | 12 ++++++------
 tests/regression/success/history1.lus |  8 ++++++++
 2 files changed, 14 insertions(+), 6 deletions(-)
 create mode 100644 tests/regression/success/history1.lus

diff --git a/src/lustre/lustreAstNormalizer.ml b/src/lustre/lustreAstNormalizer.ml
index 62a345e60..ef2350cfa 100644
--- a/src/lustre/lustreAstNormalizer.ml
+++ b/src/lustre/lustreAstNormalizer.ml
@@ -1155,25 +1155,25 @@ and normalize_node info map
   in
   (* Normalize equations and the contract *)
   let nitems, gids8, warnings5 = normalize_list (normalize_item info node_id map) items in
-  let gids7' = union gids7 gids8 in
-  let gids8' =
+  let gids6_8 = union gids6 gids8 in
+  let gids9 =
     if exists_reachability_prop_with_bounds ||
-       not (StringMap.is_empty gids7'.history_vars) then (
+       not (StringMap.is_empty gids6_8.history_vars) then (
       add_step_counter info
     )
     else
       empty ()
   in
-  let gids9 =
+  let gids10 =
     StringMap.fold
       (fun id h_id acc ->
         union acc (add_history_var_and_equation info id h_id)
       )
-      gids7'.history_vars
+      gids6_8.history_vars
       (empty ())
   in
   let new_gids = union_list [union_list gids1; union_list gids2; union_list gids3; 
-                             gids4; gids5; gids6; gids7'; gids8'; gids9] in
+                             gids4; gids5; gids7; gids6_8; gids9; gids10] in
   let old_gids, warnings6 = normalize_gid_equations info map node_id in
   let map = StringMap.add node_id (union old_gids new_gids) map in
   (node_id, is_extern, params, inputs, outputs, locals, List.flatten nitems, ncontracts),
diff --git a/tests/regression/success/history1.lus b/tests/regression/success/history1.lus
new file mode 100644
index 000000000..f93d00629
--- /dev/null
+++ b/tests/regression/success/history1.lus
@@ -0,0 +1,8 @@
+
+node N(x: int) returns (y: int);
+(*@contract
+  guarantee "G1" exists (z: history(x)) y = z + 1;
+*)
+let
+  y = x + 1 -> if any bool then x + 1 else pre y;
+tel
\ No newline at end of file