diff --git a/headers/header_spec.txt b/headers/header_spec.txt
index 06b913c3cc70a0afae8ace3b73756565deca027c..49cb0ecd52f503b7811d0f57bdc3a8372397815c 100644
--- a/headers/header_spec.txt
+++ b/headers/header_spec.txt
@@ -208,7 +208,6 @@ share/libc/__fc_runtime.c: CEA_LGPL
share/libc/__fc_select.h: CEA_LGPL
share/libc/__fc_string_axiomatic.h: CEA_LGPL
share/libc/alloca.h: CEA_LGPL
-share/libc/aorai/aorai.h: CEA_LGPL
share/libc/arpa/inet.h: CEA_LGPL
share/libc/assert.c: CEA_LGPL
share/libc/assert.h: CEA_LGPL
diff --git a/share/libc/aorai/aorai.h b/share/libc/aorai/aorai.h
deleted file mode 100644
index b2f5eeb733fa6beb109b4a54797214d8a201e79e..0000000000000000000000000000000000000000
--- a/share/libc/aorai/aorai.h
+++ /dev/null
@@ -1,33 +0,0 @@
-/**************************************************************************/
-/* */
-/* This file is part of Frama-C. */
-/* */
-/* Copyright (C) 2007-2020 */
-/* CEA (Commissariat à l'énergie atomique et aux énergies */
-/* 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). */
-/* */
-/**************************************************************************/
-
-#ifndef __FC_AORAI
-#define __FC_AORAI
-
-/*@ ghost extern int aorai_CurStates; */
-/*@ ghost extern int aorai_StatesHistory1; */
-/*@ ghost extern int aorai_StatesHistory2; */
-/*@ ghost extern int aorai_StatesHistory3; */
-/*@ ghost extern int aorai_StatesHistory4; */
-
-
-#endif
diff --git a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
index 0a57509c1c6f2901ddc29e64157f7124e69fc349..1dc6823676ef7ee36ab009e4916d0cfc77a8ea33 100644
--- a/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/serial.res.oracle
@@ -1,8 +1,8 @@
[kernel] Parsing tests/ya/serial.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/ya/serial.c:81: Warning:
+[kernel:typing:implicit-function-declaration] tests/ya/serial.c:79: Warning:
Calling undeclared function Frama_C_show_aorai_state. Old style K&R code?
[aorai] Welcome to the Aorai plugin
-[kernel:annot:missing-spec] tests/ya/serial.c:45: Warning:
+[kernel:annot:missing-spec] tests/ya/serial.c:43: Warning:
Neither code nor specification for function Frama_C_show_aorai_state, generating default assigns from the prototype
[eva] Analyzing a complete application starting at main
[eva] Computing initial state
@@ -21,28 +21,28 @@
aorai_StatesHistory_1 ∈ {19}
aorai_StatesHistory_2 ∈ {19}
[eva] using specification for function Frama_C_interval
-[eva] tests/ya/serial.c:47: starting to merge loop iterations
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 100 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 300 states
-[aorai] tests/ya/serial.c:81: Wait1 <- Wait1 <- Complete
-[aorai] tests/ya/serial.c:81: Error <- Error <- Complete
-[aorai] tests/ya/serial.c:81: Complete <- Complete <- Complete
-[aorai] tests/ya/serial.c:81: Wait1 <- Wait1 <- Complete
-[aorai] tests/ya/serial.c:81: Error <- Error <- Complete
-[aorai] tests/ya/serial.c:81: Complete <- Complete <- Complete
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 500 states
-[eva:alarm] tests/ya/serial.c:54: Warning:
+[eva] tests/ya/serial.c:45: starting to merge loop iterations
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 100 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 300 states
+[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
+[aorai] tests/ya/serial.c:79: Wait1 <- Wait1 <- Complete
+[aorai] tests/ya/serial.c:79: Error <- Error <- Complete
+[aorai] tests/ya/serial.c:79: Complete <- Complete <- Complete
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 500 states
+[eva:alarm] tests/ya/serial.c:52: Warning:
accessing uninitialized left-value. assert \initialized(&status);
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 700 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 900 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1200 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1500 states
-[aorai] tests/ya/serial.c:81: Error <- Error <- Error
-[aorai] tests/ya/serial.c:81: Error <- Error <- Error
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1700 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 1900 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 2000 states
-[eva] tests/ya/serial.c:52: Trace partitioning superposing up to 2100 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 700 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 900 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1200 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1500 states
+[aorai] tests/ya/serial.c:79: Error <- Error <- Error
+[aorai] tests/ya/serial.c:79: Error <- Error <- Error
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1700 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 1900 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2000 states
+[eva] tests/ya/serial.c:50: Trace partitioning superposing up to 2100 states
[eva] done for function main
[eva] ====== VALUES COMPUTED ======
[eva:final-states] Values at end of function input_data_post_func:
diff --git a/src/plugins/aorai/tests/ya/serial.c b/src/plugins/aorai/tests/ya/serial.c
index 2e8b8bc3d454dae9dd7e57f0329f3ea6a78a4130..8afcc7533fb16ccfc3726a32c5d95267a0f8a2bc 100644
--- a/src/plugins/aorai/tests/ya/serial.c
+++ b/src/plugins/aorai/tests/ya/serial.c
@@ -3,8 +3,6 @@
*/
#include "__fc_builtin.h"
-#include "aorai/aorai.h"
-
/*@ assigns \result \from \nothing;
ensures 0 <= \result < 0x100; */