From 8d9825b32d4a2b4b441b960efa33c406602a1fb7 Mon Sep 17 00:00:00 2001
From: Daniel Larraz <daniel-larraz@users.noreply.github.com>
Date: Thu, 21 Sep 2023 17:51:58 -0500
Subject: [PATCH] Fix node calls with same argument in constant and
 non-constant params

---
 src/lustre/lustreTransSys.ml                  | 20 +++++++++++++------
 src/transSys.ml                               |  6 +++---
 src/transSys.mli                              |  7 +++++--
 .../success/duplicate-const-arg.lus           | 11 ++++++++++
 4 files changed, 33 insertions(+), 11 deletions(-)
 create mode 100644 tests/regression/success/duplicate-const-arg.lus

diff --git a/src/lustre/lustreTransSys.ml b/src/lustre/lustreTransSys.ml
index 12307df40..4c94abb85 100644
--- a/src/lustre/lustreTransSys.ml
+++ b/src/lustre/lustreTransSys.ml
@@ -796,16 +796,24 @@ let call_terms_of_node_call mk_fresh_state_var globals
        call_locals)
   in
 
+  let non_constant_inputs =
+    (* Filter out inputs that are constants FOR THE CALLEE. *)
+    D.fold2
+      (fun formal_idx formal_sv actual_sv acc ->
+        if StateVar.is_const formal_sv then acc
+        else D.add formal_idx actual_sv acc
+      )
+      inputs
+      call_inputs
+      D.empty
+    |> D.values
+  in
+
   (* Return actual parameters of transition relation at bound in the
      correct order *)
   let trans_params_of_bound term_of_state_var pre_term_of_state_var =
     init_params_of_bound term_of_state_var @ (
-      ( (D.values call_inputs) @ D.values call_outputs @ call_locals )
-      |> List.filter (
-        (* Filter out svars that are constants FOR THE CALLEE. *)
-        fun sv ->
-          SVM.find sv state_var_map_down |> StateVar.is_const |> not
-      )
+      ( non_constant_inputs @ D.values call_outputs @ call_locals )
       |> List.map pre_term_of_state_var
     )
   in
diff --git a/src/transSys.ml b/src/transSys.ml
index 9614e0825..8f8cf4481 100644
--- a/src/transSys.ml
+++ b/src/transSys.ml
@@ -20,7 +20,7 @@ open Lib
 
 module P = Property
 module SVM = StateVar.StateVarMap
-module SVS = StateVar.StateVarSet
+(* module SVS = StateVar.StateVarSet *)
 
 (* Offset of state variables in initial state constraint *)
 let init_base = Numeral.zero
@@ -1201,7 +1201,7 @@ let flatten_instances subsystems =
     subsystems 
 *)
 
-
+(*
 let rec map_cex_prop_to_subsystem' 
     filter_out_values
     ({ scope; subsystems } as trans_sys) 
@@ -1288,7 +1288,7 @@ let rec map_cex_prop_to_subsystem'
 
 let map_cex_prop_to_subsystem filter_out_values trans_sys cex prop = 
   map_cex_prop_to_subsystem' filter_out_values trans_sys [] cex prop 
-
+*)
 
 (*
 
diff --git a/src/transSys.mli b/src/transSys.mli
index 7cfb4cc3c..455d17962 100644
--- a/src/transSys.mli
+++ b/src/transSys.mli
@@ -79,7 +79,10 @@ type instance =
 
     map_down : StateVar.t StateVar.StateVarMap.t;
     (** Map from the state variables of this system to the state
-        variables of the instance *)
+        variables of the instance. If the same variable is passed in
+        multiple arguments, the variable is only associated to
+        one of the formal parameters. Notice that for output and
+        local variables there is a one-to-one correspondence. *)
 
     map_up : StateVar.t StateVar.StateVarMap.t;
     (** Map from state variables of the called system to the state
@@ -365,7 +368,7 @@ val get_sofar_term: t -> Lib.position -> (Term.t * bool) option
 
 val get_max_depth : t -> int
 
-val map_cex_prop_to_subsystem : (Scope.t -> instance -> (StateVar.t * Model.value list) list ->  Model.value list -> Model.value list) -> t -> (StateVar.t * Model.value list) list -> Property.t -> t * instance list * (StateVar.t * Model.value list) list * Property.t 
+(*val map_cex_prop_to_subsystem : (Scope.t -> instance -> (StateVar.t * Model.value list) list ->  Model.value list -> Model.value list) -> t -> (StateVar.t * Model.value list) list -> Property.t -> t * instance list * (StateVar.t * Model.value list) list * Property.t *)
 
 (** {1 State Variables} *)
 
diff --git a/tests/regression/success/duplicate-const-arg.lus b/tests/regression/success/duplicate-const-arg.lus
new file mode 100644
index 000000000..b6d7291d9
--- /dev/null
+++ b/tests/regression/success/duplicate-const-arg.lus
@@ -0,0 +1,11 @@
+
+node M(const C:int; x:int) returns (y:int);
+let
+  y = x + C;
+tel
+
+node N(const C:int) returns (z:int);
+let
+   z = M(C, C);
+   --%PROPERTY z = 2*C;
+tel
\ No newline at end of file