diff --git a/src/kernel_services/ast_queries/acsl_extension.ml b/src/kernel_services/ast_queries/acsl_extension.ml
index 8de542adc8dd8897a440576ef8e7aed045b89afc..5b75815f9c2bc165e44e407e5c74764a7b86222e 100644
--- a/src/kernel_services/ast_queries/acsl_extension.ml
+++ b/src/kernel_services/ast_queries/acsl_extension.ml
@@ -37,6 +37,24 @@ type extension_visitor =
 type extension_printer =
   Printer_api.extensible_printer_type -> Format.formatter ->
   acsl_extension_kind -> unit
+type extension_same =
+  acsl_extension_kind -> acsl_extension_kind -> Ast_diff.is_same_env -> bool
+
+type register_extension =
+  plugin:string -> string ->
+  ?preprocessor:extension_preprocessor -> extension_typer ->
+  ?visitor:extension_visitor ->
+  ?printer:extension_printer -> ?short_printer:extension_printer ->
+  ?is_same_ext:extension_same -> bool ->
+  unit
+
+type register_extension_block =
+  plugin: string -> string ->
+  ?preprocessor:extension_preprocessor_block -> extension_typer_block ->
+  ?visitor:extension_visitor ->
+  ?printer:extension_printer -> ?short_printer:extension_printer ->
+  ?is_same_ext:extension_same -> bool -> unit
+
 type extension_single = {
   preprocessor: extension_preprocessor ;
   typer: extension_typer ;
@@ -53,6 +71,7 @@ type extension_common = {
   printer: extension_printer ;
   short_printer: extension_printer ;
   plugin: string;
+  is_same_ext: extension_same;
 }
 
 let default_printer printer fmt = function
@@ -64,6 +83,19 @@ let default_printer printer fmt = function
 
 let default_short_printer name _printer fmt _ext_kind = Format.fprintf fmt "%s" name
 
+let rec default_is_same_ext ext1 ext2 env =
+  match ext1, ext2 with
+  | Ext_id n1, Ext_id n2 -> n1 = n2
+  | Ext_terms l1, Ext_terms l2 ->
+    Ast_diff.is_same_list Ast_diff.is_same_term l1 l2 env
+  | Ext_preds l1, Ext_preds l2 ->
+    Ast_diff.is_same_list Ast_diff.is_same_predicate l1 l2 env
+  | Ext_annot(s1,l1), Ext_annot(s2,l2) ->
+    s1 = s2 && Ast_diff.is_same_list default_is_same_ext_kind l1 l2 env
+  | (Ext_id _ | Ext_terms _ | Ext_preds _ | Ext_annot _), _ -> false
+and default_is_same_ext_kind ext1 ext2 env =
+  default_is_same_ext ext1.ext_kind ext2.ext_kind env
+
 let make
     ~plugin
     name category
@@ -72,9 +104,10 @@ let make
     ?(visitor=fun _ _ -> Cil.DoChildren)
     ?(printer=default_printer)
     ?(short_printer=default_short_printer name)
+    ?(is_same_ext=default_is_same_ext)
     status : extension_single*extension_common =
   { preprocessor; typer; status},
-  { category; visitor; printer; short_printer; plugin }
+  { category; visitor; printer; short_printer; plugin; is_same_ext }
 
 let make_block
     ~plugin
@@ -84,9 +117,10 @@ let make_block
     ?(visitor=fun _ _ -> Cil.DoChildren)
     ?(printer=default_printer)
     ?(short_printer=default_short_printer name)
+    ?(is_same_ext=default_is_same_ext)
     status : extension_block*extension_common =
   { preprocessor; typer; status},
-  { category; visitor; printer; short_printer; plugin }
+  { category; visitor; printer; short_printer; plugin; is_same_ext }
 
 module Extensions = struct
   (*hash table for  category, visitor, printer and short_printer of extensions*)
@@ -119,10 +153,10 @@ module Extensions = struct
   let is_extension_block = Hashtbl.mem ext_block_tbl
 
   let register cat ~plugin name
-      ?preprocessor typer ?visitor ?printer ?short_printer status =
+      ?preprocessor typer ?visitor ?printer ?short_printer ?is_same_ext status =
     let info1,info2 =
       make ~plugin name cat ?preprocessor typer
-        ?visitor ?printer ?short_printer status
+        ?visitor ?printer ?short_printer ?is_same_ext status
     in
     if is_extension name then
       Kernel.warning ~wkey:Kernel.wkey_acsl_extension
@@ -135,10 +169,10 @@ module Extensions = struct
       end
 
   let register_block cat ~plugin name
-      ?preprocessor typer ?visitor ?printer ?short_printer status =
+      ?preprocessor typer ?visitor ?printer ?short_printer ?is_same_ext status =
     let info1,info2 =
       make_block ~plugin name cat ?preprocessor typer
-        ?visitor ?printer ?short_printer status
+        ?visitor ?printer ?short_printer ?is_same_ext status
     in
     if is_extension name then
       Kernel.warning ~wkey:Kernel.wkey_acsl_extension
@@ -207,6 +241,10 @@ module Extensions = struct
     let pp = (find_common name).short_printer in
     Format.fprintf fmt "%a" (pp printer) kind
 
+  let is_same_ext name ext1 ext2 =
+    let is_same = (find_common name).is_same_ext in
+    is_same ext1 ext2
+
   let extension_from name = (find_common name).plugin
 end
 
@@ -245,4 +283,6 @@ let () =
     ~visit: Extensions.visit ;
   Cil_printer.set_extension_handler
     ~print: Extensions.print
-    ~short_print:Extensions.short_print
+    ~short_print:Extensions.short_print;
+  Ast_diff.set_extension_diff
+    ~is_same_ext: Extensions.is_same_ext
diff --git a/src/kernel_services/ast_queries/acsl_extension.mli b/src/kernel_services/ast_queries/acsl_extension.mli
index 3fb2eec90aad5dfaac12788309e29a42fe094d53..a6cf1a108a64e16beaff0500c60884132537ed4f 100644
--- a/src/kernel_services/ast_queries/acsl_extension.mli
+++ b/src/kernel_services/ast_queries/acsl_extension.mli
@@ -51,11 +51,15 @@ type extension_printer =
   Printer_api.extensible_printer_type -> Format.formatter ->
   acsl_extension_kind -> unit
 
+(** type of functions that compare two extensions (with the same keyword)
+    to decide if they're identical or not. See {!Ast_diff} for more information.
+    @since Frama-C+dev
+*)
+type extension_same =
+  acsl_extension_kind -> acsl_extension_kind -> Ast_diff.is_same_env -> bool
 
-(** [register_behavior
-      ~plugin name ~preprocessor typer ~visitor ~printer ~short_printer status]
-    registers new ACSL extension to be used in function contracts with name
-    [name] and plugin [plugin].
+(** type of functions that register new ACSL extensions to be used in place of
+    various kinds of ACSL annotations.
 
     The labelled parameter [plugin] is used to specify which plugin registers
     this new extension. It can be used, together with the syntax
@@ -84,6 +88,11 @@ type extension_printer =
     behavior for the ACSL extension. By default, it just prints the [name]. It
     is for example used for the filetree in the GUI.
 
+    The optional [is_same_ext] parameter allows checking whether two versions
+    of the extended annotation are identical or not during a run of
+    {!Ast_diff.compare_ast}. By default, [Ast_diff] will compare the lists
+    of terms/predicates.
+
     The [status] indicates whether the extension can be assigned a property
     status or not.
 
@@ -100,89 +109,47 @@ type extension_printer =
       | [] -> let id = !count in incr count; Ext_id id
       | _ -> typing_context.error loc "expecting a predicate after keyword FOO"
     let () =
-      Acsl_extension.register_behavior ~pugin:"myplugin" "FOO" foo_typer false
+      Acsl_extension.register_behavior ~plugin:"myplugin" "FOO" foo_typer false
     ]
-    @before Frama-C+dev the parameter [plugin] was not present
+    @before Frama-C+dev parameters [plugin] and [is_same_ext] were not present
     @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
 *)
-val register_behavior:
+type register_extension =
   plugin:string -> string ->
   ?preprocessor:extension_preprocessor -> extension_typer ->
   ?visitor:extension_visitor ->
-  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
+  ?printer:extension_printer -> ?short_printer:extension_printer ->
+  ?is_same_ext:extension_same -> bool ->
   unit
 
-(** Registers extension for global annotation. See {!register_behavior}.
-
-    @before Frama-C+dev the parameter [plugin] was not present
-    @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
-*)
-val register_global:
-  plugin:string -> string ->
-  ?preprocessor:extension_preprocessor -> extension_typer ->
-  ?visitor:extension_visitor ->
-  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
-  unit
-
-(** Registers extension for global block annotation. See {!register_behavior}.
-
-    @before Frama-C+dev the parameter [plugin] was not present
-    @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
-*)
-val register_global_block:
-  plugin:string -> string ->
+(** same as {!register_extension}, but for extensions that parse an axiomatic
+    block, resulting in a {!Cil_types.Ext_annot}. *)
+type register_extension_block =
+  plugin: string -> string ->
   ?preprocessor:extension_preprocessor_block -> extension_typer_block ->
   ?visitor:extension_visitor ->
-  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
-  unit
-
-(** Registers extension for code annotation to be evaluated at _current_
-    program point. See {!register_behavior}.
+  ?printer:extension_printer -> ?short_printer:extension_printer ->
+  ?is_same_ext:extension_same -> bool -> unit
 
-    @before Frama-C+dev the parameter [plugin] was not present
-    @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
-*)
-val register_code_annot:
-  plugin:string -> string ->
-  ?preprocessor:extension_preprocessor -> extension_typer ->
-  ?visitor:extension_visitor ->
-  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
-  unit
+(** Register a behavior extension, i.e. new clauses of contracts *)
+val register_behavior: register_extension
 
-(** Registers extension for code annotation to be evaluated for the _next_
-    statement. See {!register_behavior}.
+(** Register extension for global annotation. *)
+val register_global: register_extension
 
-    @before Frama-C+dev the parameter [plugin] was not present
-    @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
-*)
-val register_code_annot_next_stmt:
-  plugin:string -> string ->
-  ?preprocessor:extension_preprocessor -> extension_typer ->
-  ?visitor:extension_visitor ->
-  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
-  unit
+(** Registers extension for global block annotation. *)
+val register_global_block: register_extension_block
 
-(** Registers extension for loop annotation. See {!register_behavior}.
+(** Registers extension for code annotation to be evaluated at _current_
+    program point. *)
+val register_code_annot: register_extension
 
-    @before Frama-C+dev the parameter [plugin] was not present
-    @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
-*)
-val register_code_annot_next_loop:
-  plugin:string -> string ->
-  ?preprocessor:extension_preprocessor -> extension_typer ->
-  ?visitor:extension_visitor ->
-  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
-  unit
+(** Registers extension for code annotation to be evaluated for the _next_
+    statement. *)
+val register_code_annot_next_stmt: register_extension
 
-(** Registers extension both for code and loop annotations.
-    See {!register_behavior}.
+(** Registers extension for loop annotation. *)
+val register_code_annot_next_loop: register_extension
 
-    @before Frama-C+dev the parameter [plugin] was not present
-    @see <https://frama-c.com/download/frama-c-plugin-development-guide.pdf>
-*)
-val register_code_annot_next_both:
-  plugin:string -> string ->
-  ?preprocessor:extension_preprocessor -> extension_typer ->
-  ?visitor:extension_visitor ->
-  ?printer:extension_printer -> ?short_printer:extension_printer -> bool ->
-  unit
+(** Registers extension both for code and loop annotations. *)
+val register_code_annot_next_both: register_extension
diff --git a/src/kernel_services/ast_queries/ast_diff.ml b/src/kernel_services/ast_queries/ast_diff.ml
index 6b325af4221883ee88ed4c23d29c505cc3e26817..1c6eb15b7f70e459f651ddd8b7a710665142a40c 100644
--- a/src/kernel_services/ast_queries/ast_diff.ml
+++ b/src/kernel_services/ast_queries/ast_diff.ml
@@ -195,6 +195,17 @@ type is_same_env =
     enumitem: enumitem Cil_datatype.Enumitem.Map.t;
   }
 
+let is_same_acsl_extension_kind:
+  (string->acsl_extension_kind->acsl_extension_kind->is_same_env->bool) ref
+  = Extlib.mk_fun "Ast_diff.is_same_acsl_extension"
+
+let set_extension_diff ~is_same_ext =
+  is_same_acsl_extension_kind := is_same_ext
+
+let is_same_acsl_extension ext1 ext2 env =
+  ext1.ext_name = ext2.ext_name &&
+  !is_same_acsl_extension_kind ext1.ext_name ext1.ext_kind ext2.ext_kind env
+
 module type Correspondence_table = sig
   include State_builder.Hashtbl
   val pretty_data: Format.formatter -> data -> unit
@@ -257,6 +268,9 @@ let make_correspondence candidate has_same_spec code_corres =
   | true, ((`Body_changed|`Callees_changed) as c) ->
     `Partial(candidate, c)
 
+let make_body_correspondence has_same_spec code_corres =
+  if has_same_spec then code_corres else `Body_changed
+
 let (&&>) (res,env) f =
   match res with
   | `Body_changed -> `Body_changed, env
@@ -693,9 +707,8 @@ and is_same_behavior b b' env =
   is_same_list is_same_identified_predicate b.b_assumes b'.b_assumes env &&
   is_same_list is_same_post_cond b.b_post_cond b'.b_post_cond env &&
   is_same_assigns b.b_assigns b'.b_assigns env &&
-  is_same_allocation b.b_allocation b'.b_allocation env
-(* TODO: also consider ACSL extensions, with the help of the plugins
-   that handle them. *)
+  is_same_allocation b.b_allocation b'.b_allocation env &&
+  is_same_list is_same_acsl_extension b.b_extended b'.b_extended env
 
 and is_same_variant (v,m) (v',m') env =
   is_same_term v v' env && is_same_opt is_matching_logic_info m m' env
@@ -762,7 +775,10 @@ and is_same_code_annotation a a' env =
   | AAllocation(bhvs, a), AAllocation(bhvs',a') ->
     is_same_behavior_set bhvs bhvs' && is_same_allocation a a' env
   | APragma p, APragma p' -> is_same_pragma p p' env
-  | AExtended _, AExtended _ -> true (*TODO: checks also for extended clauses*)
+  | AExtended (bhvs, is_next, ext),
+    AExtended (bhvs', is_next', ext') ->
+    is_same_behavior_set bhvs bhvs' && is_next = is_next' &&
+    is_same_acsl_extension ext ext' env
   | (AAssert _ | AStmtSpec _ | AInvariant _ | AVariant _ | AAssigns _
     | AAllocation _ | APragma _ | AExtended _), _ -> false
 
@@ -1156,8 +1172,9 @@ and is_same_stmt s s' env =
         | _ -> `Body_changed, env
       end else `Body_changed, env
   in
-  let res = make_correspondence s' annot_res code_res in
-  Stmt.add s res; code_res, env
+  let corres = make_correspondence s' annot_res code_res in
+  let res = make_body_correspondence annot_res code_res in
+  Stmt.add s corres; res, env
 
 (* is_same_block will return its modified environment in order
    to update correspondence table with respect to locals, in case
@@ -1537,9 +1554,8 @@ let rec gannot_correspondence =
     ignore (logic_info_correspondence ~loc li empty_env)
   | Dmodel_annot (mi,loc) ->
     ignore (model_info_correspondence ~loc mi)
-  | Dextended _ -> ()
-(* TODO: provide mechanism for extension themselves
-   to give relevant information. *)
+  | Dextended _ -> () (* TODO: as for lemmas, we don't really have a structure
+                         where to look for a matching extended annotation. *)
 
 let global_correspondence g =
   match g with
diff --git a/src/kernel_services/ast_queries/ast_diff.mli b/src/kernel_services/ast_queries/ast_diff.mli
index dc3c9ea69ac226bfdd5b981f142422b0e583ece5..c0350ab97c3c5ba0b4a813ec5ec8e74537e4c7ab 100644
--- a/src/kernel_services/ast_queries/ast_diff.mli
+++ b/src/kernel_services/ast_queries/ast_diff.mli
@@ -117,6 +117,24 @@ module Fundec:
   Correspondence_table
   with type key = fundec and type data = fundec correspondence
 
+(** map of symbols currently under comparison,
+    with their correspondence status so far *)
+type is_same_env
+
+val is_same_list:
+  ('a -> 'a -> is_same_env -> bool) -> 'a list -> 'a list -> is_same_env -> bool
+
+val is_same_term: term -> term -> is_same_env -> bool
+
+val is_same_predicate: predicate -> predicate -> is_same_env -> bool
+
+(** access custom comparison functions for ACSL extensions *)
+val set_extension_diff:
+  is_same_ext:
+    (string ->
+     acsl_extension_kind -> acsl_extension_kind -> is_same_env -> bool)
+  -> unit
+
 (** performs a comparison of AST between the current and the original
     project, which must have been set beforehand.
 *)
diff --git a/tests/spec/Extend_preprocess.ml b/tests/spec/Extend_preprocess.ml
index 1d3fb6d9502a66099f3af8b65f0cdc9412788445..d0e24ef0871e79125face9bae322ff3667c47a55 100644
--- a/tests/spec/Extend_preprocess.ml
+++ b/tests/spec/Extend_preprocess.ml
@@ -36,14 +36,14 @@ let preprocess_foo_ptree_element kind = function
 
 let preprocess_foo_ptree kind = List.map (preprocess_foo_ptree_element kind)
 
-let register registration ?visitor ?printer ?short_printer kind =
+let register registration ?visitor ?printer ?short_printer ?is_same_ext kind =
   let registration ?preprocessor typer =
     registration
-      (kind ^ "_foo") ?preprocessor typer ?visitor ?printer ?short_printer false
+      (kind ^ "_foo")
+      ?preprocessor typer ?visitor ?printer ?short_printer ?is_same_ext false
   in
   registration ~preprocessor:(preprocess_foo_ptree kind) (ext_typing kind)
 
-
 let () =
   let open Acsl_extension in
   register (register_behavior ~plugin:"test" ) "bhv";
diff --git a/tests/syntax/ast_diff_1.i b/tests/syntax/ast_diff_1.i
index 7afc3a0e3b37b57df5eb2bfe9d78d281e6e14d44..86b0c7606e68395abec4be4f0e5f217d056450c7 100644
--- a/tests/syntax/ast_diff_1.i
+++ b/tests/syntax/ast_diff_1.i
@@ -1,4 +1,6 @@
 /* run.config
+   COMMENT: we need Eva for the loop unroll ACSL extension
+   PLUGIN: eva
    MODULE: @PTEST_NAME@
      OPT: -then -ast-diff %{dep:ast_diff_2.c}
      OPT: -then -ast-diff %{dep:ast_diff_2.c} -cpp-extra-args="-DADD_ENUM_TAG"
@@ -107,3 +109,13 @@ void se() {
   struct s S;
   S.c[0] = 1;
 }
+
+void with_loop_unroll_same() {
+  //@ loop unroll 5;
+  for (int i = 0; i < 5; i++);
+}
+
+void with_loop_unroll_diff() {
+  //@ loop unroll 4;
+  for (int i = 0; i < 5; i++);
+}
diff --git a/tests/syntax/ast_diff_1.ml b/tests/syntax/ast_diff_1.ml
index 1a85f02e29488f26c4e06a1b0359cbc4a2307f6c..3bab5ff951056eb106b8cb9eec3f9739b8e1baf6 100644
--- a/tests/syntax/ast_diff_1.ml
+++ b/tests/syntax/ast_diff_1.ml
@@ -1,3 +1,5 @@
+open Cil_types
+
 include Plugin.Register(
   struct
     let name = "AST diff test"
@@ -15,13 +17,36 @@ let show_fun kf c =
     Kernel_function.pretty kf
     Ast_diff.Kernel_function.pretty_data c
 
+let cmp_fun kf1 kf2 =
+  Datatype.String.compare
+    (Kernel_function.get_vi kf1).vname (Kernel_function.get_vi kf2).vname
+
+let cmp_var v1 v2 =
+  let res = Datatype.String.compare v1.vname v2.vname in
+  if res <> 0 then res
+  else if v1.vglob && v2.vglob then 0
+  else if v1.vglob then -1
+  else if v2.vglob then 1
+  else if v1.vstorage = Static && v2.vstorage = Static then 0
+  else if v1.vstorage = Static then -1
+  else if v2.vstorage = Static then 1
+  else begin
+    let prj = Ast_diff.Orig_project.get() in
+    let kf1 = Project.on prj Kernel_function.find_defining_kf v1 in
+    let kf2 = Project.on prj Kernel_function.find_defining_kf v2 in
+    if Option.is_none kf1 || Option.is_none kf2 then
+      fatal "Variable %a(%a) is not global but has no associated function"
+        Cil_datatype.Varinfo.pretty v1 Cil_datatype.Location.pretty v1.vdecl;
+    cmp_fun (Option.get kf1) (Option.get kf2)
+  end
+
 let show_correspondances () =
   if Kernel.AstDiff.get () then begin
     result "Showing correspondances between %s and %s"
       (Project.get_name (Ast_diff.Orig_project.get()))
       (Project.get_name (Project.current()));
-    Ast_diff.Varinfo.iter show_var;
-    Ast_diff.Kernel_function.iter show_fun;
+    Ast_diff.Varinfo.iter_sorted ~cmp:cmp_var show_var;
+    Ast_diff.Kernel_function.iter_sorted ~cmp:cmp_fun show_fun;
   end
 
 let () = Boot.Main.extend show_correspondances
diff --git a/tests/syntax/ast_diff_2.c b/tests/syntax/ast_diff_2.c
index c0bd72914c114fde906e283bda7ba599497e621a..f0009e13c1827c06787605dae812ac2ed3d60cd3 100644
--- a/tests/syntax/ast_diff_2.c
+++ b/tests/syntax/ast_diff_2.c
@@ -102,3 +102,13 @@ void se() {
   struct s S;
   S.c[0] = 1;
 }
+
+void with_loop_unroll_same() {
+  //@ loop unroll 5;
+  for (int i = 0; i < 5; i++);
+}
+
+void with_loop_unroll_diff() {
+  //@ loop unroll 5;
+  for (int i = 0; i < 5; i++);
+}
diff --git a/tests/syntax/oracle/ast_diff_1.0.res.oracle b/tests/syntax/oracle/ast_diff_1.0.res.oracle
index 040eb7eac6a64962c2abd84ec40b54ea065123b1..fbb86f340f5f9bfe962414c2d0da05c5cd549ea2 100644
--- a/tests/syntax/oracle/ast_diff_1.0.res.oracle
+++ b/tests/syntax/oracle/ast_diff_1.0.res.oracle
@@ -1,45 +1,50 @@
 [kernel] Parsing ast_diff_1.i (no preprocessing)
 [kernel] Parsing ast_diff_2.c (with preprocessing)
 [AST diff test] Showing correspondances between orig_default and default
-[AST diff test] Variable i:  => i
-[AST diff test] Variable local_var_use:  => local_var_use
-[AST diff test] Variable v:  => w
-[AST diff test] Variable a:  => q
-[AST diff test] Variable x:  => z
-[AST diff test] Variable y:  => t
-[AST diff test] Variable s:  => s
-[AST diff test] Variable use_s:  => use_s
-[AST diff test] Variable x:  => x
-[AST diff test] Variable with_goto_changed:  => with_goto_changed
+[AST diff test] Variable S:  => S
 [AST diff test] Variable X:  => X
 [AST diff test] Variable Y: N/A
+[AST diff test] Variable __retres:  => __retres
+[AST diff test] Variable a:  => q
 [AST diff test] Variable c:  => c
-[AST diff test] Variable f:  => f
-[AST diff test] Variable with_goto_unchanged:  => with_goto_unchanged
-[AST diff test] Variable x:  => x
 [AST diff test] Variable c:  => c
+[AST diff test] Variable decl:  => decl
+[AST diff test] Variable f:  => f
 [AST diff test] Variable g:  => g
-[AST diff test] Variable se:  => se
-[AST diff test] Variable S:  => S
-[AST diff test] Variable has_static_local_x:  => has_static_local_y
 [AST diff test] Variable h:  => h
-[AST diff test] Variable __retres:  => __retres
+[AST diff test] Variable has_static_local:  => has_static_local
+[AST diff test] Variable has_static_local_x:  => has_static_local_y
+[AST diff test] Variable i:  => i
+[AST diff test] Variable i_0:  => i_0
+[AST diff test] Variable local_var_use:  => local_var_use
+[AST diff test] Variable ptr_func:  => ptr_func
+[AST diff test] Variable s:  => s
+[AST diff test] Variable se:  => se
 [AST diff test] Variable use_logic_builtin:  => use_logic_builtin
+[AST diff test] Variable use_s:  => use_s
+[AST diff test] Variable used_in_decl:  => used_in_decl
+[AST diff test] Variable v:  => w
+[AST diff test] Variable with_goto_changed:  => with_goto_changed
+[AST diff test] Variable with_goto_unchanged:  => with_goto_unchanged
+[AST diff test] Variable with_loop_unroll_diff:  => with_loop_unroll_diff
+[AST diff test] Variable with_loop_unroll_same:  => with_loop_unroll_same
+[AST diff test] Variable x:  => x
+[AST diff test] Variable x:  => z
+[AST diff test] Variable x:  => x
 [AST diff test] Variable x:  => x
+[AST diff test] Variable y:  => t
 [AST diff test] Variable y:  => y
-[AST diff test] Variable has_static_local:  => has_static_local
-[AST diff test] Variable decl:  => decl
-[AST diff test] Variable used_in_decl:  => used_in_decl
-[AST diff test] Variable ptr_func:  => ptr_func
+[AST diff test] Function decl:  => decl
+[AST diff test] Function f:  => f
+[AST diff test] Function g: N/A
+[AST diff test] Function h: -> h (body changed)
+[AST diff test] Function has_static_local:  => has_static_local
 [AST diff test] Function i:  => i
 [AST diff test] Function local_var_use:  => local_var_use
+[AST diff test] Function se:  => se
+[AST diff test] Function use_logic_builtin:  => use_logic_builtin
 [AST diff test] Function use_s:  => use_s
 [AST diff test] Function with_goto_changed: -> with_goto_changed (body changed)
-[AST diff test] Function f:  => f
 [AST diff test] Function with_goto_unchanged:  => with_goto_unchanged
-[AST diff test] Function g: N/A
-[AST diff test] Function se:  => se
-[AST diff test] Function h: -> h (body changed)
-[AST diff test] Function use_logic_builtin:  => use_logic_builtin
-[AST diff test] Function has_static_local:  => has_static_local
-[AST diff test] Function decl:  => decl
+[AST diff test] Function with_loop_unroll_diff: -> with_loop_unroll_diff (body changed)
+[AST diff test] Function with_loop_unroll_same:  => with_loop_unroll_same
diff --git a/tests/syntax/oracle/ast_diff_1.1.res.oracle b/tests/syntax/oracle/ast_diff_1.1.res.oracle
index 1fe85b83738a956efe119cd4c29b473fbeea6ede..30191fcff0a2c7db4e5c570acdb5667a0d137caf 100644
--- a/tests/syntax/oracle/ast_diff_1.1.res.oracle
+++ b/tests/syntax/oracle/ast_diff_1.1.res.oracle
@@ -2,42 +2,47 @@
 [kernel] Parsing ast_diff_2.c (with preprocessing)
 [kernel] Parsing ast_diff_1.i (no preprocessing)
 [AST diff test] Showing correspondances between orig_default and default
-[AST diff test] Variable use_logic_builtin:  => use_logic_builtin
-[AST diff test] Variable x:  => x
-[AST diff test] Variable y:  => y
-[AST diff test] Variable has_static_local:  => has_static_local
+[AST diff test] Variable X:  => X
+[AST diff test] Variable Y: N/A
+[AST diff test] Variable a:  => q
+[AST diff test] Variable c:  => c
+[AST diff test] Variable c:  => c
 [AST diff test] Variable decl:  => decl
-[AST diff test] Variable used_in_decl:  => used_in_decl
-[AST diff test] Variable ptr_func:  => ptr_func
+[AST diff test] Variable f:  => f
+[AST diff test] Variable g:  => g
+[AST diff test] Variable h:  => h
+[AST diff test] Variable has_static_local:  => has_static_local
+[AST diff test] Variable has_static_local_x:  => has_static_local_y
 [AST diff test] Variable i:  => i
+[AST diff test] Variable i_0:  => i_0
 [AST diff test] Variable local_var_use:  => local_var_use
-[AST diff test] Variable v:  => w
-[AST diff test] Variable a:  => q
-[AST diff test] Variable x:  => z
-[AST diff test] Variable y:  => t
+[AST diff test] Variable ptr_func:  => ptr_func
 [AST diff test] Variable s: N/A
+[AST diff test] Variable se:  => se
+[AST diff test] Variable use_logic_builtin:  => use_logic_builtin
 [AST diff test] Variable use_s: N/A
+[AST diff test] Variable used_in_decl:  => used_in_decl
+[AST diff test] Variable v:  => w
 [AST diff test] Variable with_goto_changed:  => with_goto_changed
-[AST diff test] Variable X:  => X
-[AST diff test] Variable Y: N/A
-[AST diff test] Variable c:  => c
-[AST diff test] Variable f:  => f
 [AST diff test] Variable with_goto_unchanged:  => with_goto_unchanged
+[AST diff test] Variable with_loop_unroll_diff:  => with_loop_unroll_diff
+[AST diff test] Variable with_loop_unroll_same:  => with_loop_unroll_same
 [AST diff test] Variable x:  => x
-[AST diff test] Variable c:  => c
-[AST diff test] Variable g:  => g
-[AST diff test] Variable se:  => se
-[AST diff test] Variable has_static_local_x:  => has_static_local_y
-[AST diff test] Variable h:  => h
-[AST diff test] Function use_logic_builtin:  => use_logic_builtin
-[AST diff test] Function has_static_local:  => has_static_local
+[AST diff test] Variable x:  => z
+[AST diff test] Variable x:  => x
+[AST diff test] Variable y:  => t
+[AST diff test] Variable y:  => y
 [AST diff test] Function decl:  => decl
+[AST diff test] Function f:  => f
+[AST diff test] Function g: N/A
+[AST diff test] Function h: -> h (body changed)
+[AST diff test] Function has_static_local:  => has_static_local
 [AST diff test] Function i:  => i
 [AST diff test] Function local_var_use:  => local_var_use
+[AST diff test] Function se: -> se (body changed)
+[AST diff test] Function use_logic_builtin:  => use_logic_builtin
 [AST diff test] Function use_s: N/A
 [AST diff test] Function with_goto_changed: -> with_goto_changed (body changed)
-[AST diff test] Function f:  => f
 [AST diff test] Function with_goto_unchanged:  => with_goto_unchanged
-[AST diff test] Function g: N/A
-[AST diff test] Function se: -> se (body changed)
-[AST diff test] Function h: -> h (body changed)
+[AST diff test] Function with_loop_unroll_diff: -> with_loop_unroll_diff (body changed)
+[AST diff test] Function with_loop_unroll_same:  => with_loop_unroll_same