diff --git a/examples/tests/cvc4-models.mlw b/examples/tests/cvc4-models.mlw
index 5af47dd151353a1fb9ba3ed472cb0642d2e588ef..368cd86077541846e66163083d420364a87030ba 100644
--- a/examples/tests/cvc4-models.mlw
+++ b/examples/tests/cvc4-models.mlw
@@ -53,7 +53,7 @@ module M
 
   (*** In all cases, records are decomposed using match eval ***)
 
-  type r = {f "field_f" :int; g:bool}
+  type r = {f "model_trace:field_f" :int; g:bool}
 
   (* Projection functions *)
   function projf_r_f "model_trace:.f" (x : r) : int
diff --git a/src/core/ident.ml b/src/core/ident.ml
index f44da4a438994175b97285e9b22af19d058259a4..910f56dc38814ce9428925f47e8c861400a1bee0 100644
--- a/src/core/ident.ml
+++ b/src/core/ident.ml
@@ -52,12 +52,12 @@ let is_model_trace_label label =
     true
   with Not_found -> false
 
-let get_model_trace_label labels =
+let get_model_trace_label ~labels =
   Slab.choose (Slab.filter is_model_trace_label labels)
 
 let transform_model_trace_label labels trans_fun =
   try
-    let trace_label = get_model_trace_label labels in
+    let trace_label = get_model_trace_label ~labels in
     let labels_without_trace = Slab.remove trace_label labels in
     let new_trace_label = create_label (trans_fun trace_label.lab_string) in
     Slab.add new_trace_label labels_without_trace
@@ -76,7 +76,7 @@ let append_to_model_trace_label ~labels ~to_append =
     transform_model_trace_label labels trans
 
 let get_model_element_name ~labels =
-  let trace_label = get_model_trace_label labels in
+  let trace_label = get_model_trace_label ~labels in
   let splitted1 = Str.bounded_split (Str.regexp_string ":") trace_label.lab_string 2 in
   match splitted1 with
   | [_; content] ->
@@ -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
diff --git a/src/core/ident.mli b/src/core/ident.mli
index b6be705386eda705d8b1afbe00841ae74ddf65ab..e848eaa8ec9d3d1f9bf5ca5ac49285b9122c6e29 100644
--- a/src/core/ident.mli
+++ b/src/core/ident.mli
@@ -49,6 +49,10 @@ val get_model_element_name : labels : Slab.t -> string
     Throws Not_found if there is no element name (there is no
     label of the form "model_trace:+". *)
 
+val get_model_trace_label : labels : Slab.t -> Slab.elt
+(** Return label of the for "model_trace:*".
+    Throws Not_found if there is no such label.*)
+
 (** {2 Identifiers} *)
 
 type ident = private {
@@ -83,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
 
diff --git a/src/core/model_parser.ml b/src/core/model_parser.ml
index bef63d8ca1c3c44959af665da6b7e956565fa1da..98907379319700226de9a2c0a3949e67e9063881 100644
--- a/src/core/model_parser.ml
+++ b/src/core/model_parser.ml
@@ -69,10 +69,10 @@ let rec print_indices fmt indices =
     print_indices fmt tail
 and
 print_array fmt arr =
-  fprintf fmt "[others -> ";
+  fprintf fmt "(others => ";
   print_model_value fmt arr.arr_others;
   print_indices fmt arr.arr_indices;
-  fprintf fmt "]"
+  fprintf fmt ")"
 and
 print_model_value_sanit sanit_print fmt value =
   (* Prints model value. *)
diff --git a/src/core/pretty.ml b/src/core/pretty.ml
index 3201bf70461eacca4952c045de7daa6dbdb4b0ae..369fa0b13ed286209f111ccff6a0772d36c2a502 100644
--- a/src/core/pretty.ml
+++ b/src/core/pretty.ml
@@ -603,4 +603,3 @@ let () = Exn_printer.register
       fprintf fmt "Cannot prove the termination of %a" print_ls ls
   | _ -> raise exn
   end
-
diff --git a/src/core/pretty.mli b/src/core/pretty.mli
index 04adff381f9eee5dbb6e818dd5e2c489cd181c79..ff17992235d693a4c1c235f9da44409d7e3e1640 100644
--- a/src/core/pretty.mli
+++ b/src/core/pretty.mli
@@ -64,4 +64,3 @@ val print_task : formatter -> task -> unit
 val print_theory : formatter -> theory -> unit
 
 val print_namespace : formatter -> string -> theory -> unit
-
diff --git a/src/transform/eval_match.ml b/src/transform/eval_match.ml
index 2fd97c3675a02ded3d2cbc42c9c38d25e7282dc0..c289cb0eacd724ed749af8d5a3527c5dd74ab694 100644
--- a/src/transform/eval_match.ml
+++ b/src/transform/eval_match.ml
@@ -61,10 +61,25 @@ let rec add_quant kn (vl,tl,f) v =
     | _ -> []
   in
   match cl with
-    | [ls,_] ->
+    | [ls,pjl] ->
+	(* there is only one constructor *)
         let s = ty_match Mtv.empty (Opt.get ls.ls_value) ty in
-        let mk_v ty = create_vsymbol (id_clone v.vs_name) (ty_inst s ty) in
-        let nvl = List.map mk_v ls.ls_args in
+        let mk_v ty pj =
+	  (* The name of the field corresponding to the variable that is created  *)
+	  let field_name = begin match pj with
+	    | Some pj_ls ->
+	      begin
+		try
+		  Ident.get_model_element_name ~labels:pj_ls.ls_name.id_label
+		with Not_found -> pj_ls.ls_name.id_string
+	      end
+	    | _ -> ""
+	  end in
+	  let label = Ident.append_to_model_element_name
+	    ~labels:v.vs_name.id_label ~to_append:("." ^ field_name) 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
         let f = t_let_close_simp v t f in
         let tl = tr_map (t_subst_single v t) tl in
@@ -114,7 +129,7 @@ let eval_match ~inline kn t =
   let rec eval stop env t =
     let stop = stop || Slab.mem Split_goal.stop_split t.t_label in
     let eval = eval stop in
-    t_label_copy t (match t.t_node with
+    let t_eval_matched = (match t.t_node with
     | Tapp (ls, [t1;t2]) when ls_equal ls ps_equ ->
         cs_equ kn env (eval env t1) (eval env t2)
     | Tapp (ls, [t1]) when is_projection kn ls ->
@@ -142,7 +157,18 @@ let eval_match ~inline kn t =
           else List.fold_left (add_quant kn) ([],tl,f) vl in
         t_quant_simp q (close (List.rev vl) tl (eval env f))
     | _ ->
-        t_map_simp (eval env) t)
+        t_map_simp (eval env) t) in
+
+    (* Copy all labels of t to t_eval_matched except for "model_trace:*" label.
+       This label is not copied if both t and t_eval_matched contain it. *)
+    let t =
+      (try
+	 let _ = Ident.get_model_trace_label ~labels:t_eval_matched.t_label in
+	 let original_mt_label = Ident.get_model_trace_label ~labels:t.t_label in
+	 (* If both t_eval_matched and t contain model_trace label, remove it *)
+	 t_label_remove original_mt_label t
+       with Not_found -> t) in
+    t_label_copy t t_eval_matched
   in
   eval false Mvs.empty t