Bugfix: instead of replacing original labels with new labels, new labels

were added to original labels.

src/core/ident.ml

@@ -140,6 +140,9 @@ let id_fresh ?(label = Slab.empty) ?loc nm =
 let id_user ?(label = Slab.empty) nm loc =
   create_ident nm label (Some loc)
 
+let id_lab label id =
+  create_ident id.id_string label id.id_loc
+
 let id_clone ?(label = Slab.empty) id =
   let ll = Slab.union label id.id_label in
   create_ident id.id_string ll id.id_loc

src/core/ident.mli

@@ -87,6 +87,9 @@ val id_fresh : ?label:Slab.t -> ?loc:Loc.position -> string -> preid
 (* create a localized pre-ident *)
 val id_user : ?label:Slab.t -> string -> Loc.position -> preid
 
+(* create a duplicate pre-ident with given labels *)
+val id_lab : Slab.t -> ident -> preid
+
 (* create a duplicate pre-ident *)
 val id_clone : ?label:Slab.t -> ident -> preid
 

src/transform/eval_match.ml

@@ -77,7 +77,7 @@ let rec add_quant kn (vl,tl,f) v =
 	  end in
 	  let label = Ident.append_to_model_element_name
 	    ~labels:v.vs_name.id_label ~to_append:("." ^ field_name) in
-	  create_vsymbol (id_clone ~label v.vs_name) (ty_inst s ty) in
+	  create_vsymbol (id_lab label v.vs_name) (ty_inst s ty) in
 
         let nvl = List.map2 mk_v ls.ls_args pjl in
         let t = fs_app ls (List.map t_var nvl) ty in