diff --git a/src/plugins/aorai/aorai_eva_analysis.enabled.ml b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
index 007c6ed88fe5764955a3cdd7f912559e6f2548b2..5b481c60b1d80bc9c1132323a5f88d2ea80b63ae 100644
--- a/src/plugins/aorai/aorai_eva_analysis.enabled.ml
+++ b/src/plugins/aorai/aorai_eva_analysis.enabled.ml
@@ -34,10 +34,19 @@ let show_aorai_variable state fmt var_name =
        Z.Overflow | Not_found ->
     Format.fprintf fmt "?"
 
-let builtin_show_aorai_state state _args =
+let show_val fmt (expr, v, _) =
+  Format.fprintf fmt "%a in %a"
+    Printer.pp_exp expr
+    (Cvalue.V.pretty_typ (Some (Cil.typeOf expr))) v
+
+let builtin_show_aorai_state state args =
   let history = Data_for_aorai.(curState :: (whole_history ())) in
   Aorai_option.result ~current:true "@[<hv>%a@]"
     (Pretty_utils.pp_list ~sep:" <- " (show_aorai_variable state)) history;
+  if args <> [] then begin
+    Aorai_option.result ~current:true "@[<hv>%a@]"
+      (Pretty_utils.pp_list ~sep:"," show_val) args
+  end;
   (* Return value : returns nothing, changes nothing *)
   {
     Value_types.c_values = [None, state];
@@ -46,8 +55,14 @@ let builtin_show_aorai_state state _args =
     c_cacheable = Value_types.Cacheable;
   }
 
+let show_aorai_state = "Frama_C_show_aorai_state"
+
+let () =
+  Cil_builtins.add_custom_builtin
+    (fun () -> (show_aorai_state,Cil.voidType,[],true))
+
 let () =
-  !Db.Value.register_builtin "Frama_C_show_aorai_state" builtin_show_aorai_state
+  !Db.Value.register_builtin show_aorai_state builtin_show_aorai_state
 
 let add_slevel_annotation vi kind =
   match kind with
diff --git a/tests/libc/oracle/fc_libc.2.res.oracle b/tests/libc/oracle/fc_libc.2.res.oracle
index 852a3378808b5fd9471ec06cf612b0c65da0e7eb..b1e1247a43669f03d504de710fa2a4b5337ce754 100644
--- a/tests/libc/oracle/fc_libc.2.res.oracle
+++ b/tests/libc/oracle/fc_libc.2.res.oracle
@@ -42,7 +42,6 @@ skipping share/libc/__fc_machdep_linux_shared.h
 [kernel] Parsing share/libc/__fc_select.h (with preprocessing)
 [kernel] Parsing share/libc/__fc_string_axiomatic.h (with preprocessing)
 [kernel] Parsing share/libc/alloca.h (with preprocessing)
-[kernel] Parsing share/libc/aorai/aorai.h (with preprocessing)
 [kernel] Parsing share/libc/arpa/inet.h (with preprocessing)
 [kernel] Parsing share/libc/assert.h (with preprocessing)
 [kernel] Parsing share/libc/byteswap.h (with preprocessing)
diff --git a/tests/libc/oracle/fc_libc.5.res.oracle b/tests/libc/oracle/fc_libc.5.res.oracle
index 3c89feea03b4a5c923cf5dcf11cf391b647c4a2b..73dac90425a73c971fb285476320f30bc36be7d1 100644
--- a/tests/libc/oracle/fc_libc.5.res.oracle
+++ b/tests/libc/oracle/fc_libc.5.res.oracle
@@ -1,2 +1 @@
 #include "__fc_integer.h"
-#include "aorai/aorai.h"
diff --git a/tests/syntax/oracle/bts1553_2.res.oracle b/tests/syntax/oracle/bts1553_2.res.oracle
index 9293259fe565811c4e9f7f6dedc355b38faa4288..93dacee514969b19d8bc20ff47fcaffdd2a4c526 100644
--- a/tests/syntax/oracle/bts1553_2.res.oracle
+++ b/tests/syntax/oracle/bts1553_2.res.oracle
@@ -5,6 +5,8 @@
   struct a {
      int b ;
   };
+  /* compiler builtin: 
+     void Frama_C_show_aorai_state(...);   */
   /* compiler builtin: 
      __builtin_va_list __builtin_next_arg(void);   */
   /* compiler builtin: 
@@ -40,6 +42,8 @@
   struct a {
      int b ;
   };
+  /* compiler builtin: 
+     void Frama_C_show_aorai_state(...);   */
   /* compiler builtin: 
      __builtin_va_list __builtin_next_arg(void);   */
   /* compiler builtin: 
diff --git a/tests/syntax/oracle/check_builtin_bts1440.res.oracle b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
index 510a8f2b3ab41a3c39cd5c26cc41c8703528b9e1..f81e5813ccc1c324160bc8600bf6e042c3e3fbbd 100644
--- a/tests/syntax/oracle/check_builtin_bts1440.res.oracle
+++ b/tests/syntax/oracle/check_builtin_bts1440.res.oracle
@@ -2,6 +2,8 @@
 [kernel:file:print-one] 
   result of parsing tests/syntax/check_builtin_bts1440.i:
   /* Generated by Frama-C */
+  void Frama_C_show_aorai_state(...);
+  
   void __builtin__Exit(int);
   
   int __builtin___fprintf_chk(void *, int, char const * , ...);
diff --git a/tests/syntax/oracle/static_formals_1.res.oracle b/tests/syntax/oracle/static_formals_1.res.oracle
index 94353adf96ce8cb00b16e417c838e314206f2554..f3dc98b3d3003fb066ecc0db86d86140b90ce85c 100644
--- a/tests/syntax/oracle/static_formals_1.res.oracle
+++ b/tests/syntax/oracle/static_formals_1.res.oracle
@@ -1,24 +1,24 @@
 [kernel] Parsing tests/syntax/static_formals_1.c (with preprocessing)
 [kernel] Parsing tests/syntax/static_formals_2.c (with preprocessing)
 /* Generated by Frama-C */
-/*@ requires /* vid:25, lvid:25 */x < 10; */
-static int /* vid:58 */f(int /* vid:25, lvid:25 */x);
+/*@ requires /* vid:26, lvid:26 */x < 10; */
+static int /* vid:60 */f(int /* vid:26, lvid:26 */x);
 
-int /* vid:30 */g(void)
+int /* vid:31 */g(void)
 {
-  int /* vid:31 */tmp;
-  /* vid:31 */tmp = /* vid:58 */f(4);
-  return /* vid:31 */tmp;
+  int /* vid:32 */tmp;
+  /* vid:32 */tmp = /* vid:60 */f(4);
+  return /* vid:32 */tmp;
 }
 
-/*@ requires /* vid:53, lvid:53 */x < 10; */
-static int /* vid:59 */f_0(int /* vid:53, lvid:53 */x);
+/*@ requires /* vid:55, lvid:55 */x < 10; */
+static int /* vid:61 */f_0(int /* vid:55, lvid:55 */x);
 
-int /* vid:56 */h(void)
+int /* vid:58 */h(void)
 {
-  int /* vid:57 */tmp;
-  /* vid:57 */tmp = /* vid:59 */f_0(6);
-  return /* vid:57 */tmp;
+  int /* vid:59 */tmp;
+  /* vid:59 */tmp = /* vid:61 */f_0(6);
+  return /* vid:59 */tmp;
 }