diff --git a/src/plugins/aorai/Makefile.in b/src/plugins/aorai/Makefile.in
index 0e0b5764a306b8e12d5c390bd29a14cff1c5db8f..5b8af2dea1993db71ab6ee47ef7f25de6837273a 100644
--- a/src/plugins/aorai/Makefile.in
+++ b/src/plugins/aorai/Makefile.in
@@ -73,14 +73,14 @@ PLUGIN_DISTRIB_EXTERNAL:= Makefile.in configure.ac configure
PLUGIN_HAS_EXT_DOC:=no # [JS 2010/07/28] was 'yes'
# but prevent 'make src-distrib to work
-# if ltltoba is not present, do not attempt to run any test.
-ifneq (@HAS_LTLTOBA@,yes)
-PLUGIN_NO_TEST:=yes
-PLUGIN_NO_DEFAULT_TEST:=yes
+# aorai_ya can always be run
+PLUGIN_TESTS_DIRS:=aorai_ya
+
+ifeq (@HAS_LTLTOBA@,yes)
+PLUGIN_TESTS_DIRS+=aorai_ltl
endif
-PLUGIN_TESTS_DIRS:=aorai
-PLUGIN_TESTS_LIB:=$(PLUGIN_DIR)/tests/Aorai_test.ml $(PLUGIN_DIR)/tests/aorai/name_projects.ml
+PLUGIN_TESTS_LIB:=$(PLUGIN_DIR)/tests/Aorai_test.ml $(PLUGIN_DIR)/tests/aorai_ya/name_projects.ml
include $(FRAMAC_SHARE)/Makefile.dynamic
@@ -101,7 +101,7 @@ $(Aorai_DIR)/tests/test_config_prove: \
$(SED) -e 's!@AORAI_WP_SHARE@!$(AORAI_WP_SHARE)!' $< > $@
$(CHMOD_RO) $@
-Aorai_DEFAULT_TESTS: $(Aorai_DIR)/tests/Aorai_test.cmxs $(Aorai_DIR)/tests/Aorai_test.cmo $(Aorai_DIR)/tests/aorai/name_projects.cmxs $(Aorai_DIR)/tests/aorai/name_projects.cmo
+Aorai_DEFAULT_TESTS: $(Aorai_DIR)/tests/Aorai_test.cmxs $(Aorai_DIR)/tests/Aorai_test.cmo $(Aorai_DIR)/tests/aorai_ya/name_projects.cmxs $(Aorai_DIR)/tests/aorai_ya/name_projects.cmo
# Regenerating the Makefile on need
diff --git a/src/plugins/aorai/tests/aorai/bts1289.i b/src/plugins/aorai/tests/aorai/bts1289.i
deleted file mode 100644
index 9cf6122636bc60413140b772f022128558bf0e00..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/tests/aorai/bts1289.i
+++ /dev/null
@@ -1,14 +0,0 @@
-/* run.config*
- OPT: -aorai-automata tests/aorai/bts1289.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-automata tests/aorai/bts1289-2.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- */
-
-void a(void) {}
-
-void main(void)
-{
- //@ loop assigns i;
- for (int i=0; i<10; ++i)
- a();
-}
-
diff --git a/src/plugins/aorai/tests/aorai/formals.i b/src/plugins/aorai/tests/aorai/formals.i
deleted file mode 100644
index 6ff8527a52c3936f402df299670cf6d0a88eee17..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/tests/aorai/formals.i
+++ /dev/null
@@ -1,9 +0,0 @@
-/* run.config*
-OPT: -aorai-automata tests/aorai/formals.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-*/
-
-int f(int x) { return x; }
-
-int g(int y) { return y; }
-
-int main() { f(1); g(2); }
diff --git a/src/plugins/aorai/tests/aorai/generate_assigns_bts1290.i b/src/plugins/aorai/tests/aorai/generate_assigns_bts1290.i
deleted file mode 100644
index 81fb7f1a5144bd6d748f6de008bee2babf8801bf..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/tests/aorai/generate_assigns_bts1290.i
+++ /dev/null
@@ -1,9 +0,0 @@
-/* run.config*
- OPT: -aorai-automata tests/aorai/generate_assigns_bts1290.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- */
-void main(void)
-{
- //@ loop assigns i;
- for (int i=0; i<10; ++i)
- ;
-}
diff --git a/src/plugins/aorai/tests/aorai/hoare_seq.i b/src/plugins/aorai/tests/aorai/hoare_seq.i
deleted file mode 100644
index 39e87b49e027ae26183d5a7b785703bd6373a3ac..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/tests/aorai/hoare_seq.i
+++ /dev/null
@@ -1,14 +0,0 @@
-/* run.config*
-OPT: -aorai-automata tests/aorai/hoare_seq.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-*/
-
-void f(void) { }
-
-/*@ behavior bhv:
- assumes c > 0;
- ensures \result == 0;
-*/
-int main(int c) {
- if (c <= 0) { f (); }
- return 0;
-}
diff --git a/src/plugins/aorai/tests/aorai/not_prm.i b/src/plugins/aorai/tests/aorai/not_prm.i
deleted file mode 100644
index 3eb7b631a64e579a377daadfbfb3151ef3352ba7..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/tests/aorai/not_prm.i
+++ /dev/null
@@ -1,7 +0,0 @@
-/* run.config*
- OPT: -aorai-automata tests/aorai/not_prm.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-*/
-
-int f(int x) {
- return x;
-}
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/monostate.res.oracle b/src/plugins/aorai/tests/aorai/oracle_prove/monostate.res.oracle
deleted file mode 100644
index fcbb126e71536b5d56700432953494a2ce09929a..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/tests/aorai/oracle_prove/monostate.res.oracle
+++ /dev/null
@@ -1 +0,0 @@
-[kernel] Parsing tests/aorai/monostate.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_factorial2.res.oracle b/src/plugins/aorai/tests/aorai/oracle_prove/test_factorial2.res.oracle
deleted file mode 100644
index 78ecfbfbfa1800fbcbb0f176e08fd47109ba5614..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_factorial2.res.oracle
+++ /dev/null
@@ -1,4 +0,0 @@
-[kernel] Parsing tests/aorai/test_factorial2.c (with preprocessing)
-[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_factorial2_0.i (no preprocessing)
-[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/other.c b/src/plugins/aorai/tests/aorai/other.c
deleted file mode 100644
index 0d0eb41b0a17dafe3d6a52a4507f25e69b585c34..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/tests/aorai/other.c
+++ /dev/null
@@ -1,17 +0,0 @@
-/* run.config*
- OPT: -aorai-automata tests/aorai/other.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-*/
-
-int x=0;
-
-void f (void) { x=3; }
-
-void g (void) { x=4; }
-
-int main () {
- f();
- g();
- f();
- g();
- return x;
-}
diff --git a/src/plugins/aorai/tests/aorai/result_prove/.empty b/src/plugins/aorai/tests/aorai/result_prove/.empty
deleted file mode 100644
index e69de29bb2d1d6434b8b29ae775ad8c2e48c5391..0000000000000000000000000000000000000000
diff --git a/src/plugins/aorai/tests/aorai/seq.i b/src/plugins/aorai/tests/aorai/seq.i
deleted file mode 100644
index f05fcf7bbe983c07df80721f6f11b4d9f6053b2a..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/tests/aorai/seq.i
+++ /dev/null
@@ -1,14 +0,0 @@
-/* run.config*
- OPT: -aorai-automata tests/aorai/seq.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- */
-
-void f() { }
-
-void g() { }
-
-int main(int c) {
- if (c) f();
- g();
- if (c) g();
- return 0;
-}
diff --git a/src/plugins/aorai/tests/aorai/single_call.i b/src/plugins/aorai/tests/aorai/single_call.i
deleted file mode 100644
index 03124cf5c9710fbcd9c0dd66c3923ae0b913683b..0000000000000000000000000000000000000000
--- a/src/plugins/aorai/tests/aorai/single_call.i
+++ /dev/null
@@ -1,5 +0,0 @@
-/* run.config*
- OPT: -aorai-automata tests/aorai/single_call.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
-*/
-
-int main () {}
diff --git a/src/plugins/aorai/tests/aorai/call_tree.c b/src/plugins/aorai/tests/aorai_ltl/call_tree.c
similarity index 100%
rename from src/plugins/aorai/tests/aorai/call_tree.c
rename to src/plugins/aorai/tests/aorai_ltl/call_tree.c
diff --git a/src/plugins/aorai/tests/aorai/call_tree.ltl b/src/plugins/aorai/tests/aorai_ltl/call_tree.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/call_tree.ltl
rename to src/plugins/aorai/tests/aorai_ltl/call_tree.ltl
diff --git a/src/plugins/aorai/tests/aorai/goto.c b/src/plugins/aorai/tests/aorai_ltl/goto.c
similarity index 72%
rename from src/plugins/aorai/tests/aorai/goto.c
rename to src/plugins/aorai/tests/aorai_ltl/goto.c
index 74c4a0c9ffc4e8b23c4adc900d401ffc3fcb6b85..ccd31e28dbe2344aa5c4fee8254898945fcfa29c 100644
--- a/src/plugins/aorai/tests/aorai/goto.c
+++ b/src/plugins/aorai/tests/aorai_ltl/goto.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/goto.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/aorai/goto.ltl b/src/plugins/aorai/tests/aorai_ltl/goto.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/goto.ltl
rename to src/plugins/aorai/tests/aorai_ltl/goto.ltl
diff --git a/src/plugins/aorai/tests/aorai/oracle/goto.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/goto.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/goto.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/goto.res.oracle
index 4fbc7da4bc899a5ac4d94b6fdda4afa1694d72de..8b7b7b0a0d808b69edc11ad02f4aefedf27e50b4 100644
--- a/src/plugins/aorai/tests/aorai/oracle/goto.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/goto.res.oracle
@@ -1,6 +1,6 @@
-[kernel] Parsing tests/aorai/goto.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/goto.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[aorai] tests/aorai/goto.c:28: Warning:
+[aorai] tests/aorai_ltl/goto.c:28: Warning:
Call to opc does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_goto_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_boucle.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/test_boucle.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle.res.oracle
index 9a56e5059141c412172fb9ae3fa460bb37851880..d75adfbc5e5adbdb6129a99284c5158c1df92e64 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle.res.oracle
@@ -1,5 +1,5 @@
-[kernel] Parsing tests/aorai/test_boucle.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/aorai/test_boucle.c:16: Warning:
+[kernel] Parsing tests/aorai_ltl/test_boucle.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/aorai_ltl/test_boucle.c:16: Warning:
Calling undeclared function call_to_an_undefined_function. Old style K&R code?
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_boucle1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle1.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_boucle1.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle1.res.oracle
index df9bd42ac2648170ce8e13f89b9cc3d44ab6ef18..2bf7be9ad507d609b9aba915153e8c40db855a7b 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_boucle1.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_boucle1.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle1_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_boucle2.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle2.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_boucle2.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle2.res.oracle
index 22b1adb03b4f7da3929240d53bab9b59e6ab176f..ce25f46ed9e9ecbef85be7fe724af1ee488c5a9c 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_boucle2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_boucle2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle2_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_boucle3.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle3.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_boucle3.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle3.res.oracle
index 8b3518d3db8a3cb2bcc22db417f4549797392789..4e2b603ec5833b8091fc4ba8b1b30ea012cca67b 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_boucle3.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_boucle3.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_boucle3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle3_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_factorial.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_factorial.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_factorial.res.oracle
index ceb7709726c121a7f69a5bbc8247be0be7402c2d..68238aef16a83db606409ddf834c90d7a23bb28b 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_factorial.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_factorial.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_factorial.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_factorial_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_recursion1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion1.res.oracle
similarity index 97%
rename from src/plugins/aorai/tests/aorai/oracle/test_recursion1.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion1.res.oracle
index c2bd185f1366ca54eb563f5dfbc820490d2fce39..3c998970b026be782c5dee0a3d63d83a87e0f035 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] Parsing tests/aorai/test_recursion1.c (with preprocessing)
-[kernel] tests/aorai/test_recursion1.c:21: Warning:
+[kernel] Parsing tests/aorai_ltl/test_recursion1.c (with preprocessing)
+[kernel] tests/aorai_ltl/test_recursion1.c:21: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_recursion1.c:42: Warning:
+[kernel] tests/aorai_ltl/test_recursion1.c:42: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_recursion1.c:54: Warning:
+[kernel] tests/aorai_ltl/test_recursion1.c:54: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion1_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.0.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_recursion2.0.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.0.res.oracle
index 06415a77d5fc0015f312d5fdbff3816f966bf442..c022dfa8dcacf2851c6bb4a3722d48e9bedc8060 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_recursion2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion2_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.1.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_recursion2.1.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.1.res.oracle
index f7476480b9e0afec0b414d38e8d41106750e61c2..54106258b48bd381d9e66a9305e730782ca15216 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_recursion2.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_recursion2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion2_1.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_switch2.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch2.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_switch2.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_switch2.res.oracle
index 81a8063b0a89f5ae9f35f66dd9b94c13774662dc..cf8da9996a690b3628d39c46fbacbcb0f38f8895 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch2.res.oracle
@@ -1,8 +1,8 @@
-[kernel] Parsing tests/aorai/test_switch2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[aorai] tests/aorai/test_switch2.c:34: Warning:
+[aorai] tests/aorai_ltl/test_switch2.c:34: Warning:
Call to opc not conforming to automaton (post-cond). Assuming it is on a dead path
-[aorai] tests/aorai/test_switch2.c:23: Warning:
+[aorai] tests/aorai_ltl/test_switch2.c:23: Warning:
Call to opc not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing /tmp/aorai_test_switch2_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_switch3.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_switch3.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3.res.oracle
index d21f9f44bf7cdcd0d6f2fb6909ae487cf131a084..231b350ca48c16279500ec0d3bddba4572480690 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_switch3.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_switch3_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_et_recursion.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/test_switch3_et_recursion.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_et_recursion.res.oracle
index 14157f96c419376155b697c5442f360bbddf5d50..3675b0bbde05fe61d8bddeb093e87c3ba9f01247 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_et_recursion.res.oracle
@@ -1,6 +1,6 @@
-[kernel] Parsing tests/aorai/test_switch3_et_recursion.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3_et_recursion.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[aorai] tests/aorai/test_switch3_et_recursion.c:26: Warning:
+[aorai] tests/aorai_ltl/test_switch3_et_recursion.c:26: Warning:
Call to countOne does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_test_switch3_et_recursion_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_switch3_if.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_if.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_switch3_if.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_if.res.oracle
index 9f10f0b8669625d2a83dcb82c929cf63e94d592e..6c2693aa58d0b260012100dca1b53d09bff68f02 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_if.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_switch3_if.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3_if.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_switch3_if_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_switch3_return.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_return.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_switch3_return.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_return.res.oracle
index 79aae782b2d78024cf2e4e2a15d19c52b1ab871b..f3a55fc5f091fd8ff0e6861695b5800bef91b4cc 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle/test_switch3_return.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_switch3_return.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3_return.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_switch3_return_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/goto.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/goto.res.oracle
similarity index 74%
rename from src/plugins/aorai/tests/aorai/oracle_prove/goto.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/goto.res.oracle
index 90d513137afe2ca3fd22d5721c2fc1cb28da8c66..616ce9f00553b51ef6c8881e3f5165116e8e457a 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/goto.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/goto.res.oracle
@@ -1,6 +1,6 @@
-[kernel] Parsing tests/aorai/goto.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/goto.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[aorai] tests/aorai/goto.c:28: Warning:
+[aorai] tests/aorai_ltl/goto.c:28: Warning:
Call to opc does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_goto_0.i (no preprocessing)
[wp] /tmp/aorai_goto_0.i:4: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle.res.oracle
similarity index 71%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_boucle.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle.res.oracle
index 1e1cc8acb149b69e62719f05364e2b4059a5ed16..d43ee66898a6a0870356373cd283d102024187a9 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle.res.oracle
@@ -1,5 +1,5 @@
-[kernel] Parsing tests/aorai/test_boucle.c (with preprocessing)
-[kernel:typing:implicit-function-declaration] tests/aorai/test_boucle.c:16: Warning:
+[kernel] Parsing tests/aorai_ltl/test_boucle.c (with preprocessing)
+[kernel:typing:implicit-function-declaration] tests/aorai_ltl/test_boucle.c:16: Warning:
Calling undeclared function call_to_an_undefined_function. Old style K&R code?
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle1.res.oracle
similarity index 83%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_boucle1.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle1.res.oracle
index ea51c03c1194f8e4cc201c32a0eaff1520a0d1b4..be9bc110e5eeb5962503050a78c8eea4c41440a2 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_boucle1.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_boucle1.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle1_0.i (no preprocessing)
[wp] /tmp/aorai_test_boucle1_0.i:3: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle2.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle2.res.oracle
similarity index 76%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_boucle2.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle2.res.oracle
index c92dd0a548ef141e82706a317fde2e7d7218f18b..68ab6eeb39b5e988d6299c772e0680d87fe9bf18 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_boucle2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_boucle2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle2_0.i (no preprocessing)
[wp] /tmp/aorai_test_boucle2_0.i:4: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle3.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle3.res.oracle
similarity index 76%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_boucle3.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle3.res.oracle
index ecc13c24f91ff2f21bb18d2f2312270bc174735a..0da9c1d93facae9b856c51349d11f136e5f56d3b 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_boucle3.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_boucle3.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_boucle3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle3_0.i (no preprocessing)
[wp] /tmp/aorai_test_boucle3_0.i:4: Warning:
diff --git a/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_factorial.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_factorial.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..ccb09c7d5a6177d9dd78b1d61563325e7de82611
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_factorial.res.oracle
@@ -0,0 +1,4 @@
+[kernel] Parsing tests/aorai_ltl/test_factorial.c (with preprocessing)
+[aorai] Welcome to the Aorai plugin
+[kernel] Parsing /tmp/aorai_test_factorial_0.i (no preprocessing)
+[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion1.res.oracle
similarity index 69%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_recursion1.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion1.res.oracle
index d635246be991db1aaf2daf921e81e7affdc2b633..bbd07a1eb1d3003bc8e907182be0a70aa4f635c0 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion1.res.oracle
@@ -1,9 +1,9 @@
-[kernel] Parsing tests/aorai/test_recursion1.c (with preprocessing)
-[kernel] tests/aorai/test_recursion1.c:21: Warning:
+[kernel] Parsing tests/aorai_ltl/test_recursion1.c (with preprocessing)
+[kernel] tests/aorai_ltl/test_recursion1.c:21: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_recursion1.c:42: Warning:
+[kernel] tests/aorai_ltl/test_recursion1.c:42: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_recursion1.c:54: Warning:
+[kernel] tests/aorai_ltl/test_recursion1.c:54: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion1_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.0.res.oracle
similarity index 79%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_recursion2.0.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.0.res.oracle
index 1bf5237ee0b0253f2bd01d12432dd3c1c0b77553..44eb148e42acc40de7891e1de3e2f30c63ef84ee 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_recursion2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion2_0.i (no preprocessing)
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.1.res.oracle
similarity index 79%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_recursion2.1.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.1.res.oracle
index 6782e2af71e1129dc7238ac11b8f4facbc8ab0b4..e6b17cbbc0bcf95c66ef24a36855489cc7d03a3e 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_recursion2.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_recursion2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_recursion2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion2_1.i (no preprocessing)
[wp] Warning: No definition for 'string_len' interpreted as reads nothing
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch2.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch2.res.oracle
similarity index 69%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_switch2.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch2.res.oracle
index 93f710b0f1ac3217e43d52feac9b3774b07c657a..697d945d96f427fa14aeaac9ee63d0596700a325 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch2.res.oracle
@@ -1,8 +1,8 @@
-[kernel] Parsing tests/aorai/test_switch2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[aorai] tests/aorai/test_switch2.c:34: Warning:
+[aorai] tests/aorai_ltl/test_switch2.c:34: Warning:
Call to opc not conforming to automaton (post-cond). Assuming it is on a dead path
-[aorai] tests/aorai/test_switch2.c:23: Warning:
+[aorai] tests/aorai_ltl/test_switch2.c:23: Warning:
Call to opc not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing /tmp/aorai_test_switch2_0.i (no preprocessing)
[wp] /tmp/aorai_test_switch2_0.i:4: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3.res.oracle
similarity index 65%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_switch3.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3.res.oracle
index 18083a07f97a4ae9788647aea229ab95e6a91295..bf08eea3748c0b063dcb073dc3935ef15ab3f1ce 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_switch3.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_switch3_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_et_recursion.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_et_recursion.res.oracle
similarity index 61%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_et_recursion.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_et_recursion.res.oracle
index f8cb4d8f76544eebb3e58cf05a32f8c19a69dad5..09beb110d3a22cad15eeeaf061f6d28ae9c69983 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_et_recursion.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_et_recursion.res.oracle
@@ -1,6 +1,6 @@
-[kernel] Parsing tests/aorai/test_switch3_et_recursion.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3_et_recursion.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[aorai] tests/aorai/test_switch3_et_recursion.c:26: Warning:
+[aorai] tests/aorai_ltl/test_switch3_et_recursion.c:26: Warning:
Call to countOne does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_test_switch3_et_recursion_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_if.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_if.res.oracle
similarity index 65%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_if.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_if.res.oracle
index adfb3aca7b5b77fb780ba60c8198b2b7e4152d35..87f8f5e09ae03a0bf5f6eec2cbad8bea9110c8bb 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_if.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_switch3_if.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3_if.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_switch3_if_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_return.res.oracle b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_return.res.oracle
similarity index 64%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_return.res.oracle
rename to src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_return.res.oracle
index 68bbfec82cc9b42f63eab4c70eba89ba72d0158d..79655160142ad3f1450763ed74c7720dcccae49a 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ltl/oracle_prove/test_switch3_return.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_switch3_return.c (with preprocessing)
+[kernel] Parsing tests/aorai_ltl/test_switch3_return.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_switch3_return_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/test_boucle.c b/src/plugins/aorai/tests/aorai_ltl/test_boucle.c
similarity index 69%
rename from src/plugins/aorai/tests/aorai/test_boucle.c
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle.c
index 5da0acccb4c9bdfc9eeb611d73b3215b449dd384..72cf5e78ac931fa05a5a21be18a1777112e6e8e2 100644
--- a/src/plugins/aorai/tests/aorai/test_boucle.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_boucle.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_boucle.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/*@ requires \true;
diff --git a/src/plugins/aorai/tests/aorai/test_boucle.ltl b/src/plugins/aorai/tests/aorai_ltl/test_boucle.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_boucle.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_boucle1.c b/src/plugins/aorai/tests/aorai_ltl/test_boucle1.c
similarity index 92%
rename from src/plugins/aorai/tests/aorai/test_boucle1.c
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle1.c
index a27cc68936407559d626119be9953f6555d545ef..0245ffedcfdfe67aad9a8d9610159c9a3313b0e8 100644
--- a/src/plugins/aorai/tests/aorai/test_boucle1.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_boucle1.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_boucle1.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int cpt=3;
diff --git a/src/plugins/aorai/tests/aorai/test_boucle1.ltl b/src/plugins/aorai/tests/aorai_ltl/test_boucle1.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_boucle1.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle1.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_boucle2.c b/src/plugins/aorai/tests/aorai_ltl/test_boucle2.c
similarity index 87%
rename from src/plugins/aorai/tests/aorai/test_boucle2.c
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle2.c
index 818bf517667a0d33ff29d1fbb15f2e3cba8fa167..9d4cf3a9aff3c018e3739a253578cdcfb92eea5e 100644
--- a/src/plugins/aorai/tests/aorai/test_boucle2.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_boucle2.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_boucle2.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/aorai/test_boucle2.ltl b/src/plugins/aorai/tests/aorai_ltl/test_boucle2.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_boucle2.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle2.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_boucle3.c b/src/plugins/aorai/tests/aorai_ltl/test_boucle3.c
similarity index 87%
rename from src/plugins/aorai/tests/aorai/test_boucle3.c
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle3.c
index 07a59e0f5250efef052332f948638e2f16b1c9fd..6c93a4202649a24dff714ef33906252a84b74704 100644
--- a/src/plugins/aorai/tests/aorai/test_boucle3.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_boucle3.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_boucle3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_boucle3.ltl b/src/plugins/aorai/tests/aorai_ltl/test_boucle3.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_boucle3.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_boucle3.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_factorial.c b/src/plugins/aorai/tests/aorai_ltl/test_factorial.c
similarity index 91%
rename from src/plugins/aorai/tests/aorai/test_factorial.c
rename to src/plugins/aorai/tests/aorai_ltl/test_factorial.c
index da1305fee66feb2d339933265208e3a4a966048d..6a429a55e31de0a06be227ffd9ca72d1fb4770ea 100644
--- a/src/plugins/aorai/tests/aorai/test_factorial.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_factorial.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_factorial.ltl -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_factorial.ltl b/src/plugins/aorai/tests/aorai_ltl/test_factorial.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_factorial.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_factorial.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_recursion1.c b/src/plugins/aorai/tests/aorai_ltl/test_recursion1.c
similarity index 91%
rename from src/plugins/aorai/tests/aorai/test_recursion1.c
rename to src/plugins/aorai/tests/aorai_ltl/test_recursion1.c
index 64d448142d1fbe53e084ebeb23941b362337e9de..ee0968101b1a776f5b232d5740d4ae4e2c568f7e 100644
--- a/src/plugins/aorai/tests/aorai/test_recursion1.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_recursion1.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_recursion1.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_recursion1.ltl b/src/plugins/aorai/tests/aorai_ltl/test_recursion1.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_recursion1.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_recursion1.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_recursion2.c b/src/plugins/aorai/tests/aorai_ltl/test_recursion2.c
similarity index 91%
rename from src/plugins/aorai/tests/aorai/test_recursion2.c
rename to src/plugins/aorai/tests/aorai_ltl/test_recursion2.c
index dcbeddd090c3b7a144cb2b6ad98e2f3b8b627849..a13c39b9f887df7af32c52fa0f2a142e992478cd 100644
--- a/src/plugins/aorai/tests/aorai/test_recursion2.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_recursion2.c
@@ -1,6 +1,6 @@
/* run.config*
- OPT: -aorai-buchi tests/aorai/test_recursion2.promela -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-buchi tests/aorai/test_recursion3.promela -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-buchi @PTEST_DIR@/@PTEST_NAME@.promela -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-buchi @PTEST_DIR@/test_recursion3.promela -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/aorai/test_recursion2.promela b/src/plugins/aorai/tests/aorai_ltl/test_recursion2.promela
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_recursion2.promela
rename to src/plugins/aorai/tests/aorai_ltl/test_recursion2.promela
diff --git a/src/plugins/aorai/tests/aorai/test_recursion3.promela b/src/plugins/aorai/tests/aorai_ltl/test_recursion3.promela
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_recursion3.promela
rename to src/plugins/aorai/tests/aorai_ltl/test_recursion3.promela
diff --git a/src/plugins/aorai/tests/aorai/test_switch2.c b/src/plugins/aorai/tests/aorai_ltl/test_switch2.c
similarity index 87%
rename from src/plugins/aorai/tests/aorai/test_switch2.c
rename to src/plugins/aorai/tests/aorai_ltl/test_switch2.c
index 39039890d9ae8ac8f6c81dc31a1959697781ad9b..f411cec23dcd459cbfe1bdb5d3d33b05ad6e3ee2 100644
--- a/src/plugins/aorai/tests/aorai/test_switch2.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_switch2.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_switch2.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/aorai/test_switch2.ltl b/src/plugins/aorai/tests/aorai_ltl/test_switch2.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_switch2.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_switch2.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_switch3.c b/src/plugins/aorai/tests/aorai_ltl/test_switch3.c
similarity index 91%
rename from src/plugins/aorai/tests/aorai/test_switch3.c
rename to src/plugins/aorai/tests/aorai_ltl/test_switch3.c
index dee84adec79ec7dd8c64b41b82755e12a4e6fb1a..42e5fc6ba9aebb0bf7be62ec776e3a969f250d4a 100644
--- a/src/plugins/aorai/tests/aorai/test_switch3.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_switch3.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/aorai/test_switch3.ltl b/src/plugins/aorai/tests/aorai_ltl/test_switch3.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_switch3.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_switch3.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_switch3_et_recursion.c b/src/plugins/aorai/tests/aorai_ltl/test_switch3_et_recursion.c
similarity index 80%
rename from src/plugins/aorai/tests/aorai/test_switch3_et_recursion.c
rename to src/plugins/aorai/tests/aorai_ltl/test_switch3_et_recursion.c
index 343354821341fbd6584911940f28e629aa9128ae..00caa9826bb96e63a099b54204d1e1d5e9c3aeab 100644
--- a/src/plugins/aorai/tests/aorai/test_switch3_et_recursion.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_switch3_et_recursion.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_switch3_et_recursion.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/@PTEST_NAME@.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/aorai/test_switch3_et_recursion.ltl b/src/plugins/aorai/tests/aorai_ltl/test_switch3_et_recursion.ltl
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_switch3_et_recursion.ltl
rename to src/plugins/aorai/tests/aorai_ltl/test_switch3_et_recursion.ltl
diff --git a/src/plugins/aorai/tests/aorai/test_switch3_if.c b/src/plugins/aorai/tests/aorai_ltl/test_switch3_if.c
similarity index 90%
rename from src/plugins/aorai/tests/aorai/test_switch3_if.c
rename to src/plugins/aorai/tests/aorai_ltl/test_switch3_if.c
index e9dd534a3b04c111edbeb0e9a5d8bde6d530436e..f6375d4d859a018e4349cbcbdca037d48298de40 100644
--- a/src/plugins/aorai/tests/aorai/test_switch3_if.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_switch3_if.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/aorai/test_switch3_return.c b/src/plugins/aorai/tests/aorai_ltl/test_switch3_return.c
similarity index 91%
rename from src/plugins/aorai/tests/aorai/test_switch3_return.c
rename to src/plugins/aorai/tests/aorai_ltl/test_switch3_return.c
index 6c4583363a779481ec0b2ddb87c298560d82eb09..a105540b9829ff3d2cdb2a7c12b4f7b056c8ece2 100644
--- a/src/plugins/aorai/tests/aorai/test_switch3_return.c
+++ b/src/plugins/aorai/tests/aorai_ltl/test_switch3_return.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-ltl tests/aorai/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-ltl @PTEST_DIR@/test_switch3.ltl -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
/* Calcul de la longueur cumulee des chaines de caracteres prises en parametre */
diff --git a/src/plugins/aorai/tests/aorai/assigns.c b/src/plugins/aorai/tests/aorai_ya/assigns.c
similarity index 50%
rename from src/plugins/aorai/tests/aorai/assigns.c
rename to src/plugins/aorai/tests/aorai_ya/assigns.c
index 15e4e3c4b549ff88a94021b8de322abc12a24eda..ce6fe159678db8d14bddb1119d020f3b6362b14b 100644
--- a/src/plugins/aorai/tests/aorai/assigns.c
+++ b/src/plugins/aorai/tests/aorai_ya/assigns.c
@@ -1,8 +1,8 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/assigns.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
- OPT: -aorai-automata tests/aorai/assigns_det.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/assigns_det.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
MODULE: @PTEST_DIR@/name_projects.cmxs
- OPT: -aorai-automata tests/aorai/assigns.ya -aorai-test 1 -then -print
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -then -print
*/
int X;
diff --git a/src/plugins/aorai/tests/aorai/assigns.ya b/src/plugins/aorai/tests/aorai_ya/assigns.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/assigns.ya
rename to src/plugins/aorai/tests/aorai_ya/assigns.ya
diff --git a/src/plugins/aorai/tests/aorai/assigns_det.ya b/src/plugins/aorai/tests/aorai_ya/assigns_det.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/assigns_det.ya
rename to src/plugins/aorai/tests/aorai_ya/assigns_det.ya
diff --git a/src/plugins/aorai/tests/aorai/bts1289-2.ya b/src/plugins/aorai/tests/aorai_ya/bts1289-2.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/bts1289-2.ya
rename to src/plugins/aorai/tests/aorai_ya/bts1289-2.ya
diff --git a/src/plugins/aorai/tests/aorai_ya/bts1289.i b/src/plugins/aorai/tests/aorai_ya/bts1289.i
new file mode 100644
index 0000000000000000000000000000000000000000..2c6c8f9aa59097ab9cd9f8dd9aa63d1ffcf62900
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/bts1289.i
@@ -0,0 +1,14 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@-2.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ */
+
+void a(void) {}
+
+void main(void)
+{
+ //@ loop assigns i;
+ for (int i=0; i<10; ++i)
+ a();
+}
+
diff --git a/src/plugins/aorai/tests/aorai/bts1289.ya b/src/plugins/aorai/tests/aorai_ya/bts1289.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/bts1289.ya
rename to src/plugins/aorai/tests/aorai_ya/bts1289.ya
diff --git a/src/plugins/aorai/tests/aorai/declared_function.i b/src/plugins/aorai/tests/aorai_ya/declared_function.i
similarity index 100%
rename from src/plugins/aorai/tests/aorai/declared_function.i
rename to src/plugins/aorai/tests/aorai_ya/declared_function.i
diff --git a/src/plugins/aorai/tests/aorai/declared_function.ya b/src/plugins/aorai/tests/aorai_ya/declared_function.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/declared_function.ya
rename to src/plugins/aorai/tests/aorai_ya/declared_function.ya
diff --git a/src/plugins/aorai/tests/aorai/deterministic.i b/src/plugins/aorai/tests/aorai_ya/deterministic.i
similarity index 58%
rename from src/plugins/aorai/tests/aorai/deterministic.i
rename to src/plugins/aorai/tests/aorai_ya/deterministic.i
index f0171ca436a915b3405a9ede9bc6375a801945f8..b92271127e264c85e2578be4fbdc86a1e7ac8a9e 100644
--- a/src/plugins/aorai/tests/aorai/deterministic.i
+++ b/src/plugins/aorai/tests/aorai_ya/deterministic.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/deterministic.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int X;
diff --git a/src/plugins/aorai/tests/aorai/deterministic.ya b/src/plugins/aorai/tests/aorai_ya/deterministic.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/deterministic.ya
rename to src/plugins/aorai/tests/aorai_ya/deterministic.ya
diff --git a/src/plugins/aorai/tests/aorai_ya/formals.i b/src/plugins/aorai/tests/aorai_ya/formals.i
new file mode 100644
index 0000000000000000000000000000000000000000..4a32df49b67be992c14ceb88e3541d05c638992d
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/formals.i
@@ -0,0 +1,9 @@
+/* run.config*
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+int f(int x) { return x; }
+
+int g(int y) { return y; }
+
+int main() { f(1); g(2); }
diff --git a/src/plugins/aorai/tests/aorai/formals.ya b/src/plugins/aorai/tests/aorai_ya/formals.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/formals.ya
rename to src/plugins/aorai/tests/aorai_ya/formals.ya
diff --git a/src/plugins/aorai/tests/aorai_ya/generate_assigns_bts1290.i b/src/plugins/aorai/tests/aorai_ya/generate_assigns_bts1290.i
new file mode 100644
index 0000000000000000000000000000000000000000..2e92796ec0655d2ae0977566205fc1072e275a60
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/generate_assigns_bts1290.i
@@ -0,0 +1,9 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -load-module tests/Aorai_test.cmxs -aorai-test 1 -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ */
+void main(void)
+{
+ //@ loop assigns i;
+ for (int i=0; i<10; ++i)
+ ;
+}
diff --git a/src/plugins/aorai/tests/aorai/generate_assigns_bts1290.ya b/src/plugins/aorai/tests/aorai_ya/generate_assigns_bts1290.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/generate_assigns_bts1290.ya
rename to src/plugins/aorai/tests/aorai_ya/generate_assigns_bts1290.ya
diff --git a/src/plugins/aorai/tests/aorai_ya/hoare_seq.i b/src/plugins/aorai/tests/aorai_ya/hoare_seq.i
new file mode 100644
index 0000000000000000000000000000000000000000..cc7e148477430589b00c142325c5a4baf3a32531
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/hoare_seq.i
@@ -0,0 +1,14 @@
+/* run.config*
+OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+void f(void) { }
+
+/*@ behavior bhv:
+ assumes c > 0;
+ ensures \result == 0;
+*/
+int main(int c) {
+ if (c <= 0) { f (); }
+ return 0;
+}
diff --git a/src/plugins/aorai/tests/aorai/hoare_seq.ya b/src/plugins/aorai/tests/aorai_ya/hoare_seq.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/hoare_seq.ya
rename to src/plugins/aorai/tests/aorai_ya/hoare_seq.ya
diff --git a/src/plugins/aorai/tests/aorai/incorrect.i b/src/plugins/aorai/tests/aorai_ya/incorrect.i
similarity index 100%
rename from src/plugins/aorai/tests/aorai/incorrect.i
rename to src/plugins/aorai/tests/aorai_ya/incorrect.i
diff --git a/src/plugins/aorai/tests/aorai/incorrect.ya b/src/plugins/aorai/tests/aorai_ya/incorrect.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/incorrect.ya
rename to src/plugins/aorai/tests/aorai_ya/incorrect.ya
diff --git a/src/plugins/aorai/tests/aorai/loop_bts1050.i b/src/plugins/aorai/tests/aorai_ya/loop_bts1050.i
similarity index 81%
rename from src/plugins/aorai/tests/aorai/loop_bts1050.i
rename to src/plugins/aorai/tests/aorai_ya/loop_bts1050.i
index 73fd922002a79ff210b984ad3518049694d684c4..fdec741b7b32ef14be4756afd8847a9ac21ccb27 100644
--- a/src/plugins/aorai/tests/aorai/loop_bts1050.i
+++ b/src/plugins/aorai/tests/aorai_ya/loop_bts1050.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/loop_bts1050.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f(){};
diff --git a/src/plugins/aorai/tests/aorai/loop_bts1050.ya b/src/plugins/aorai/tests/aorai_ya/loop_bts1050.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/loop_bts1050.ya
rename to src/plugins/aorai/tests/aorai_ya/loop_bts1050.ya
diff --git a/src/plugins/aorai/tests/aorai/monostate.i b/src/plugins/aorai/tests/aorai_ya/monostate.i
similarity index 100%
rename from src/plugins/aorai/tests/aorai/monostate.i
rename to src/plugins/aorai/tests/aorai_ya/monostate.i
diff --git a/src/plugins/aorai/tests/aorai/monostate.ya b/src/plugins/aorai/tests/aorai_ya/monostate.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/monostate.ya
rename to src/plugins/aorai/tests/aorai_ya/monostate.ya
diff --git a/src/plugins/aorai/tests/aorai/name_projects.ml b/src/plugins/aorai/tests/aorai_ya/name_projects.ml
similarity index 100%
rename from src/plugins/aorai/tests/aorai/name_projects.ml
rename to src/plugins/aorai/tests/aorai_ya/name_projects.ml
diff --git a/src/plugins/aorai/tests/aorai_ya/not_prm.i b/src/plugins/aorai/tests/aorai_ya/not_prm.i
new file mode 100644
index 0000000000000000000000000000000000000000..d96e123d6e6a367565597f0cce0df942b23a2ba5
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/not_prm.i
@@ -0,0 +1,7 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test -main f -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+int f(int x) {
+ return x;
+}
diff --git a/src/plugins/aorai/tests/aorai/not_prm.ya b/src/plugins/aorai/tests/aorai_ya/not_prm.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/not_prm.ya
rename to src/plugins/aorai/tests/aorai_ya/not_prm.ya
diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.0.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/assigns.0.res.oracle
index 587631cdbf4b3e377b840611ff496de8c6814733..5c7443d37ab4b68d8a950a2ddb5ef0c455aab032 100644
--- a/src/plugins/aorai/tests/aorai/oracle/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_assigns_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.1.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/assigns.1.res.oracle
index c6501e5664e85b37841806f7963b170b08c65f45..01876080d5c50d062d19b8d6c20f60cc1b5abb37 100644
--- a/src/plugins/aorai/tests/aorai/oracle/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_assigns_1.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/assigns.2.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.2.res.oracle
similarity index 83%
rename from src/plugins/aorai/tests/aorai/oracle_prove/assigns.2.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/assigns.2.res.oracle
index a03928c6cad0adaaa70de524ae1c846eca1db1bd..a88a5548285661e2f42c260ff33502876dbeb0fb 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/assigns.2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/assigns.2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
/* Generated by Frama-C */
int X;
diff --git a/src/plugins/aorai/tests/aorai/oracle/bts1289.0.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.0.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/bts1289.0.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/bts1289.0.res.oracle
index a313805caf47651715eb72d737ff22d1aa670a63..3dea38d70a1758d514c80e5bebfdd12241a774c9 100644
--- a/src/plugins/aorai/tests/aorai/oracle/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/bts1289.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_bts1289_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle/bts1289.1.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.1.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/bts1289.1.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/bts1289.1.res.oracle
index 0e1b58e415e22e647e96dd4122c6bc403b1bcb14..5f22740b63832b2c3709c3f672c8825a93836f61 100644
--- a/src/plugins/aorai/tests/aorai/oracle/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/bts1289.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/bts1289.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_bts1289_1.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/declared_function.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/declared_function.res.oracle
similarity index 97%
rename from src/plugins/aorai/tests/aorai/oracle/declared_function.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/declared_function.res.oracle
index 7b00c3f64fecbe874659161d8d987a6e160fae2c..fbeda724d7097f2cde8b8de75d6e58728dba4443 100644
--- a/src/plugins/aorai/tests/aorai/oracle/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/declared_function.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/declared_function.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/declared_function.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_declared_function_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/deterministic.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/deterministic.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/deterministic.res.oracle
index 03ffe79dc58e46b95e3bbf8943e14beeb6f46b90..c4a89c4951e49dd6d97a713c0904a4e9db62228e 100644
--- a/src/plugins/aorai/tests/aorai/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/deterministic.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/deterministic.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/deterministic.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_deterministic_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/formals.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/formals.res.oracle
index 55923d34f281cd32b37030daf68a3585dc3a410b..c2bd9a6d56645f2ef6e3907fbaf3ec8b9e0ef476 100644
--- a/src/plugins/aorai/tests/aorai/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/formals.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/formals.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/formals.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_formals_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/generate_assigns_bts1290.res.oracle
similarity index 96%
rename from src/plugins/aorai/tests/aorai/oracle/generate_assigns_bts1290.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/generate_assigns_bts1290.res.oracle
index f822ad621a1f063e86bd0af5f86bb9adea43a345..3d7e763902c3225e5a84ac081814ce057614a2eb 100644
--- a/src/plugins/aorai/tests/aorai/oracle/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/generate_assigns_bts1290.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/generate_assigns_bts1290.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/generate_assigns_bts1290.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_generate_assigns_bts1290_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/hoare_seq.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/hoare_seq.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/hoare_seq.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/hoare_seq.res.oracle
index c420dac4bde2f7fb559303c95568f7bd79685dae..546c4e7d846c246bf3f5083f02424d2db1110ced 100644
--- a/src/plugins/aorai/tests/aorai/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/hoare_seq.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/hoare_seq.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/hoare_seq.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_hoare_seq_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/incorrect.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/incorrect.res.oracle
similarity index 96%
rename from src/plugins/aorai/tests/aorai/oracle/incorrect.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/incorrect.res.oracle
index 62b6e9a75cc2e8b3dfeb92af6e68e33f5c6d02fa..6a56d3e182e0c035ee5381cd801f520ad7f4e5cc 100644
--- a/src/plugins/aorai/tests/aorai/oracle/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/incorrect.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/incorrect.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/incorrect.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_incorrect_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/loop_bts1050.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/loop_bts1050.res.oracle
index be1dc66d50a67adc2e0084901bd3f42750112477..c0ad530b635d88c70687395a24eedf78959003ef 100644
--- a/src/plugins/aorai/tests/aorai/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/loop_bts1050.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/loop_bts1050.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/loop_bts1050.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_loop_bts1050_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/monostate.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/monostate.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/monostate.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/monostate.res.oracle
index 678af350fd7113676fc7b5fed075ebe1b93095d2..4e83e52e08bab259fa97bfe3812b0f70e87f2625 100644
--- a/src/plugins/aorai/tests/aorai/oracle/monostate.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/monostate.res.oracle
@@ -1,7 +1,7 @@
-[kernel] Parsing tests/aorai/monostate.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/monostate.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
-[aorai] tests/aorai/monostate.i:8: Warning:
+[aorai] tests/aorai_ya/monostate.i:8: Warning:
Call to main not conforming to automaton (pre-cond). Assuming it is on a dead path
[kernel] Parsing /tmp/aorai_monostate_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/not_prm.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/not_prm.res.oracle
similarity index 97%
rename from src/plugins/aorai/tests/aorai/oracle/not_prm.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/not_prm.res.oracle
index f8d92a9b563fdf9512b524ee09ceb1d18005dca1..6455cd141e580a4883d326c2a53bc531ba4752fc 100644
--- a/src/plugins/aorai/tests/aorai/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/not_prm.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/not_prm.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/not_prm.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_not_prm_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/other.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/other.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/other.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/other.res.oracle
index ad7f48504f1b3b471917a56a6f4f8596245aefe0..1b70959421e89b5b3d9f3e2898a0c068a36c7696 100644
--- a/src/plugins/aorai/tests/aorai/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/other.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/other.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/other.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_other_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/seq.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/seq.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/seq.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/seq.res.oracle
index a5cacc4f933d918b45b6edc55ad5f29a5fae441f..6d3bd0b4fd98b0ba42715b9b168313a037557a6d 100644
--- a/src/plugins/aorai/tests/aorai/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/seq.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/seq.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/seq.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_seq_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/seq_loop.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/seq_loop.res.oracle
index ee365599daca21839bef129193e1c900b8b41a3a..37a5942b8e57f96812af05d45bef498561273caa 100644
--- a/src/plugins/aorai/tests/aorai/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/seq_loop.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/seq_loop.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/seq_loop.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_seq_loop_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/single_call.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/single_call.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/single_call.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/single_call.res.oracle
index d93f86515a7c9e02f5d2762a5fff86a604f82b2b..89cfcb8ea821190dc0cc3ea3870e2fe6dbd2ce62 100644
--- a/src/plugins/aorai/tests/aorai/oracle/single_call.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/single_call.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/single_call.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/single_call.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_single_call_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_acces_params.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_acces_params.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params.res.oracle
index ad696afccfd8cc459fb46df5f66bcb8dec19b9df..6920ad1626231603e42666fb549a8b29638eb6e1 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_acces_params.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_acces_params.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_acces_params_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_acces_params2.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params2.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_acces_params2.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params2.res.oracle
index 49f7c5b25ad5468a630d043c4404cd1b7bf174fa..9899759571f86557d6b98dc26fffb020f53449e7 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_acces_params2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_acces_params2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_acces_params2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_acces_params2_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_boucle_rechercheTableau.res.oracle
similarity index 97%
rename from src/plugins/aorai/tests/aorai/oracle/test_boucle_rechercheTableau.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_boucle_rechercheTableau.res.oracle
index 49a1be8807f96a252a379b0fc677353e8d3d2b65..c65e202d5f674ce91226a5046aa89ee2729d7970 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_boucle_rechercheTableau.res.oracle
@@ -1,7 +1,7 @@
-[kernel] Parsing tests/aorai/test_boucle_rechercheTableau.c (with preprocessing)
-[kernel] tests/aorai/test_boucle_rechercheTableau.c:17: Warning:
+[kernel] Parsing tests/aorai_ya/test_boucle_rechercheTableau.c (with preprocessing)
+[kernel] tests/aorai_ya/test_boucle_rechercheTableau.c:17: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_boucle_rechercheTableau.c:7: Warning:
+[kernel] tests/aorai_ya/test_boucle_rechercheTableau.c:7: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_factorial2.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_factorial.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/test_factorial2.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_factorial.res.oracle
index 68c37c23c9cdb73b438d4009ded72e36cc29d04e..2db6fe590f82a8dfe1d0376ab13a987d8fe35aa4 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_factorial2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_factorial.res.oracle
@@ -1,6 +1,6 @@
-[kernel] Parsing tests/aorai/test_factorial2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_factorial.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
-[kernel] Parsing /tmp/aorai_test_factorial2_0.i (no preprocessing)
+[kernel] Parsing /tmp/aorai_test_factorial_0.i (no preprocessing)
/* Generated by Frama-C */
enum aorai_ListOper {
op_decode_int = 2,
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_recursion4.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion4.res.oracle
similarity index 99%
rename from src/plugins/aorai/tests/aorai/oracle/test_recursion4.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_recursion4.res.oracle
index 3a5c6d3807794b18ddee0f7cf99b49ebca9ccf80..8a7f6b375212ee855fd0f4d271204ec492722401 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion4.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_recursion4.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_recursion4.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion4_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_recursion5.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion5.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/test_recursion5.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_recursion5.res.oracle
index 8bc2cd519afb0fe2dc55feb7cabb5469e06a1b1e..f4f409b2231bf79236b0287a764b41e9a711eaa6 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_recursion5.res.oracle
@@ -1,7 +1,7 @@
-[kernel] Parsing tests/aorai/test_recursion5.c (with preprocessing)
-[kernel] tests/aorai/test_recursion5.c:12: Warning:
+[kernel] Parsing tests/aorai_ya/test_recursion5.c (with preprocessing)
+[kernel] tests/aorai_ya/test_recursion5.c:12: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_recursion5.c:28: Warning:
+[kernel] tests/aorai_ya/test_recursion5.c:28: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion5_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle/test_struct.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle/test_struct.res.oracle
similarity index 98%
rename from src/plugins/aorai/tests/aorai/oracle/test_struct.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle/test_struct.res.oracle
index e03f82652406ebc3c89d48ee0adc9cc516e6194b..48449b62e49d386fd111c2a150c6ab9990218630 100644
--- a/src/plugins/aorai/tests/aorai/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle/test_struct.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_struct.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_struct.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_struct_0.i (no preprocessing)
/* Generated by Frama-C */
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/assigns.0.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.0.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/assigns.0.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.0.res.oracle
index 5aec8b21daa3a3dcb4af484c1f115d2b59736883..3bdcb7f459f7fb2a44ed44f1aa0aaee6ba7e272e 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/assigns.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_assigns_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/assigns.1.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.1.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/assigns.1.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.1.res.oracle
index 49feab1f711fb27f3d3cbe9023b371942ae021b6..64a6a02b04312590aa3e5ec95bb6490101f14a58 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/assigns.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_assigns_1.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle/assigns.2.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.2.res.oracle
similarity index 83%
rename from src/plugins/aorai/tests/aorai/oracle/assigns.2.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.2.res.oracle
index a03928c6cad0adaaa70de524ae1c846eca1db1bd..a88a5548285661e2f42c260ff33502876dbeb0fb 100644
--- a/src/plugins/aorai/tests/aorai/oracle/assigns.2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/assigns.2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/assigns.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/assigns.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
/* Generated by Frama-C */
int X;
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/bts1289.0.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.0.res.oracle
similarity index 79%
rename from src/plugins/aorai/tests/aorai/oracle_prove/bts1289.0.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.0.res.oracle
index 43d8b12fc49f8f8b86c69c30a399b5925cb64bab..84559a6dd0ebcc1b57577ce56e7faf127b7b5ea2 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/bts1289.0.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.0.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/bts1289.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_bts1289_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/bts1289.1.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.1.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/bts1289.1.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.1.res.oracle
index f8cbd2cb00cc28beac038201209a13a6f97f0c01..67505dcb5c5fe63cb83fcc65adc52c3a5bd19be0 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/bts1289.1.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/bts1289.1.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/bts1289.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/bts1289.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_bts1289_1.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/declared_function.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/declared_function.res.oracle
similarity index 81%
rename from src/plugins/aorai/tests/aorai/oracle_prove/declared_function.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/declared_function.res.oracle
index a648f24de411db26b26f4b5b4d45c9eab0db4440..7b836a362ab1163bacde49cb7e4253fadba3ae57 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/declared_function.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/declared_function.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/declared_function.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/declared_function.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_declared_function_0.i (no preprocessing)
[kernel:annot:missing-spec] /tmp/aorai_declared_function_0.i:48: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/deterministic.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/deterministic.res.oracle
similarity index 66%
rename from src/plugins/aorai/tests/aorai/oracle_prove/deterministic.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/deterministic.res.oracle
index 24fb75961ac86626467eb9a9f64ce3cc57ff36fc..40255d6fc4b460ffeae5c3d5ba8c673f9fc10a9f 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/deterministic.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/deterministic.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/deterministic.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_deterministic_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/formals.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/formals.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/formals.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/formals.res.oracle
index 909b386d342a780effeac57643276283280105cd..b7c2460da5ec97a7f2271f054e44d95a3dd6bb6c 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/formals.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/formals.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/formals.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/formals.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_formals_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/generate_assigns_bts1290.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/generate_assigns_bts1290.res.oracle
similarity index 65%
rename from src/plugins/aorai/tests/aorai/oracle_prove/generate_assigns_bts1290.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/generate_assigns_bts1290.res.oracle
index cbb069f8f76dfa325a45f225fae22e8ce906bdcb..e402347bb7fc056e82dd3e8504c6050e3590dda5 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/generate_assigns_bts1290.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/generate_assigns_bts1290.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/generate_assigns_bts1290.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/generate_assigns_bts1290.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_generate_assigns_bts1290_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/hoare_seq.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/hoare_seq.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/hoare_seq.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/hoare_seq.res.oracle
index 2270c4bc39855f932441fed24b4032d593122f67..fb6a559a080c3cde36d0d6f50f3904f680d036f2 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/hoare_seq.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/hoare_seq.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/hoare_seq.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_hoare_seq_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/incorrect.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/incorrect.res.oracle
similarity index 86%
rename from src/plugins/aorai/tests/aorai/oracle_prove/incorrect.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/incorrect.res.oracle
index b981ababa8830e6f8e3555ceded3f9d253f2a26e..5d37997bb66de5b2c67f367f052896246901a681 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/incorrect.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/incorrect.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/incorrect.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/incorrect.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[aorai] Warning: Call to main does not follow automaton's specification. This path is assumed to be dead
[kernel] Parsing /tmp/aorai_incorrect_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/loop_bts1050.res.oracle
similarity index 66%
rename from src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/loop_bts1050.res.oracle
index 92104920d5c8adb5c661dc1d9b2aad3ecd67d897..2aa37b76715411cc4a93e8cc112216188223485d 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/loop_bts1050.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/loop_bts1050.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/loop_bts1050.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_loop_bts1050_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/oracle_prove/monostate.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/monostate.res.oracle
new file mode 100644
index 0000000000000000000000000000000000000000..204c70d48603b1985a11edd36203e5c30dc529bd
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/monostate.res.oracle
@@ -0,0 +1 @@
+[kernel] Parsing tests/aorai_ya/monostate.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/not_prm.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/not_prm.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/not_prm.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/not_prm.res.oracle
index 01011d01c1f0027d7567671d668e8d8cf2148805..1b02aa00afdce03664c43bcfad7446b161d84efa 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/not_prm.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/not_prm.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/not_prm.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_not_prm_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/other.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/other.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/other.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/other.res.oracle
index 1d33786221618dd7e40f0ee66d798e851849010c..e0b3215a1bc2fd6b7f741a66b2d397429f01b8b5 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/other.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/other.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/other.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/other.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_other_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq.res.oracle
similarity index 68%
rename from src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/seq.res.oracle
index ab5514b69d283470a1e2184cdcc12e63f8ebb982..bb5f9ad8f3eb4a5a728b972b6a1f79269a6afdb6 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/seq.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/seq.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/seq.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_seq_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq_loop.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/seq_loop.res.oracle
index 64b2e8b35400831ed2002e84f81fae3ae841e55f..c9b971ff32f785c699f1943afedef436ed421d0b 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/seq_loop.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/seq_loop.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/seq_loop.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_seq_loop_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/single_call.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/single_call.res.oracle
similarity index 67%
rename from src/plugins/aorai/tests/aorai/oracle_prove/single_call.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/single_call.res.oracle
index 705c6f7085cc5e1a5483e6514b0334623f911d3c..7e3251748543b0c59732d52fe7cefbd879fab34d 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/single_call.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/single_call.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/single_call.i (no preprocessing)
+[kernel] Parsing tests/aorai_ya/single_call.i (no preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_single_call_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_acces_params.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params.res.oracle
similarity index 76%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_acces_params.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params.res.oracle
index 006ec0acdd2678df89af629134ab5fcba9ee2f0b..eaa6a845adf8f0cecbbf57ddade5412f6d10e8a9 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_acces_params.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_acces_params.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_acces_params_0.i (no preprocessing)
[wp] /tmp/aorai_test_acces_params_0.i:4: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_acces_params2.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params2.res.oracle
similarity index 76%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_acces_params2.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params2.res.oracle
index c5b2f97589bfe3a0b833081f0782788f5b8af497..dcd88018b2077a89a93a86987f9fb240be2e8cd4 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_acces_params2.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_acces_params2.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_acces_params2.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_acces_params2_0.i (no preprocessing)
[wp] /tmp/aorai_test_acces_params2_0.i:3: Warning:
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
similarity index 63%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_boucle_rechercheTableau.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
index 6a9fc826a871d2802b82780f28a0df4c9c0f2ee0..c64d82f705727818e5737df5d9ee6ca3fc415864 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_boucle_rechercheTableau.res.oracle
@@ -1,7 +1,7 @@
-[kernel] Parsing tests/aorai/test_boucle_rechercheTableau.c (with preprocessing)
-[kernel] tests/aorai/test_boucle_rechercheTableau.c:17: Warning:
+[kernel] Parsing tests/aorai_ya/test_boucle_rechercheTableau.c (with preprocessing)
+[kernel] tests/aorai_ya/test_boucle_rechercheTableau.c:17: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_boucle_rechercheTableau.c:7: Warning:
+[kernel] tests/aorai_ya/test_boucle_rechercheTableau.c:7: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_boucle_rechercheTableau_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_factorial.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_factorial.res.oracle
similarity index 65%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_factorial.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_factorial.res.oracle
index 999cb771ba7268229f0af5eceb9d4963f59c3eea..4265d80c2eb5313a270a3c2918b056caed21c1fb 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_factorial.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_factorial.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_factorial.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_factorial_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion4.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion4.res.oracle
similarity index 65%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_recursion4.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion4.res.oracle
index 2cb6a23598f3b75b3779c7b00937bd4fdd776456..6293804566c02aca053629caed4f6f2e462f0051 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion4.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_recursion4.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_recursion4.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion4_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion5.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion5.res.oracle
similarity index 66%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_recursion5.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion5.res.oracle
index d9337988b6937f7f2deae0720894f0272ce4b0b1..db107f75b48196c402efe5dd5e659a4671124ae2 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_recursion5.res.oracle
@@ -1,7 +1,7 @@
-[kernel] Parsing tests/aorai/test_recursion5.c (with preprocessing)
-[kernel] tests/aorai/test_recursion5.c:12: Warning:
+[kernel] Parsing tests/aorai_ya/test_recursion5.c (with preprocessing)
+[kernel] tests/aorai_ya/test_recursion5.c:12: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
-[kernel] tests/aorai/test_recursion5.c:28: Warning:
+[kernel] tests/aorai_ya/test_recursion5.c:28: Warning:
parsing obsolete ACSL construct '\valid_range(addr,min,max)'. '\valid(addr+(min..max))' should be used instead.
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_recursion5_0.i (no preprocessing)
diff --git a/src/plugins/aorai/tests/aorai/oracle_prove/test_struct.res.oracle b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_struct.res.oracle
similarity index 66%
rename from src/plugins/aorai/tests/aorai/oracle_prove/test_struct.res.oracle
rename to src/plugins/aorai/tests/aorai_ya/oracle_prove/test_struct.res.oracle
index 60ed3fef31e7f4f0c731f19f23e8ad40fb989d92..6571fc60e01366ccb49c3c043d5d571161517658 100644
--- a/src/plugins/aorai/tests/aorai/oracle_prove/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/aorai_ya/oracle_prove/test_struct.res.oracle
@@ -1,4 +1,4 @@
-[kernel] Parsing tests/aorai/test_struct.c (with preprocessing)
+[kernel] Parsing tests/aorai_ya/test_struct.c (with preprocessing)
[aorai] Welcome to the Aorai plugin
[kernel] Parsing /tmp/aorai_test_struct_0.i (no preprocessing)
[wp] Warning: Missing RTE guards
diff --git a/src/plugins/aorai/tests/aorai_ya/other.c b/src/plugins/aorai/tests/aorai_ya/other.c
new file mode 100644
index 0000000000000000000000000000000000000000..4e13872dbf2b5ae2c6f44bb887577bfa91d3402e
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/other.c
@@ -0,0 +1,17 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+int x=0;
+
+void f (void) { x=3; }
+
+void g (void) { x=4; }
+
+int main () {
+ f();
+ g();
+ f();
+ g();
+ return x;
+}
diff --git a/src/plugins/aorai/tests/aorai/other.ya b/src/plugins/aorai/tests/aorai_ya/other.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/other.ya
rename to src/plugins/aorai/tests/aorai_ya/other.ya
diff --git a/src/plugins/aorai/tests/aorai_ya/seq.i b/src/plugins/aorai/tests/aorai_ya/seq.i
new file mode 100644
index 0000000000000000000000000000000000000000..f573a5491b319de72d6072634e78f3ebc33d5381
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/seq.i
@@ -0,0 +1,14 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ */
+
+void f() { }
+
+void g() { }
+
+int main(int c) {
+ if (c) f();
+ g();
+ if (c) g();
+ return 0;
+}
diff --git a/src/plugins/aorai/tests/aorai/seq.ya b/src/plugins/aorai/tests/aorai_ya/seq.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/seq.ya
rename to src/plugins/aorai/tests/aorai_ya/seq.ya
diff --git a/src/plugins/aorai/tests/aorai/seq_loop.i b/src/plugins/aorai/tests/aorai_ya/seq_loop.i
similarity index 58%
rename from src/plugins/aorai/tests/aorai/seq_loop.i
rename to src/plugins/aorai/tests/aorai_ya/seq_loop.i
index 0d85eb80cc33f9cef9a75bb17bf9a5a7bc1b7425..07cc7cf2a9b9593684429bbd6d0a1950f97818c1 100644
--- a/src/plugins/aorai/tests/aorai/seq_loop.i
+++ b/src/plugins/aorai/tests/aorai_ya/seq_loop.i
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/seq_loop.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
void f() {}
diff --git a/src/plugins/aorai/tests/aorai/seq_loop.ya b/src/plugins/aorai/tests/aorai_ya/seq_loop.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/seq_loop.ya
rename to src/plugins/aorai/tests/aorai_ya/seq_loop.ya
diff --git a/src/plugins/aorai/tests/aorai_ya/single_call.i b/src/plugins/aorai/tests/aorai_ya/single_call.i
new file mode 100644
index 0000000000000000000000000000000000000000..257ce2b2c7a4493ee42953dcff3b29bed8d29643
--- /dev/null
+++ b/src/plugins/aorai/tests/aorai_ya/single_call.i
@@ -0,0 +1,5 @@
+/* run.config*
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-acceptance -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+*/
+
+int main () {}
diff --git a/src/plugins/aorai/tests/aorai/single_call.ya b/src/plugins/aorai/tests/aorai_ya/single_call.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/single_call.ya
rename to src/plugins/aorai/tests/aorai_ya/single_call.ya
diff --git a/src/plugins/aorai/tests/aorai/test_acces_params.c b/src/plugins/aorai/tests/aorai_ya/test_acces_params.c
similarity index 65%
rename from src/plugins/aorai/tests/aorai/test_acces_params.c
rename to src/plugins/aorai/tests/aorai_ya/test_acces_params.c
index 3961685e4280d45ec95dac745f7d4c2c618e12ed..884140ce9cab8b66952394937c1595f7a31dd37a 100644
--- a/src/plugins/aorai/tests/aorai/test_acces_params.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_acces_params.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_acces_params.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
int status=0;
diff --git a/src/plugins/aorai/tests/aorai/test_acces_params.ya b/src/plugins/aorai/tests/aorai_ya/test_acces_params.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_acces_params.ya
rename to src/plugins/aorai/tests/aorai_ya/test_acces_params.ya
diff --git a/src/plugins/aorai/tests/aorai/test_acces_params2.c b/src/plugins/aorai/tests/aorai_ya/test_acces_params2.c
similarity index 74%
rename from src/plugins/aorai/tests/aorai/test_acces_params2.c
rename to src/plugins/aorai/tests/aorai_ya/test_acces_params2.c
index df66a09f957e32ac45f7adce7e21c0e23daec659..86092179e3f19e4041f7d3f3b5b2623d073edf51 100644
--- a/src/plugins/aorai/tests/aorai/test_acces_params2.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_acces_params2.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_acces_params2.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_acces_params2.ya b/src/plugins/aorai/tests/aorai_ya/test_acces_params2.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_acces_params2.ya
rename to src/plugins/aorai/tests/aorai_ya/test_acces_params2.ya
diff --git a/src/plugins/aorai/tests/aorai/test_boucle_rechercheTableau.c b/src/plugins/aorai/tests/aorai_ya/test_boucle_rechercheTableau.c
similarity index 79%
rename from src/plugins/aorai/tests/aorai/test_boucle_rechercheTableau.c
rename to src/plugins/aorai/tests/aorai_ya/test_boucle_rechercheTableau.c
index 250ba9f88e384bca7e7c6e95a15247a4cb546213..7dcf436cfe3bc7a95f03bb57faf63c8cca87b1b9 100644
--- a/src/plugins/aorai/tests/aorai/test_boucle_rechercheTableau.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_boucle_rechercheTableau.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_boucle_rechercheTableau.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_boucle_rechercheTableau.ya b/src/plugins/aorai/tests/aorai_ya/test_boucle_rechercheTableau.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_boucle_rechercheTableau.ya
rename to src/plugins/aorai/tests/aorai_ya/test_boucle_rechercheTableau.ya
diff --git a/src/plugins/aorai/tests/aorai/test_factorial2.c b/src/plugins/aorai/tests/aorai_ya/test_factorial.c
similarity index 89%
rename from src/plugins/aorai/tests/aorai/test_factorial2.c
rename to src/plugins/aorai/tests/aorai_ya/test_factorial.c
index 691ac2923125afd84d6a0b5d7bea614694f0362c..9cb2213b68d6e23abeaed004b89d16e8b7a8d67e 100644
--- a/src/plugins/aorai/tests/aorai/test_factorial2.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_factorial.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_factorial.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_factorial.ya b/src/plugins/aorai/tests/aorai_ya/test_factorial.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_factorial.ya
rename to src/plugins/aorai/tests/aorai_ya/test_factorial.ya
diff --git a/src/plugins/aorai/tests/aorai/test_recursion4.c b/src/plugins/aorai/tests/aorai_ya/test_recursion4.c
similarity index 78%
rename from src/plugins/aorai/tests/aorai/test_recursion4.c
rename to src/plugins/aorai/tests/aorai_ya/test_recursion4.c
index b04d4b88ab205d284d0f2dfb964be3f83d693237..cf4c5d8523a6c123692f77b03bb2a129b9e3c20c 100644
--- a/src/plugins/aorai/tests/aorai/test_recursion4.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_recursion4.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_recursion4.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
# pragma JessieIntegerModel(math)
diff --git a/src/plugins/aorai/tests/aorai/test_recursion4.ya b/src/plugins/aorai/tests/aorai_ya/test_recursion4.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_recursion4.ya
rename to src/plugins/aorai/tests/aorai_ya/test_recursion4.ya
diff --git a/src/plugins/aorai/tests/aorai/test_recursion5.c b/src/plugins/aorai/tests/aorai_ya/test_recursion5.c
similarity index 87%
rename from src/plugins/aorai/tests/aorai/test_recursion5.c
rename to src/plugins/aorai/tests/aorai_ya/test_recursion5.c
index 00dc4c63e2ef6f0795168cd0e19bf398b24a6574..241030e711241484c0f829e0a16101618649f832 100644
--- a/src/plugins/aorai/tests/aorai/test_recursion5.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_recursion5.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_recursion5.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
diff --git a/src/plugins/aorai/tests/aorai/test_recursion5.ya b/src/plugins/aorai/tests/aorai_ya/test_recursion5.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_recursion5.ya
rename to src/plugins/aorai/tests/aorai_ya/test_recursion5.ya
diff --git a/src/plugins/aorai/tests/aorai/test_struct.c b/src/plugins/aorai/tests/aorai_ya/test_struct.c
similarity index 56%
rename from src/plugins/aorai/tests/aorai/test_struct.c
rename to src/plugins/aorai/tests/aorai_ya/test_struct.c
index 552c7cdb3ec5f66b6f170a1da94111d597f0e97a..1b8ff3ec2ff039f6a94506b149db7d128961e656 100644
--- a/src/plugins/aorai/tests/aorai/test_struct.c
+++ b/src/plugins/aorai/tests/aorai_ya/test_struct.c
@@ -1,5 +1,5 @@
/* run.config*
- OPT: -aorai-automata tests/aorai/test_struct.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
+ OPT: -aorai-automata @PTEST_DIR@/@PTEST_NAME@.ya -aorai-test 1 -aorai-acceptance -load-module tests/Aorai_test.cmxs -aorai-test-number @PTEST_NUMBER@ @PROVE_OPTIONS@
*/
struct People{
diff --git a/src/plugins/aorai/tests/aorai/test_struct.ya b/src/plugins/aorai/tests/aorai_ya/test_struct.ya
similarity index 100%
rename from src/plugins/aorai/tests/aorai/test_struct.ya
rename to src/plugins/aorai/tests/aorai_ya/test_struct.ya