diff --git a/src/loop/parser.ml b/src/loop/parser.ml
index ad2445ea6..af5a86e90 100644
--- a/src/loop/parser.ml
+++ b/src/loop/parser.ml
@@ -376,9 +376,13 @@ module Make(State : State.S) = struct
 
   let expand st c =
     let ret = match c with
-      | { S.descr = S.Pack l; _ } ->
+      | { S.descr = S.Pack l; attrs; _ } ->
         let file = State.get State.logic_file st in
-        st, `Gen (merge, wrap_parser ~file (Gen.of_list l))
+        let g =
+          Gen.of_list l
+          |> Gen.map (S.add_attrs attrs)
+        in
+        st, `Gen (merge, wrap_parser ~file g)
       (* TODO: filter the statements by passing some options *)
       | { S.descr = S.Include file; _ } ->
         let logic_file = State.get State.logic_file st in
diff --git a/src/loop/typer.ml b/src/loop/typer.ml
index 2a6753544..8a2a73eb5 100644
--- a/src/loop/typer.ml
+++ b/src/loop/typer.ml
@@ -1841,6 +1841,7 @@ module Make
     id : Dolmen.Std.Id.t;
     loc : Dolmen.Std.Loc.t;
     contents  : 'a;
+    attrs : Dolmen.Std.Term.t list;
   }
 
   type def = [
@@ -1908,7 +1909,8 @@ module Make
 
   (* Simple constructor *)
   (* let tr implicit contents = { implicit; contents; } *)
-  let simple id loc (contents: typechecked)  = { id; loc; contents; }
+  let simple id loc attrs (contents: typechecked) =
+    { id; loc; attrs; contents; }
 
   let print_def fmt = function
     | `Type_alias (id, c, vars, body) ->
@@ -2009,10 +2011,17 @@ module Make
     | `Exit ->
       Format.fprintf fmt "@[<hov 2>exit@]"
 
-  let print fmt ({ id; loc; contents; } : typechecked stmt) =
-    Format.fprintf fmt "@[<v 2>%a[%a]:@,%a@]"
+  let print_attr fmt t =
+    Format.fprintf fmt "{%a}@," Dolmen.Std.Term.print t
+
+  let print_attrs fmt attrs =
+    List.iter (print_attr fmt) attrs
+
+  let print fmt ({ id; loc; attrs; contents; } : typechecked stmt) =
+    Format.fprintf fmt "@[<v 2>%a[%a]:@,%a%a@]"
       Dolmen.Std.Id.print id
       Dolmen.Std.Loc.print_compact loc
+      print_attrs attrs
       print_typechecked contents
 
   (* Typechecking *)
@@ -2074,93 +2083,93 @@ module Make
     let input = `Logic (State.get State.logic_file st) in
     match normalize st c with
     (* State&Assertion stack management *)
-    | { S.descr = S.Reset; _ } ->
-      let st = Typer.reset st ~loc:c.S.loc () in
-      st, simple (other_id c) c.S.loc `Reset
-    | { S.descr = S.Pop i; _ } ->
-      let st = Typer.pop st ~input ~loc:c.S.loc i in
-      st, (simple (other_id c) c.S.loc (`Pop i))
-    | { S.descr = S.Push i; _ } ->
-      let st = Typer.push st ~input ~loc:c.S.loc i in
-      st, (simple (other_id c) c.S.loc (`Push i))
-    | { S.descr = S.Reset_assertions; _ } ->
-      let st = Typer.reset_assertions st ~loc:c.S.loc () in
-      st, (simple (other_id c) c.S.loc `Reset_assertions)
+    | { S.descr = S.Reset; loc; attrs; _ } ->
+      let st = Typer.reset st ~loc () in
+      st, simple (other_id c) loc attrs `Reset
+    | { S.descr = S.Pop i; loc; attrs; _ } ->
+      let st = Typer.pop st ~input ~loc i in
+      st, (simple (other_id c) loc attrs (`Pop i))
+    | { S.descr = S.Push i; loc; attrs; _ } ->
+      let st = Typer.push st ~input ~loc i in
+      st, (simple (other_id c) loc attrs (`Push i))
+    | { S.descr = S.Reset_assertions; loc; attrs; _ } ->
+      let st = Typer.reset_assertions st ~loc () in
+      st, (simple (other_id c) loc attrs `Reset_assertions)
 
     (* Plain statements
        TODO: allow the `plain` function to return a meaningful value *)
-    | { S.descr = S.Plain t; _ } ->
-      st, (simple (other_id c) c.S.loc (`Plain t))
+    | { S.descr = S.Plain t; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs (`Plain t))
 
     (* Hypotheses and goal statements *)
-    | { S.descr = S.Prove { hyps; goals }; _ } ->
-      let st, hyps = Typer.formulas st ~input ~loc:c.S.loc ~attrs:c.S.attrs hyps in
-      let st, goals = Typer.formulas st ~input ~loc:c.S.loc ~attrs:c.S.attrs goals in
-      st, (simple (prove_id c) c.S.loc (`Solve (hyps, goals)))
+    | { S.descr = S.Prove { hyps; goals }; loc; attrs; _ } ->
+      let st, hyps = Typer.formulas st ~input ~loc ~attrs hyps in
+      let st, goals = Typer.formulas st ~input ~loc ~attrs goals in
+      st, (simple (prove_id c) loc attrs(`Solve (hyps, goals)))
 
     (* Hypotheses & Goals *)
-    | { S.descr = S.Clause l; _ } ->
-      let st, res = Typer.formulas st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in
-      let stmt : typechecked stmt = simple (hyp_id c) c.S.loc (`Clause res) in
+    | { S.descr = S.Clause l; loc; attrs; _ } ->
+      let st, res = Typer.formulas st ~input ~loc ~attrs l in
+      let stmt : typechecked stmt = simple (hyp_id c) loc attrs (`Clause res) in
       st, stmt
-    | { S.descr = S.Antecedent t; _ } ->
-      let st, ret = Typer.formula st ~input ~loc:c.S.loc ~attrs:c.S.attrs ~goal:false t in
-      let stmt : typechecked stmt = simple (hyp_id c) c.S.loc (`Hyp ret) in
+    | { S.descr = S.Antecedent t; loc; attrs; _ } ->
+      let st, ret = Typer.formula st ~input ~loc ~attrs ~goal:false t in
+      let stmt : typechecked stmt = simple (hyp_id c) loc attrs (`Hyp ret) in
       st, stmt
-    | { S.descr = S.Consequent t; _ } ->
-      let st, ret = Typer.formula st ~input ~loc:c.S.loc ~attrs:c.S.attrs ~goal:true t in
-      let stmt : typechecked stmt = simple (goal_id c) c.S.loc (`Goal ret) in
+    | { S.descr = S.Consequent t; loc; attrs; _ } ->
+      let st, ret = Typer.formula st ~input ~loc ~attrs ~goal:true t in
+      let stmt : typechecked stmt = simple (goal_id c) loc attrs (`Goal ret) in
       st, stmt
 
     (* Other set_logics should check whether corresponding plugins are activated ? *)
-    | { S.descr = S.Set_logic s; _ } ->
-      let st, new_logic = Typer.set_logic st ~input ~loc:c.S.loc s in
-      st, (simple (other_id c) c.S.loc (`Set_logic (s, new_logic)))
+    | { S.descr = S.Set_logic s; loc; attrs; _ } ->
+      let st, new_logic = Typer.set_logic st ~input ~loc s in
+      st, (simple (other_id c) loc attrs (`Set_logic (s, new_logic)))
 
     (* Set/Get info *)
-    | { S.descr = S.Get_info s; _ } ->
-      st, (simple (other_id c) c.S.loc (`Get_info s))
-    | { S.descr = S.Set_info t; _ } ->
-      st, (simple (other_id c) c.S.loc (`Set_info t))
+    | { S.descr = S.Get_info s; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs (`Get_info s))
+    | { S.descr = S.Set_info t; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs (`Set_info t))
 
     (* Set/Get options *)
-    | { S.descr = S.Get_option s; _ } ->
-      st, (simple (other_id c) c.S.loc (`Get_option s))
-    | { S.descr = S.Set_option t; _ } ->
-      st, (simple (other_id c) c.S.loc (`Set_option t))
+    | { S.descr = S.Get_option s; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs (`Get_option s))
+    | { S.descr = S.Set_option t; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs (`Set_option t))
 
     (* Declarations and definitions *)
-    | { S.descr = S.Defs d; _ } ->
-      let st, l = Typer.defs ~mode:`Create_id st ~input ~loc:c.S.loc ~attrs:c.S.attrs d in
-      let res : typechecked stmt = simple (def_id c) c.S.loc (`Defs l) in
+    | { S.descr = S.Defs d; loc; attrs; _ } ->
+      let st, l = Typer.defs ~mode:`Create_id st ~input ~loc ~attrs d in
+      let res : typechecked stmt = simple (def_id c) loc attrs (`Defs l) in
       st, (res)
-    | { S.descr = S.Decls l; _ } ->
-      let st, l = Typer.decls st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in
-      let res : typechecked stmt = simple (decl_id c) c.S.loc (`Decls l) in
+    | { S.descr = S.Decls l; loc; attrs; _ } ->
+      let st, l = Typer.decls st ~input ~loc ~attrs l in
+      let res : typechecked stmt = simple (decl_id c) loc attrs (`Decls l) in
       st, (res)
 
     (* Smtlib's proof/model instructions *)
-    | { S.descr = S.Get_proof; _ } ->
-      st, (simple (other_id c) c.S.loc `Get_proof)
-    | { S.descr = S.Get_unsat_core; _ } ->
-      st, (simple (other_id c) c.S.loc `Get_unsat_core)
-    | { S.descr = S.Get_unsat_assumptions; _ } ->
-      st, (simple (other_id c) c.S.loc `Get_unsat_assumptions)
-    | { S.descr = S.Get_model; _ } ->
-      st, (simple (other_id c) c.S.loc `Get_model)
-    | { S.descr = S.Get_value l; _ } ->
-      let st, l = Typer.terms st ~input ~loc:c.S.loc ~attrs:c.S.attrs l in
-      st, (simple (other_id c) c.S.loc (`Get_value l))
-    | { S.descr = S.Get_assignment; _ } ->
-      st, (simple (other_id c) c.S.loc `Get_assignment)
+    | { S.descr = S.Get_proof; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs `Get_proof)
+    | { S.descr = S.Get_unsat_core; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs `Get_unsat_core)
+    | { S.descr = S.Get_unsat_assumptions; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs `Get_unsat_assumptions)
+    | { S.descr = S.Get_model; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs `Get_model)
+    | { S.descr = S.Get_value l; loc; attrs; _ } ->
+      let st, l = Typer.terms st ~input ~loc ~attrs l in
+      st, (simple (other_id c) loc attrs (`Get_value l))
+    | { S.descr = S.Get_assignment; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs `Get_assignment)
     (* Assertions *)
-    | { S.descr = S.Get_assertions; _ } ->
-      st, (simple (other_id c) c.S.loc `Get_assertions)
+    | { S.descr = S.Get_assertions; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs `Get_assertions)
     (* Misc *)
-    | { S.descr = S.Echo s; _ } ->
-      st, (simple (other_id c) c.S.loc (`Echo s))
-    | { S.descr = S.Exit; _ } ->
-      st, (simple (other_id c) c.S.loc `Exit)
+    | { S.descr = S.Echo s; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs (`Echo s))
+    | { S.descr = S.Exit; loc; attrs; _ } ->
+      st, (simple (other_id c) loc attrs `Exit)
 
     (* packs and includes *)
     | { S.descr = S.Include _; _ } -> assert false
diff --git a/src/loop/typer_intf.ml b/src/loop/typer_intf.ml
index ba093b46d..a88886436 100644
--- a/src/loop/typer_intf.ml
+++ b/src/loop/typer_intf.ml
@@ -186,6 +186,7 @@ module type S = sig
     id          : Dolmen.Std.Id.t;
     loc         : Dolmen.Std.Loc.t;
     contents    : 'a;
+    attrs       : Dolmen.Std.Term.t list;
   }
   (** Wrapper around statements. It records implicit type declarations. *)
 
diff --git a/src/standard/statement.ml b/src/standard/statement.ml
index 0a166ed99..943ad0974 100644
--- a/src/standard/statement.ml
+++ b/src/standard/statement.ml
@@ -329,6 +329,9 @@ let annot = Term.apply
 let mk ?id ?(loc=Loc.no_loc) ?(attrs=[]) descr =
   { id; descr; loc; attrs; }
 
+let add_attrs attrs t =
+  { t with attrs = attrs @ t.attrs; }
+
 (* Pack *)
 let pack ?id ?loc ?attrs l =
   mk ?id ?loc ?attrs (Pack l)
diff --git a/src/standard/statement.mli b/src/standard/statement.mli
index ae3fc0eca..fc567ecb2 100644
--- a/src/standard/statement.mli
+++ b/src/standard/statement.mli
@@ -171,6 +171,9 @@ include Dolmen_intf.Stmt.Logic
 
 (** {2 Additional functions} *)
 
+val add_attrs : term list -> t -> t
+(** Add some attributes to a statement. *)
+
 val mk_decls :
   ?loc:location -> ?attrs:term list -> recursive:bool -> decl list -> t
 (** Create a group of declarations *)