diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index a86fbfb6d2588301194bcf986db745d69ec60ba7..855cd1b3312d97a4a887f7dff4df4546b6f6f69b 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -1643,6 +1643,8 @@ src/plugins/wp/TacRange.ml: CEA_WP
src/plugins/wp/TacRange.mli: CEA_WP
src/plugins/wp/TacRewrite.ml: CEA_WP
src/plugins/wp/TacRewrite.mli: CEA_WP
+src/plugins/wp/TacSequence.ml: CEA_WP
+src/plugins/wp/TacSequence.mli: CEA_WP
src/plugins/wp/TacShift.ml: CEA_WP
src/plugins/wp/TacShift.mli: CEA_WP
src/plugins/wp/TacSplit.ml: CEA_WP
diff --git a/src/plugins/wp/Makefile.in b/src/plugins/wp/Makefile.in
index 2d81efcad32e86e800f6a2f0d61bec9eab53b4c7..2f7ebfb458abb852409764942639b31e831e2e90 100644
--- a/src/plugins/wp/Makefile.in
+++ b/src/plugins/wp/Makefile.in
@@ -90,6 +90,7 @@ PLUGIN_CMO:= \
TacHavoc TacInstance TacLemma \
TacFilter TacCut WpTac TacNormalForm \
TacRewrite TacBitwised TacBitrange TacBittest TacShift \
+ TacSequence \
TacCongruence TacOverflow Auto \
ProofSession ProofScript ProofEngine \
ProverTask ProverErgo ProverCoq \
diff --git a/src/plugins/wp/TacSequence.ml b/src/plugins/wp/TacSequence.ml
new file mode 100644
index 0000000000000000000000000000000000000000..1c711e93757918c7897d361407ad1bdf52c92162
--- /dev/null
+++ b/src/plugins/wp/TacSequence.ml
@@ -0,0 +1,92 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+open Lang
+
+let negative n = F.p_leq n F.e_zero
+let positive n = F.p_leq F.e_zero n
+let concat ~result es = F.e_fun ~result Vlist.f_concat es
+let repeat ~result a n = F.e_fun ~result Vlist.f_repeat [a;n]
+let sum n = match F.repr n with
+ | Add ns -> ns
+ | _ -> [n]
+
+(* -------------------------------------------------------------------------- *)
+(* --- Induction Tactical --- *)
+(* -------------------------------------------------------------------------- *)
+
+let vmode,pmode =
+ Tactical.selector ~id:"seq.side" ~title:"Mode" ~descr:"Unrolling mode"
+ ~options:[
+ { vid = "left" ; title = "Unroll left" ;
+ descr = "Transform (A^n) into (A.A^n-1)" ; value = `Left } ;
+ { vid = "right" ; title = "Unroll right" ;
+ descr = "Transform (A^n) into (A^n-1.A)" ; value = `Right } ;
+ { vid = "sum" ; title = "Concat sum" ;
+ descr = "Transform A^(p+q) into (A^p.A^q)" ; value = `Sum }
+ ] ()
+
+class sequence =
+ object(self)
+ inherit Tactical.make
+ ~id:"Wp.sequence"
+ ~title:"Sequence"
+ ~descr:"Unroll repeat-sequence operator"
+ ~params:[pmode]
+
+ method select _feedback (s : Tactical.selection) =
+ let value = Tactical.selected s in
+ match F.repr value with
+ | Fun(f,[a;n]) when f == Vlist.f_repeat ->
+ let result = F.typeof value in
+ let at = Tactical.at s in
+ Applicable
+ begin
+ match self#get_field vmode with
+ | `Sum ->
+ let ns = sum n in
+ let pos = F.p_all positive ns in
+ let cat = concat ~result (List.map (repeat ~result a) ns) in
+ Tactical.condition "Positive" pos @@
+ Tactical.rewrite ?at [ "Unroll" , pos , value , cat ]
+ | `Left ->
+ let p = F.e_add n F.e_minus_one in
+ let unroll = concat ~result [a ; repeat ~result a p] in
+ Tactical.rewrite ?at [
+ "Nil", negative n , value , concat ~result [] ;
+ "Unroll", positive p , value , unroll ;
+ ]
+ | `Right ->
+ let p = F.e_add n F.e_minus_one in
+ let unroll = concat ~result [repeat ~result a p ; a] in
+ Tactical.rewrite ?at [
+ "Nil", negative n , value , concat ~result [] ;
+ "Unroll", positive p , value , unroll ;
+ ]
+ end
+ | _ -> Not_applicable
+
+ end
+
+let tactical = Tactical.export (new sequence)
+
+(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/TacSequence.mli b/src/plugins/wp/TacSequence.mli
new file mode 100644
index 0000000000000000000000000000000000000000..51e970bdaf1083d3ec5e9fb9f0371b8b9899532d
--- /dev/null
+++ b/src/plugins/wp/TacSequence.mli
@@ -0,0 +1,29 @@
+(**************************************************************************)
+(* *)
+(* This file is part of WP plug-in of Frama-C. *)
+(* *)
+(* Copyright (C) 2007-2020 *)
+(* CEA (Commissariat a l'energie atomique et aux energies *)
+(* alternatives) *)
+(* *)
+(* you can redistribute it and/or modify it under the terms of the GNU *)
+(* Lesser General Public License as published by the Free Software *)
+(* Foundation, version 2.1. *)
+(* *)
+(* It is distributed in the hope that it will be useful, *)
+(* but WITHOUT ANY WARRANTY; without even the implied warranty of *)
+(* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the *)
+(* GNU Lesser General Public License for more details. *)
+(* *)
+(* See the GNU Lesser General Public License version 2.1 *)
+(* for more details (enclosed in the file licenses/LGPLv2.1). *)
+(* *)
+(**************************************************************************)
+
+(** Built-in Sequence Tactical (auto-registered) *)
+
+open Tactical
+
+val tactical : tactical
+
+(**************************************************************************)
diff --git a/src/plugins/wp/Tactical.ml b/src/plugins/wp/Tactical.ml
index 16e16203b0a791f60630800eb7b0c0e2520f4cb1..2cd4ff603fd859a645abfb13660e81440a0abde1 100644
--- a/src/plugins/wp/Tactical.ml
+++ b/src/plugins/wp/Tactical.ml
@@ -372,6 +372,9 @@ let rewrite ?at patterns sequent =
descr , Conditions.insert ?at step sequent
) patterns
+let condition name guard process seq =
+ ( name , (fst seq , guard) ) :: process seq
+
(* -------------------------------------------------------------------------- *)
(* --- Tactical Engines --- *)
(* -------------------------------------------------------------------------- *)
diff --git a/src/plugins/wp/Tactical.mli b/src/plugins/wp/Tactical.mli
index a1e8c042a1fdceae2d410103f57fe3ca6895d53d..320881d5c5b660ea4bf694a256c380f6806717a1 100644
--- a/src/plugins/wp/Tactical.mli
+++ b/src/plugins/wp/Tactical.mli
@@ -184,6 +184,9 @@ val rewrite : ?at:int -> (string * pred * term * term) list -> process
(** For each pattern [(descr,guard,src,tgt)] replace [src] with [tgt]
under condition [guard], inserted in position [at]. *)
+val condition : string -> pred -> process -> process
+(** Apply process, but only after proving some condition *)
+
(** {2 Tactical Plug-in} *)
class type tactical =
diff --git a/src/plugins/wp/doc/manual/wp_plugin.tex b/src/plugins/wp/doc/manual/wp_plugin.tex
index c85ce39e4a49fcb2189c3635009f6b597231acf1..aaf0e60480d3adc4ea3bf6eeafe3eff30a0d0fd8 100644
--- a/src/plugins/wp/doc/manual/wp_plugin.tex
+++ b/src/plugins/wp/doc/manual/wp_plugin.tex
@@ -532,6 +532,53 @@ This is a variant of the \texttt{Lemma} tactic dedicated to \texttt{Havoc} predi
\paragraph{Separated} Expand Separation Cases\\
This tactic decompose a \texttt{separated}$(a,n,b,m)$ predicate into its four base cases: $a$ and $b$ have different bases, $a+n \leq b$, $b+m \leq a$, and $a[0..n-1]$ and $b[0..m-1]$ overlaps. The regions are separated in the first three cases, and not separated in the overlapping case. This is kind of normal disjunctive form of the separation clause.
+
+\paragraph{Sequence} Unroll repeat-sequence operator\\
+In this section, let us use $A^n$ for the ACSL notation \lstinline{A *^ n},
+the repeat list operation, and $A \oplus l$ for the list concatenation.
+
+This tactics is used to transform $A^n$ sequences. Threes behaviors
+can be selected:
+unroll left that rewrites the list $A^n$ into $A \oplus A^{n-1}$,
+unroll right that rewrites the list $A^n$ into $A^{n-1} \oplus A$
+and unroll sum that rewrites the list $A ^{n_1 + ... + n_k}$
+into $A^{n_1} \oplus ... \oplus A^{n_k}$. For unroll left and right,
+a negative value leads to an empty list. For unroll sum, one must prove that all
+$nI$ are positive.
+
+Rule for unroll left:
+
+\[
+\TACTIC{\Delta\models\,G}{%
+\begin{array}[t]{lll}
+ \Delta[A^n\leftarrow A \oplus A^{n-1}],& n > 0 & \models G[A^n\leftarrow A \oplus A^{n-1}]\\
+ \Delta[A^n\leftarrow []],& n \leq 0 & \models G[A^n\leftarrow []]
+\end{array}
+}\]
+
+Rule for unroll right:
+
+\[
+\TACTIC{\Delta\models\,G}{%
+\begin{array}[t]{lll}
+ \Delta[A^n\leftarrow A^{n-1} \oplus A],& n > 0 & \models G[A^n\leftarrow A^{n-1} \oplus A]\\
+ \Delta[A^n\leftarrow []],& n \leq 0 & \models G[A^n\leftarrow []]
+\end{array}
+}\]
+
+Rule for unroll sum:
+
+\[
+\TACTIC{\Delta\models\,G}{%
+\begin{array}[t]{ll}
+ \Delta & \models\bigwedge_{i=1}^{k} 0 \leq n_i\\
+ &\\
+ \Delta[A^{\sum_{i=1}^{k}n_i}\leftarrow \bigoplus_{i=1}^{k} A^{n_i}] &
+ \models G[A^{\sum_{i=1}^{k}n_i}\leftarrow \bigoplus_{i=1}^{k} A^{n_i}]
+\end{array}
+}\]
+
+
\subsection{Custom Tactics and Strategies}
\label{wp-custom-tactics}
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json
new file mode 100644
index 0000000000000000000000000000000000000000..885feb947bdb3b276a90fc8d54f807ae6dd76e79
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json
@@ -0,0 +1,7 @@
+[ { "prover": "script", "verdict": "valid" },
+ { "header": "Sequence", "tactic": "Wp.sequence",
+ "params": { "seq.side": "left" },
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "(repeat a_0 n_0)", "pattern": "repeat$a$n" },
+ "children": { "Nil": [ { "prover": "qed", "verdict": "valid" } ],
+ "Unroll": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json
new file mode 100644
index 0000000000000000000000000000000000000000..75e4064cdb6eb792772488a295e01855174a6132
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json
@@ -0,0 +1,7 @@
+[ { "prover": "script", "verdict": "valid" },
+ { "header": "Sequence", "tactic": "Wp.sequence",
+ "params": { "seq.side": "right" },
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "(repeat a_0 n_0)", "pattern": "repeat$a$n" },
+ "children": { "Nil": [ { "prover": "qed", "verdict": "valid" } ],
+ "Unroll": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json
new file mode 100644
index 0000000000000000000000000000000000000000..65a87aa59ca69040135319b35d107a49d773886a
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json
@@ -0,0 +1,8 @@
+[ { "prover": "script", "verdict": "valid" },
+ { "header": "Sequence", "tactic": "Wp.sequence",
+ "params": { "seq.side": "sum" },
+ "select": { "select": "inside-goal", "occur": 0,
+ "target": "(repeat a_0 (p_0+q_0))",
+ "pattern": "repeat$a+$p$q" },
+ "children": { "Positive": [ { "prover": "qed", "verdict": "valid" } ],
+ "Unroll": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.res.oracle b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..d520e08daacf19a629295d7d3766e250e627005c
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.res.oracle
@@ -0,0 +1,14 @@
+# frama-c -wp [...]
+[kernel] Parsing tests/wp_tip/unroll.i (no preprocessing)
+[wp] Running WP plugin...
+[wp] 3 goals scheduled
+[wp] [Script] Goal typed_lemma_LEFT : Valid
+[wp] [Script] Goal typed_lemma_RIGHT : Valid
+[wp] [Script] Goal typed_lemma_SUM : Valid
+[wp] Proved goals: 3 / 3
+ Qed: 0
+ Script: 3
+------------------------------------------------------------
+ Axiomatics WP Alt-Ergo Total Success
+ Lemma - - 3 100%
+------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_tip/unroll.i b/src/plugins/wp/tests/wp_tip/unroll.i
new file mode 100644
index 0000000000000000000000000000000000000000..c3392a979882d88ac32a403217b9a24fb4d55398
--- /dev/null
+++ b/src/plugins/wp/tests/wp_tip/unroll.i
@@ -0,0 +1,31 @@
+/* run.config
+ DONTRUN:
+*/
+
+/* run.config_qualif
+ OPT: -wp-prover script,none
+ */
+
+/*@
+ lemma SUM:
+ \forall \list<integer> a;
+ \forall integer p,q;
+ 0 <= p ==> 0 <= q ==>
+ (a *^ (p+q)) == ((a *^ p) ^ (a *^ q)) ;
+*/
+
+/*@
+ lemma RIGHT:
+ \forall \list<integer> a;
+ \forall integer n;
+ 0 < n ==>
+ (a *^ n) == ((a *^ (n-1)) ^ a) ;
+*/
+
+/*@
+ lemma LEFT:
+ \forall \list<integer> a;
+ \forall integer n;
+ 0 < n ==>
+ (a *^ n) == (a ^ (a *^ (n-1))) ;
+*/