diff --git a/src/plugins/aorai/aorai_option.ml b/src/plugins/aorai/aorai_option.ml
index 1dfe1a0504a9c33546d943fe3705f79c97373bf9..c31e0137a1780c486cc446af0c5d16dca926a760 100644
--- a/src/plugins/aorai/aorai_option.ml
+++ b/src/plugins/aorai/aorai_option.ml
@@ -160,6 +160,16 @@ module Deterministic=
         let default () = false
      end)
 
+module InstrumentationHistory =
+  Int
+    (struct
+      let option_name = "-aorai-instrumentation-history"
+      let arg_name = "N"
+      let help = "the instrumentation will keep an history of the N last states"
+      let default = 0
+    end)
+
+
 let is_on () =
   not (Ltl_File.is_default () && To_Buchi.is_default () &&
        Buchi.is_default ()    && Ya.is_default () )
diff --git a/src/plugins/aorai/aorai_option.mli b/src/plugins/aorai/aorai_option.mli
index 111cf0e74ea3f7ac344cb47ffd02be462f11734c..636b793b21834faaacaa5aff35091120f5740219 100644
--- a/src/plugins/aorai/aorai_option.mli
+++ b/src/plugins/aorai/aorai_option.mli
@@ -43,6 +43,8 @@ module AddingOperationNameAndStatusInSpecification: Parameter_sig.Bool
 (** [true] if the user declares that its ya automaton is deterministic. *)
 module Deterministic: State_builder.Ref with type data = bool
 
+module InstrumentationHistory: Parameter_sig.Int
+
 val is_on : unit -> bool
 val promela_file: unit -> Filepath.Normalized.t
 val advance_abstract_interpretation: unit -> bool
diff --git a/src/plugins/aorai/aorai_utils.ml b/src/plugins/aorai/aorai_utils.ml
index 7615b72d83c5c6ba6554e5cd857ad39a0ec978ee..9d1f4b3641245817b971009f2fe89edac84339c0 100644
--- a/src/plugins/aorai/aorai_utils.ml
+++ b/src/plugins/aorai/aorai_utils.ml
@@ -1132,9 +1132,12 @@ let initGlobals root complete =
 
   mk_global_comment "//* ";
   mk_global_comment "//* States and Trans Variables";
-  if Aorai_option.Deterministic.get () then
-    mk_global_c_var_init curState (getInitialState())
-  else
+  if Aorai_option.Deterministic.get () then begin
+    mk_global_c_var_init curState (getInitialState());
+    let init = getInitialState() (* TODO a distinct initial value for history *)
+    and history = Data_for_aorai.whole_history () in
+    List.iter (fun name -> mk_global_c_var_init name init) history
+  end else
     mk_global_states_init root;
 
   if complete then begin
@@ -2120,6 +2123,20 @@ let auto_func_block generated_kf loc f st status res =
            (Const (Data_for_aorai.func_to_cenum (Kernel_function.get_name f))))
         loc
     ]
+  and stmt_history_update =
+    if Aorai_option.Deterministic.get () then
+      let history = Data_for_aorai.whole_history ()
+      and cur_state = Data_for_aorai.(get_varinfo curState) in
+      let add_stmt (src,acc) dst_name =
+        let dst = Data_for_aorai.get_varinfo dst_name in
+        let stmt = equalsStmt (Cil.var dst) (Cil.evar ~loc src) loc in
+        dst, stmt :: acc
+      in
+      snd (List.fold_left add_stmt (cur_state,[]) history)
+    else if Aorai_option.InstrumentationHistory.get () > 0 then
+      Aorai_option.fatal "history is not implemented for non-deterministic \
+                          automaton"
+    else []
   in
   let new_funcs, local_var, main_stmt =
     if Aorai_option.Deterministic.get() then
@@ -2130,7 +2147,7 @@ let auto_func_block generated_kf loc f st status res =
   let ret = [ Cil.mkStmt ~ghost:true (Cil_types.Return(None,loc)) ] in
   let res_block =
     (Cil.mkBlock
-       ( stmt_begin_list @ main_stmt @ ret))
+       ( stmt_begin_list @ stmt_history_update @ main_stmt @ ret))
   in
   res_block.blocals <- local_var;
   Aorai_option.debug ~dkey "Generated body is:@\n%a"
diff --git a/src/plugins/aorai/data_for_aorai.ml b/src/plugins/aorai/data_for_aorai.ml
index 157f44778f221d425e88170fdc2beacb164518ca..f4e4d3a64c0067ab5b408cd561c389c165609a59 100644
--- a/src/plugins/aorai/data_for_aorai.ml
+++ b/src/plugins/aorai/data_for_aorai.ml
@@ -177,7 +177,13 @@ let loopInit    = "aorai_Loop_Init"                      (* OK *)
 
 (* C variables *)
 let curState    = "aorai_CurStates"                      (* OK *)
-let curStateOld = "aorai_CurStates_old"                  (* OK *)
+let history n   = "aorai_StatesHistory_" ^ string_of_int n (* OK *)
+let whole_history () =
+  let rec aux acc n =
+    if n > 0 then aux (history n :: acc) (n - 1) else acc
+  in
+  aux [] (Aorai_option.InstrumentationHistory.get ())
+
 let curTrans    = "aorai_CurTrans"                       (* OK *)
 (*let curTransTmp = "aorai_CurTrans_tmp"                   (* OK *)*)
 let curOp       = "aorai_CurOperation"                   (* OK *)
diff --git a/src/plugins/aorai/data_for_aorai.mli b/src/plugins/aorai/data_for_aorai.mli
index 786ca7217fbe4d5d1e6e5c7b912deea6a570da71..b5869d0611776bf9d0dd2b7c443ce2587e0d4136 100644
--- a/src/plugins/aorai/data_for_aorai.mli
+++ b/src/plugins/aorai/data_for_aorai.mli
@@ -130,8 +130,9 @@ val curOpStatus  : string
 (** Name of curState C generated variable (Table of states that can be synchronized with the program) *)
 val curState     : string
 
-(** Name of curStateOld C generated variable (Last value of curState) *)
-val curStateOld  : string
+(** Name of the history variables (History of previous states) *)
+val history  : int -> string
+val whole_history  : unit -> string list
 
 (** Name of curTrans C generated variable (Last transitions that can be crossed) *)
 val curTrans     : string