diff --git a/src/kernel_internals/parsing/logic_parser.mly b/src/kernel_internals/parsing/logic_parser.mly
index d96ad86c4f7bc3d131e882feb2dc9cf60f1f2d80..66cc4871b219c24fb147fd2d2609a8cf47c5ac62 100644
--- a/src/kernel_internals/parsing/logic_parser.mly
+++ b/src/kernel_internals/parsing/logic_parser.mly
@@ -116,16 +116,16 @@
       let f ds d = if List.exists (is_same_lexpr d) ds then ds else d :: ds in
       l, From(List.(rev (fold_left f [] ds)))
 
-  let concat_froms a1 a2 =
-    let compare_pair (b1,_) (b2,_) = is_same_lexpr b1 b2 in
+  let concat_froms cura newa =
+    let compare_pair (curb,_) (newb,_) = is_same_lexpr curb newb in
     (* NB: the following has an horrible complexity, but the order of
        clauses in the input is preserved. *)
-    let concat_one acc (l, f2)  =
-      let (_, f2) as p = filter_from l f2 in
+    let concat_one acc (l, newf)  =
+      let (_, newf) as p = filter_from l newf in
       try
-        let (_,f1) = List.find (compare_pair p) acc
+        let (_,curf) = List.find (compare_pair p) acc
         in
-        match (f1, f2) with
+        match (curf, newf) with
           | _,FromAny ->
             (* the new fundeps does not give more information than the one
                which is already present. Just ignore it.
@@ -138,12 +138,15 @@
                  that we get the exact same clause if we try to
                  link the original contract with its pretty-printed version. *)
               Extlib.replace compare_pair p acc
-          | From _, From _ ->
-            (* we keep the two functional dependencies,
-               as they have to be proved separately. *)
-            acc @ [p]
+          | From curl, From newl ->
+            let incl l lin =
+              List.(for_all (fun e -> exists (is_same_lexpr e) lin) l)
+            in
+            if      incl curl newl then acc
+            else if incl newl curl then Extlib.replace compare_pair p acc
+            else acc @ [p]
       with Not_found -> acc @ [p]
-    in List.fold_left concat_one a1 a2
+    in List.fold_left concat_one cura newa
 
   let concat_allocation fa1 fa2 =
     match fa1,fa2 with
diff --git a/tests/rte/oracle/assign4.res.oracle b/tests/rte/oracle/assign4.res.oracle
index 4ce28ed1aba25b34732c23053edffd88fc1acbd3..143f1a6b3fcb116c94c4f1f3e00b27372d1e075d 100644
--- a/tests/rte/oracle/assign4.res.oracle
+++ b/tests/rte/oracle/assign4.res.oracle
@@ -6,9 +6,7 @@
 int choose1(int min, int max);
 
 /*@ assigns \result;
-    assigns \result \from min, max;
-    assigns \result \from min, max;
- */
+    assigns \result \from min, max; */
 int choose2(int min, int max);
 
 int main(void)
diff --git a/tests/rte/oracle/assign5.res.oracle b/tests/rte/oracle/assign5.res.oracle
index c72860ec208ca0f7f4e5a6df05da28856c05c613..b8dd6f9a5408f3f1bb05de08fd78656412953b85 100644
--- a/tests/rte/oracle/assign5.res.oracle
+++ b/tests/rte/oracle/assign5.res.oracle
@@ -2,13 +2,11 @@
 [rte] annotating function main
 /* Generated by Frama-C */
 /*@ assigns *p;
-    assigns *p \from x;
     assigns *p \from \nothing; */
 int f(int *p, int x);
 
 /*@ assigns *p;
-    assigns *p \from \nothing;
-    assigns *p \from x; */
+    assigns *p \from \nothing; */
 int g(int *p, int x);
 
 int main(void)
diff --git a/tests/syntax/multiple_froms.i b/tests/syntax/multiple_froms.i
index 9903819400faf04b705c3badf8d9990388b7e4f3..6a0a25687f9e2960e533cbec4ac5dbc0dc21e286 100644
--- a/tests/syntax/multiple_froms.i
+++ b/tests/syntax/multiple_froms.i
@@ -1,11 +1,15 @@
 int a, b, c, d, e;
 
+// Reminder: assigns are visited in reverse
+
 /*@ assigns a;
-    assigns a \from a, a, b, c, c;
+    assigns a \from a, a, b, c, c; // more precise so replace the next one
     assigns a \from c, b, d, e, a;
     assigns a;
-    assigns b \from a, e, b, d, c;
-    assigns c \from c, c, c, c, c;
+    assigns b \from a, e, b, d, c; // is ignored because the next one is more precise
+    assigns b \from a, e;
+    assigns c \from c, c, c, c, c; // both are kept (no inclusion)
+    assigns c \from d;
  */
 void function(void)
 {
diff --git a/tests/syntax/oracle/multiple_froms.res.oracle b/tests/syntax/oracle/multiple_froms.res.oracle
index eac436bb15e27f1c02399c35a5ca6292d7b938fa..421f9c3f94dd3e4a45dc412c15674b6f181c23ff 100644
--- a/tests/syntax/oracle/multiple_froms.res.oracle
+++ b/tests/syntax/oracle/multiple_froms.res.oracle
@@ -7,9 +7,9 @@ int d;
 int e;
 /*@ assigns a, b, c;
     assigns a \from a, b, c;
-    assigns a \from c, b, d, e, a;
-    assigns b \from a, e, b, d, c;
+    assigns b \from a, e;
     assigns c \from c;
+    assigns c \from d;
  */
 void function(void)
 {