diff --git a/src/plugins/aorai/tests/Aorai_test.ml b/src/plugins/aorai/tests/Aorai_test.ml
index b559eeb411ce69b62129d8bf7ba5beb05415ec3d..7807773dd168dcd111c2c11a09ae6fa1efe817cc 100644
--- a/src/plugins/aorai/tests/Aorai_test.ml
+++ b/src/plugins/aorai/tests/Aorai_test.ml
@@ -1,15 +1,15 @@
(* Small script to test that the code generated by aorai can be parsed again
* by frama-c.
- *)
+*)
open Kernel
module P = Plugin.Register
-(struct
- let name = "aorai testing module"
- let shortname = "aorai-test"
- let help = "utility script for aorai regtests"
- end)
+ (struct
+ let name = "aorai testing module"
+ let shortname = "aorai-test"
+ let help = "utility script for aorai regtests"
+ end)
module TestNumber =
P.Zero
@@ -17,25 +17,25 @@ module TestNumber =
let option_name = "-aorai-test-number"
let help = "test number when multiple tests are run over the same file"
let arg_name = "n"
- end)
+ end)
module InternalWpShare =
P.Filepath(
- struct
- let option_name = "-aorai-test-wp-share"
- let help = "use custom wp share dir (when in internal plugin mode)"
- let arg_name = "dir"
- let existence = Filepath.Must_exist
- let file_kind = "wp share directory"
- end)
+ struct
+ let option_name = "-aorai-test-wp-share"
+ let help = "use custom wp share dir (when in internal plugin mode)"
+ let arg_name = "dir"
+ let existence = Filepath.Must_exist
+ let file_kind = "wp share directory"
+ end)
module ProveAuxSpec =
P.False(
- struct
- let option_name = "-aorai-test-prove-aux-spec"
- let help = "use WP + alt-ergo to prove that generated spec and body \
- of auxiliary automata functions match"
- end)
+ struct
+ let option_name = "-aorai-test-prove-aux-spec"
+ let help = "use WP + alt-ergo to prove that generated spec and body \
+ of auxiliary automata functions match"
+ end)
let ok = ref false
@@ -95,6 +95,7 @@ let extend () =
Project.set_current my_project;
Kernel.SymbolicPath.add ("TMPDIR:"^Filename.get_temp_dir_name());
Files.append_after [ Filepath.Normalized.of_string tmpfile ];
+ Kernel.LogicalOperators.on ();
Constfold.off ();
Ast.compute();
if ProveAuxSpec.get () then begin
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
index 43f443e26e9773bfe488435071f0953066f1112b..af9bc71a2b3a1adf94c0022438693926ffc17f6f 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle.res.oracle
@@ -52,9 +52,8 @@ extern int call_to_an_undefined_function(void);
T0_S2_tmp = T0_S2;
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
- if (T0_S2 == 1) accept_S1_tmp = 1;
- else
- if (accept_S1 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
+ if (T0_S2 == 1 || accept_S1 == 1) accept_S1_tmp = 1;
+ else accept_S1_tmp = 0;
T0_init_tmp = 0;
T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
@@ -159,9 +158,7 @@ int a(void)
accept_S1_tmp = accept_S1;
accept_S1_tmp = 0;
T0_init_tmp = 0;
- if (T0_S2 == 1) T0_S2_tmp = 1;
- else
- if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+ if (T0_S2 == 1 || accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
index 31031e82bb479afbb18fa7e403bf822e42c7f654..9da27b6622ebd3fbb5ae7fefb8a0e694d48175d1 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle1.res.oracle
@@ -271,12 +271,10 @@ int commit_trans(void)
accept_S4_tmp = accept_S4;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
- if (accept_S2 == 1)
- if (status != 0) accept_S4_tmp = 1; else accept_S4_tmp = 0;
+ if (accept_S2 == 1 && status != 0) accept_S4_tmp = 1;
else accept_S4_tmp = 0;
accept_S3_tmp = 0;
- if (accept_S2 == 1)
- if (status == 0) accept_S2_tmp = 1; else accept_S2_tmp = 0;
+ if (accept_S2 == 1 && status == 0) accept_S2_tmp = 1;
else accept_S2_tmp = 0;
accept_S1_tmp = 0;
accept_S1 = accept_S1_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
index e2122593e23b155dd6385ea9e1f256cf66a3157d..3b6f510bb856cc315fcedd97a9d0796d7bbf4d9a 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle2.res.oracle
@@ -144,9 +144,7 @@ int rr = 1;
accept_all_tmp = 0;
accept_S5_tmp = 0;
accept_S4_tmp = 0;
- if (T0_S2 == 1)
- if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
- else accept_S3_tmp = 0;
+ if (T0_S2 == 1 && rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
T0_init_tmp = 0;
if (T0_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
index 44c7d11061b5a33640e834283e79a608ac9885e1..0e2861364d6f1efef4a6191a0cd4ac2a817c7b23 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_boucle3.res.oracle
@@ -236,9 +236,7 @@ void opa(void)
accept_S3_tmp = accept_S3;
accept_all_tmp = accept_all;
accept_all_tmp = 0;
- if (T1_S2 == 1)
- if (rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
- else accept_S3_tmp = 0;
+ if (T1_S2 == 1 && rr == 51) accept_S3_tmp = 1; else accept_S3_tmp = 0;
T1_S2_tmp = 0;
T0_init_tmp = 0;
T0_S4_tmp = 0;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
index 41a681dcff82e65b2fa850c0c8f9f7485adc2a39..384591685af0dcf73ebd192dafbaa2cf6424b777 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_factorial.res.oracle
@@ -217,9 +217,8 @@ int decode_int(char *s)
accept_S2_tmp = accept_S2;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
- if (accept_S1 == 1) accept_S2_tmp = 1;
- else
- if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
+ if (accept_S1 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
+ else accept_S2_tmp = 0;
accept_S1_tmp = 0;
accept_S1 = accept_S1_tmp;
accept_S2 = accept_S2_tmp;
@@ -266,12 +265,10 @@ int decode_int(char *s)
accept_S2_tmp = accept_S2;
accept_init_tmp = accept_init;
accept_init_tmp = 0;
- if (accept_S1 == 1) accept_S2_tmp = 1;
- else
- if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
- if (accept_S1 == 1) accept_S1_tmp = 1;
- else
- if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
+ if (accept_S1 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
+ else accept_S2_tmp = 0;
+ if (accept_S1 == 1 || accept_S2 == 1) accept_S1_tmp = 1;
+ else accept_S1_tmp = 0;
accept_S1 = accept_S1_tmp;
accept_S2 = accept_S2_tmp;
accept_init = accept_init_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
index 2a45f6df9a0c0492d43a914b3956d05da1ec92dc..fd43837e998528a1c7cfa61c0424d06e0c3d4508 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.0.res.oracle
@@ -106,11 +106,7 @@ int global_argc = 0;
accept_T2_tmp = 0;
T1_tmp = 0;
T0_init_tmp = 0;
- if (S1 == 1) S1_tmp = 1;
- else
- if (T1 == 1)
- if (global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
- else S1_tmp = 0;
+ if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
T0_init = T0_init_tmp;
T1 = T1_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
index 741ab2d5228be77cd697851f6fb4c8a80e783e9c..a40a3eae30459dfa081154ccd2b0eed95761f1b8 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_recursion2.1.res.oracle
@@ -106,11 +106,7 @@ int global_argc = 0;
accept_T2_tmp = 0;
T1_tmp = 0;
T0_init_tmp = 0;
- if (S1 == 1) S1_tmp = 1;
- else
- if (T1 == 1)
- if (global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
- else S1_tmp = 0;
+ if (S1 == 1 || T1 == 1 && global_argc > 0) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
T0_init = T0_init_tmp;
T1 = T1_tmp;
@@ -419,9 +415,7 @@ int sumOne(char *t, int length)
T0_init_tmp = T0_init;
T1_tmp = T1;
accept_T2_tmp = accept_T2;
- if (T1 == 1)
- if (res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0;
- else accept_T2_tmp = 0;
+ if (T1 == 1 && res == 1) accept_T2_tmp = 1; else accept_T2_tmp = 0;
if (T1 == 1) T1_tmp = 1; else T1_tmp = 0;
T0_init_tmp = 0;
S1_tmp = 0;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
index 98fef42772d572f1ea75d8df26c6b528b85884c1..d81509eb53661bace2a79e5e2babdface3e95275 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3.res.oracle
@@ -58,9 +58,7 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
- if (T0_S2 == 1) T0_S2_tmp = 1;
- else
- if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+ if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
@@ -249,14 +247,10 @@ int countOne(char *argv)
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
accept_S2_tmp = accept_S2;
- if (T0_S2 == 1) accept_S2_tmp = 1;
- else
- if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
- if (T0_S2 == 1) accept_S1_tmp = 1;
- else
- if (accept_S1 == 1) accept_S1_tmp = 1;
- else
- if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
+ if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
+ else accept_S2_tmp = 0;
+ if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
+ else accept_S1_tmp = 0;
T0_init_tmp = 0;
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
index 4666520a57e4971263d00b54bcf6e80c92189602..5cc019fcad43e0cfacafa6eb123b8055daf1dda4 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_if.res.oracle
@@ -58,9 +58,7 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
- if (T0_S2 == 1) T0_S2_tmp = 1;
- else
- if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+ if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
@@ -247,14 +245,10 @@ int countOne(char *argv)
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
accept_S2_tmp = accept_S2;
- if (T0_S2 == 1) accept_S2_tmp = 1;
- else
- if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
- if (T0_S2 == 1) accept_S1_tmp = 1;
- else
- if (accept_S1 == 1) accept_S1_tmp = 1;
- else
- if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
+ if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
+ else accept_S2_tmp = 0;
+ if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
+ else accept_S1_tmp = 0;
T0_init_tmp = 0;
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
diff --git a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
index 95252b378b334550da4837d9954756ec07d77f4c..0fb781bb7040975d8e51beef6328114ceb34a501 100644
--- a/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
+++ b/src/plugins/aorai/tests/ltl/oracle/test_switch3_return.res.oracle
@@ -58,9 +58,7 @@ enum aorai_OpStatusList {
accept_S2_tmp = 0;
accept_S1_tmp = 0;
T0_init_tmp = 0;
- if (T0_S2 == 1) T0_S2_tmp = 1;
- else
- if (accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
+ if (T0_S2 == 1 || accept_S2 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
T0_init = T0_init_tmp;
accept_S1 = accept_S1_tmp;
@@ -254,14 +252,10 @@ int countOne(char *argv)
T0_init_tmp = T0_init;
accept_S1_tmp = accept_S1;
accept_S2_tmp = accept_S2;
- if (T0_S2 == 1) accept_S2_tmp = 1;
- else
- if (accept_S2 == 1) accept_S2_tmp = 1; else accept_S2_tmp = 0;
- if (T0_S2 == 1) accept_S1_tmp = 1;
- else
- if (accept_S1 == 1) accept_S1_tmp = 1;
- else
- if (accept_S2 == 1) accept_S1_tmp = 1; else accept_S1_tmp = 0;
+ if (T0_S2 == 1 || accept_S2 == 1) accept_S2_tmp = 1;
+ else accept_S2_tmp = 0;
+ if ((T0_S2 == 1 || accept_S1 == 1) || accept_S2 == 1) accept_S1_tmp = 1;
+ else accept_S1_tmp = 0;
T0_init_tmp = 0;
if (accept_S1 == 1) T0_S2_tmp = 1; else T0_S2_tmp = 0;
T0_S2 = T0_S2_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
index 8e648b2ea61129f84dbd19578c474b63943ede22..6b9c9095bc9917c070ddd1dbf2ec9d73de8d75c4 100644
--- a/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/deterministic.res.oracle
@@ -107,14 +107,9 @@ check lemma S0_deterministic_trans{L}:
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_g;
- if (3 == aorai_CurStates) {
- if (x == 4) aorai_CurStates = S4; else goto _LAND;
- }
- else {
- _LAND: ;
- if (3 == aorai_CurStates)
- if (x == 5) aorai_CurStates = S5;
- }
+ if (3 == aorai_CurStates && x == 4) aorai_CurStates = S4;
+ else
+ if (3 == aorai_CurStates && x == 5) aorai_CurStates = S5;
return;
}
@@ -231,8 +226,7 @@ void g(int x)
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
- if (1 == aorai_CurStates)
- if (x == 4) aorai_CurStates = S3;
+ if (1 == aorai_CurStates && x == 4) aorai_CurStates = S3;
return;
}
@@ -278,9 +272,7 @@ void g(int x)
{
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
- if (1 == aorai_CurStates)
- if (res == 0)
- if (X == 5) aorai_CurStates = S2;
+ if (1 == aorai_CurStates && (res == 0 && X == 5)) aorai_CurStates = S2;
return;
}
@@ -351,14 +343,9 @@ int f(int x)
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_real_main;
- if (0 == aorai_CurStates) {
- if (c != 0) aorai_CurStates = S1; else goto _LAND;
- }
- else {
- _LAND: ;
- if (0 == aorai_CurStates)
- if (c == 0) aorai_CurStates = S2;
- }
+ if (0 == aorai_CurStates && c != 0) aorai_CurStates = S1;
+ else
+ if (0 == aorai_CurStates && c == 0) aorai_CurStates = S2;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
index 0b99905eb22e9a6695591a121fd351424d8c7826..52323f131b74b603bc960c19408f6ea80930453f 100644
--- a/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/formals.res.oracle
@@ -132,21 +132,15 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_f;
- if (7 == aorai_CurStates) {
- if (x == 1) {
- aorai_CurStates = aorai_intermediate_state;
- aorai_x = x;
- }
- else goto _LAND;
- }
- else {
- _LAND: ;
- if (7 == aorai_CurStates)
- if (x == 3) {
- aorai_CurStates = aorai_intermediate_state_2;
- aorai_x_0 = x;
- }
+ if (7 == aorai_CurStates && x == 1) {
+ aorai_CurStates = aorai_intermediate_state;
+ aorai_x = x;
}
+ else
+ if (7 == aorai_CurStates && x == 3) {
+ aorai_CurStates = aorai_intermediate_state_2;
+ aorai_x_0 = x;
+ }
return;
}
@@ -219,28 +213,13 @@ check lemma aorai_intermediate_state_deterministic_trans{L}:
{
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_f;
- if (4 == aorai_CurStates) {
- if (aorai_x_0 == 3) aorai_CurStates = OK; else goto _LAND_1;
- }
- else {
- _LAND_1: ;
- if (1 == aorai_CurStates) {
- if (aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0;
- else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (4 == aorai_CurStates) {
- if (aorai_x_0 != 3) aorai_CurStates = aorai_reject;
- else goto _LAND;
- }
- else {
- _LAND: ;
- if (1 == aorai_CurStates)
- if (aorai_x != 1) aorai_CurStates = aorai_reject;
- }
- }
- }
+ if (4 == aorai_CurStates && aorai_x_0 == 3) aorai_CurStates = OK;
+ else
+ if (1 == aorai_CurStates && aorai_x == 1) aorai_CurStates = aorai_intermediate_state_0;
+ else
+ if (4 == aorai_CurStates && aorai_x_0 != 3) aorai_CurStates = aorai_reject;
+ else
+ if (1 == aorai_CurStates && aorai_x != 1) aorai_CurStates = aorai_reject;
return;
}
@@ -438,18 +417,13 @@ int f(int x)
{
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_g;
- if (3 == aorai_CurStates) {
- if (aorai_y == 2) aorai_CurStates = OK; else goto _LAND;
- }
- else {
- _LAND: ;
+ if (3 == aorai_CurStates && aorai_y == 2) aorai_CurStates = OK;
+ else
if (0 == aorai_CurStates) aorai_CurStates = OK;
else
if (5 == aorai_CurStates) aorai_CurStates = aorai_reject;
else
- if (3 == aorai_CurStates)
- if (aorai_y != 2) aorai_CurStates = aorai_reject;
- }
+ if (3 == aorai_CurStates && aorai_y != 2) aorai_CurStates = aorai_reject;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
index ebd409ed392d15619f4c8d0f79e744425eb21ad0..ea603b7e865bbc3a1982b4512166a5ed8cf48eb7 100644
--- a/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/hoare_seq.res.oracle
@@ -315,14 +315,10 @@ int main_bhv_bhv(int c); */
aorai_reject_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
aorai_intermediate_state_1_tmp = 0;
- if (S0 == 1)
- if (c <= 0) aorai_intermediate_state_0_tmp = 1;
- else aorai_intermediate_state_0_tmp = 0;
+ if (S0 == 1 && c <= 0) aorai_intermediate_state_0_tmp = 1;
else aorai_intermediate_state_0_tmp = 0;
bhv_aux = main_bhv_bhv(c);
- if (S0 == 1)
- if (bhv_aux) aorai_intermediate_state_tmp = 1;
- else aorai_intermediate_state_tmp = 0;
+ if (S0 == 1 && bhv_aux) aorai_intermediate_state_tmp = 1;
else aorai_intermediate_state_tmp = 0;
Sf_tmp = 0;
S0_tmp = 0;
@@ -410,25 +406,17 @@ int main_bhv_bhv(int c); */
aorai_intermediate_state_1_tmp = aorai_intermediate_state_1;
aorai_intermediate_state_2_tmp = aorai_intermediate_state_2;
aorai_reject_tmp = aorai_reject;
- if (aorai_intermediate_state_0 == 1) aorai_reject_tmp = 1;
- else
- if (aorai_intermediate_state_2 == 1) {
- if (res != 0) aorai_reject_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- if (aorai_reject == 1) aorai_reject_tmp = 1;
- else aorai_reject_tmp = 0;
- }
+ if ((aorai_intermediate_state_0 == 1 || aorai_intermediate_state_2 == 1 &&
+ res != 0) || aorai_reject == 1)
+ aorai_reject_tmp = 1;
+ else aorai_reject_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
aorai_intermediate_state_1_tmp = 0;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
- if (aorai_intermediate_state == 1) Sf_tmp = 1;
- else
- if (aorai_intermediate_state_2 == 1)
- if (res == 0) Sf_tmp = 1; else Sf_tmp = 0;
- else Sf_tmp = 0;
+ if (aorai_intermediate_state == 1 || aorai_intermediate_state_2 == 1 &&
+ res == 0) Sf_tmp = 1;
+ else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
Sf = Sf_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
index 8057befb9f5e9705eece6bcb9985cbe67a5a3cd2..ccc98a41d83d4339cb70a182bed8396973f9d901 100644
--- a/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/loop_bts1050.res.oracle
@@ -95,14 +95,10 @@ enum aorai_OpStatusList {
aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
aorai_intermediate_state_3_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
- if (aorai_intermediate_state == 1) aorai_intermediate_state_1_tmp = 1;
- else
- if (aorai_intermediate_state_0 == 1)
- if (aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
- else aorai_intermediate_state_1_tmp = 0;
- else aorai_intermediate_state_1_tmp = 0;
- if (aorai_intermediate_state_0 == 1)
- if (aorai_counter < 5) aorai_counter ++;
+ if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1 &&
+ aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
+ else aorai_intermediate_state_1_tmp = 0;
+ if (aorai_intermediate_state_0 == 1 && aorai_counter < 5) aorai_counter ++;
if (aorai_intermediate_state == 1) aorai_counter = 1;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
@@ -543,9 +539,9 @@ void g(void)
aorai_intermediate_state_1_tmp = 0;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
- if (aorai_intermediate_state == 1) Sf_tmp = 1;
- else
- if (aorai_intermediate_state_0 == 1) Sf_tmp = 1; else Sf_tmp = 0;
+ if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1)
+ Sf_tmp = 1;
+ else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
Sf = Sf_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
index b464e8baf7b87b063d54d17c50ae7aa4f34d1a03..39843d1a28ef389cbcc34ab6095bff3f80d0ec8a 100644
--- a/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/metavariables-right.res.oracle
@@ -338,8 +338,7 @@ void g(void)
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_h;
- if (4 == aorai_CurStates)
- if (aorai_x > 0) aorai_CurStates = f_0;
+ if (4 == aorai_CurStates && aorai_x > 0) aorai_CurStates = f_0;
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
index fb6b465a2256fcbac162429a15459d215ef802d0..1d964840b06fc2869b27dc1f9ff1115c052861fc 100644
--- a/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/not_prm.res.oracle
@@ -39,9 +39,7 @@ enum aorai_OpStatusList {
aorai_CurOperation = op_f;
S0_tmp = S0;
Sf_tmp = Sf;
- if (S0 == 1)
- if (x >= 4) Sf_tmp = 1; else Sf_tmp = 0;
- else Sf_tmp = 0;
+ if (S0 == 1 && x >= 4) Sf_tmp = 1; else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
Sf = Sf_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/other.res.oracle b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
index 80809ada84f52d13998c0490ccf20da3bad3ce0f..8f230ecadb224c890456d0ef3ef0415fa9db4e9a 100644
--- a/src/plugins/aorai/tests/ya/oracle/other.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/other.res.oracle
@@ -65,42 +65,13 @@ int x = 0;
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (last == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- if (step1 == 1)
- if (x != 4) step1_tmp = 1; else step1_tmp = 0;
- else step1_tmp = 0;
- }
- }
- if (last == 1) {
- if (x != 4) {
- if (x != 3) last_tmp = 1; else goto _LAND_1;
- }
- else goto _LAND_1;
- }
- else {
- _LAND_1: ;
- if (step1 == 1)
- if (x == 4) last_tmp = 1; else last_tmp = 0;
- else last_tmp = 0;
- }
- if (init == 1) {
- if (x != 3) init_tmp = 1; else goto _LAND_2;
- }
- else {
- _LAND_2: ;
- if (last == 1)
- if (x == 4) init_tmp = 1; else init_tmp = 0;
- else init_tmp = 0;
- }
+ if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4)
+ step1_tmp = 1;
+ else step1_tmp = 0;
+ if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
+ else last_tmp = 0;
+ if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
+ else init_tmp = 0;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -157,42 +128,13 @@ int x = 0;
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (last == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- if (step1 == 1)
- if (x != 4) step1_tmp = 1; else step1_tmp = 0;
- else step1_tmp = 0;
- }
- }
- if (last == 1) {
- if (x != 4) {
- if (x != 3) last_tmp = 1; else goto _LAND_1;
- }
- else goto _LAND_1;
- }
- else {
- _LAND_1: ;
- if (step1 == 1)
- if (x == 4) last_tmp = 1; else last_tmp = 0;
- else last_tmp = 0;
- }
- if (init == 1) {
- if (x != 3) init_tmp = 1; else goto _LAND_2;
- }
- else {
- _LAND_2: ;
- if (last == 1)
- if (x == 4) init_tmp = 1; else init_tmp = 0;
- else init_tmp = 0;
- }
+ if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4)
+ step1_tmp = 1;
+ else step1_tmp = 0;
+ if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
+ else last_tmp = 0;
+ if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
+ else init_tmp = 0;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -313,42 +255,13 @@ void f(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (last == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- if (step1 == 1)
- if (x != 4) step1_tmp = 1; else step1_tmp = 0;
- else step1_tmp = 0;
- }
- }
- if (last == 1) {
- if (x != 4) {
- if (x != 3) last_tmp = 1; else goto _LAND_1;
- }
- else goto _LAND_1;
- }
- else {
- _LAND_1: ;
- if (step1 == 1)
- if (x == 4) last_tmp = 1; else last_tmp = 0;
- else last_tmp = 0;
- }
- if (init == 1) {
- if (x != 3) init_tmp = 1; else goto _LAND_2;
- }
- else {
- _LAND_2: ;
- if (last == 1)
- if (x == 4) init_tmp = 1; else init_tmp = 0;
- else init_tmp = 0;
- }
+ if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4)
+ step1_tmp = 1;
+ else step1_tmp = 0;
+ if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
+ else last_tmp = 0;
+ if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
+ else init_tmp = 0;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -405,42 +318,13 @@ void f(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (last == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- if (step1 == 1)
- if (x != 4) step1_tmp = 1; else step1_tmp = 0;
- else step1_tmp = 0;
- }
- }
- if (last == 1) {
- if (x != 4) {
- if (x != 3) last_tmp = 1; else goto _LAND_1;
- }
- else goto _LAND_1;
- }
- else {
- _LAND_1: ;
- if (step1 == 1)
- if (x == 4) last_tmp = 1; else last_tmp = 0;
- else last_tmp = 0;
- }
- if (init == 1) {
- if (x != 3) init_tmp = 1; else goto _LAND_2;
- }
- else {
- _LAND_2: ;
- if (last == 1)
- if (x == 4) init_tmp = 1; else init_tmp = 0;
- else init_tmp = 0;
- }
+ if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4)
+ step1_tmp = 1;
+ else step1_tmp = 0;
+ if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
+ else last_tmp = 0;
+ if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
+ else init_tmp = 0;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -548,13 +432,9 @@ void g(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1)
- if (x == 3) step1_tmp = 1; else step1_tmp = 0;
- else step1_tmp = 0;
+ if (init == 1 && x == 3) step1_tmp = 1; else step1_tmp = 0;
last_tmp = 0;
- if (init == 1)
- if (x != 3) init_tmp = 1; else init_tmp = 0;
- else init_tmp = 0;
+ if (init == 1 && x != 3) init_tmp = 1; else init_tmp = 0;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
@@ -611,42 +491,13 @@ void g(void)
init_tmp = init;
last_tmp = last;
step1_tmp = step1;
- if (init == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (last == 1) {
- if (x == 3) step1_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- if (step1 == 1)
- if (x != 4) step1_tmp = 1; else step1_tmp = 0;
- else step1_tmp = 0;
- }
- }
- if (last == 1) {
- if (x != 4) {
- if (x != 3) last_tmp = 1; else goto _LAND_1;
- }
- else goto _LAND_1;
- }
- else {
- _LAND_1: ;
- if (step1 == 1)
- if (x == 4) last_tmp = 1; else last_tmp = 0;
- else last_tmp = 0;
- }
- if (init == 1) {
- if (x != 3) init_tmp = 1; else goto _LAND_2;
- }
- else {
- _LAND_2: ;
- if (last == 1)
- if (x == 4) init_tmp = 1; else init_tmp = 0;
- else init_tmp = 0;
- }
+ if ((init == 1 && x == 3 || last == 1 && x == 3) || step1 == 1 && x != 4)
+ step1_tmp = 1;
+ else step1_tmp = 0;
+ if (last == 1 && (x != 4 && x != 3) || step1 == 1 && x == 4) last_tmp = 1;
+ else last_tmp = 0;
+ if (init == 1 && x != 3 || last == 1 && x == 4) init_tmp = 1;
+ else init_tmp = 0;
init = init_tmp;
last = last_tmp;
step1 = step1_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
index b8816b350cc8bac60112c601bb17d0db9ee1b4fe..506dca121a3f23b957ced47740eee807cff752ec 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq.res.oracle
@@ -278,16 +278,10 @@ void f(void)
aorai_intermediate_state_1_tmp = aorai_intermediate_state_1;
aorai_intermediate_state_2_tmp = aorai_intermediate_state_2;
aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
- if (aorai_intermediate_state == 1) aorai_intermediate_state_3_tmp = 1;
- else
- if (aorai_intermediate_state_0 == 1) aorai_intermediate_state_3_tmp = 1;
- else
- if (aorai_intermediate_state_2 == 1)
- if (aorai_counter < 2) aorai_intermediate_state_3_tmp = 1;
- else aorai_intermediate_state_3_tmp = 0;
- else aorai_intermediate_state_3_tmp = 0;
- if (aorai_intermediate_state_2 == 1)
- if (aorai_counter < 2) aorai_counter ++;
+ if ((aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1) ||
+ aorai_intermediate_state_2 == 1 && aorai_counter < 2) aorai_intermediate_state_3_tmp = 1;
+ else aorai_intermediate_state_3_tmp = 0;
+ if (aorai_intermediate_state_2 == 1 && aorai_counter < 2) aorai_counter ++;
if (aorai_intermediate_state_0 == 1) aorai_counter = 1;
if (aorai_intermediate_state == 1) aorai_counter = 1;
aorai_intermediate_state_2_tmp = 0;
@@ -568,8 +562,7 @@ void g(void)
aorai_intermediate_state_1_tmp = 0;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
- if (aorai_intermediate_state_2 == 1)
- if (1 <= aorai_counter) Sf_tmp = 1; else Sf_tmp = 0;
+ if (aorai_intermediate_state_2 == 1 && 1 <= aorai_counter) Sf_tmp = 1;
else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
index 51f26c9c67fd769cf96b4a89a86f25d9f89cfaab..91097fdf88b9aa56ad5e7d32f14521e41cb9cbd8 100644
--- a/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/seq_loop.res.oracle
@@ -95,14 +95,10 @@ enum aorai_OpStatusList {
aorai_intermediate_state_3_tmp = aorai_intermediate_state_3;
aorai_intermediate_state_3_tmp = 0;
aorai_intermediate_state_2_tmp = 0;
- if (aorai_intermediate_state == 1) aorai_intermediate_state_1_tmp = 1;
- else
- if (aorai_intermediate_state_0 == 1)
- if (aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
- else aorai_intermediate_state_1_tmp = 0;
- else aorai_intermediate_state_1_tmp = 0;
- if (aorai_intermediate_state_0 == 1)
- if (aorai_counter < 5) aorai_counter ++;
+ if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1 &&
+ aorai_counter < 5) aorai_intermediate_state_1_tmp = 1;
+ else aorai_intermediate_state_1_tmp = 0;
+ if (aorai_intermediate_state_0 == 1 && aorai_counter < 5) aorai_counter ++;
if (aorai_intermediate_state == 1) aorai_counter = 1;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
@@ -543,9 +539,9 @@ void g(void)
aorai_intermediate_state_1_tmp = 0;
aorai_intermediate_state_0_tmp = 0;
aorai_intermediate_state_tmp = 0;
- if (aorai_intermediate_state == 1) Sf_tmp = 1;
- else
- if (aorai_intermediate_state_0 == 1) Sf_tmp = 1; else Sf_tmp = 0;
+ if (aorai_intermediate_state == 1 || aorai_intermediate_state_0 == 1)
+ Sf_tmp = 1;
+ else Sf_tmp = 0;
S0_tmp = 0;
S0 = S0_tmp;
Sf = Sf_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
index ee706aca96de2ada859ae369fa5c0e2003f97077..6ca094fa00c5447876ad01b5e9f2b6297b9ecbcd 100644
--- a/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/stack.res.oracle
@@ -204,8 +204,7 @@ void push(void)
{
aorai_CurOpStatus = aorai_Called;
aorai_CurOperation = op_pop;
- if (3 == aorai_CurStates)
- if (aorai_n > 0) aorai_CurStates = emptying_stack;
+ if (3 == aorai_CurStates && aorai_n > 0) aorai_CurStates = emptying_stack;
return;
}
@@ -258,21 +257,15 @@ void push(void)
{
aorai_CurOpStatus = aorai_Terminated;
aorai_CurOperation = op_pop;
- if (2 == aorai_CurStates) {
- if (aorai_n == 1) {
- aorai_CurStates = empty_stack;
+ if (2 == aorai_CurStates && aorai_n == 1) {
+ aorai_CurStates = empty_stack;
+ aorai_n --;
+ }
+ else
+ if (2 == aorai_CurStates && aorai_n > 1) {
+ aorai_CurStates = filled_stack;
aorai_n --;
}
- else goto _LAND;
- }
- else {
- _LAND: ;
- if (2 == aorai_CurStates)
- if (aorai_n > 1) {
- aorai_CurStates = filled_stack;
- aorai_n --;
- }
- }
return;
}
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
index 2f0841a21006211b9a4f313bf10bf689d197d285..89553036d1a684d71bccedc4dc525fe7dbcb2ed1 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params.res.oracle
@@ -76,9 +76,7 @@ int rr = 1;
SF_tmp = 0;
S4_tmp = 0;
S3_tmp = 0;
- if (S1 == 1)
- if (i >= 0) S2_tmp = 1; else S2_tmp = 0;
- else S2_tmp = 0;
+ if (S1 == 1 && i >= 0) S2_tmp = 1; else S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
S2 = S2_tmp;
@@ -293,9 +291,7 @@ void opa(int i, int j)
SF_tmp = SF;
mainst_tmp = mainst;
mainst_tmp = 0;
- if (S4 == 1)
- if (res > 0) SF_tmp = 1; else SF_tmp = 0;
- else SF_tmp = 0;
+ if (S4 == 1 && res > 0) SF_tmp = 1; else SF_tmp = 0;
S4_tmp = 0;
S3_tmp = 0;
S2_tmp = 0;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
index 14191d7f00b8e8d5cd13f1a5f7842b00c44a3c4b..16997723976399ec7e581375b99d0be6dc37e33e 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_acces_params2.res.oracle
@@ -82,9 +82,7 @@ int rr = 1;
S6_tmp = 0;
S5_tmp = 0;
S4_tmp = 0;
- if (S2 == 1)
- if (r >= 0) S3_tmp = 1; else S3_tmp = 0;
- else S3_tmp = 0;
+ if (S2 == 1 && r >= 0) S3_tmp = 1; else S3_tmp = 0;
S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
@@ -156,9 +154,7 @@ int rr = 1;
S7_tmp = 0;
S6_tmp = 0;
S5_tmp = 0;
- if (S3 == 1)
- if (res <= 5000) S4_tmp = 1; else S4_tmp = 0;
- else S4_tmp = 0;
+ if (S3 == 1 && res <= 5000) S4_tmp = 1; else S4_tmp = 0;
S3_tmp = 0;
S2_tmp = 0;
S1_tmp = 0;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
index 862eecf00b3d95eabb6ff90430a634d16d8f3a2d..6bd1a0b39b8010458503b8e83ae36ac33f416ecf 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_boucle_rechercheTableau.res.oracle
@@ -97,13 +97,9 @@ enum aorai_OpStatusList {
End_tmp = End;
Idle_tmp = Idle;
WillDoFoo_tmp = WillDoFoo;
- if (Idle == 1)
- if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
- else WillDoFoo_tmp = 0;
+ if (Idle == 1 && res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
Idle_tmp = 0;
- if (Idle == 1)
- if (res != -1) End_tmp = 1; else End_tmp = 0;
- else End_tmp = 0;
+ if (Idle == 1 && res != -1) End_tmp = 1; else End_tmp = 0;
End = End_tmp;
Idle = Idle_tmp;
WillDoFoo = WillDoFoo_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
index d3c59bb4befd891ca4a21f07b24c760adc8df894..43699ce9ec7abf7b39c5d535b758c4b7e908d813 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_factorial.res.oracle
@@ -216,9 +216,7 @@ int decode_int(char *s)
S2_tmp = S2;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1) S2_tmp = 1;
- else
- if (S2 == 1) S2_tmp = 1; else S2_tmp = 0;
+ if (S1 == 1 || S2 == 1) S2_tmp = 1; else S2_tmp = 0;
S1_tmp = 0;
S1 = S1_tmp;
S2 = S2_tmp;
@@ -264,12 +262,8 @@ int decode_int(char *s)
S2_tmp = S2;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1) S2_tmp = 1;
- else
- if (S2 == 1) S2_tmp = 1; else S2_tmp = 0;
- if (S1 == 1) S1_tmp = 1;
- else
- if (S2 == 1) S1_tmp = 1; else S1_tmp = 0;
+ if (S1 == 1 || S2 == 1) S2_tmp = 1; else S2_tmp = 0;
+ if (S1 == 1 || S2 == 1) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
S2 = S2_tmp;
main_0 = main_0_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
index 6652049d8dd0807628419b6c351661b2da4ea857..cdfe4aba74bff1e589436adad382f28f9967766a 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion4.res.oracle
@@ -100,25 +100,11 @@ enum aorai_OpStatusList {
End_tmp = End;
Idle_tmp = Idle;
WillDoFoo_tmp = WillDoFoo;
- if (Idle == 1) {
- if (res == -1) WillDoFoo_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- if (WillDoFoo == 1)
- if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
- else WillDoFoo_tmp = 0;
- }
+ if (Idle == 1 && res == -1 || WillDoFoo == 1 && res == -1) WillDoFoo_tmp = 1;
+ else WillDoFoo_tmp = 0;
Idle_tmp = 0;
- if (End == 1) {
- if (res != -1) End_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (Idle == 1)
- if (res != -1) End_tmp = 1; else End_tmp = 0;
- else End_tmp = 0;
- }
+ if (End == 1 && res != -1 || Idle == 1 && res != -1) End_tmp = 1;
+ else End_tmp = 0;
End = End_tmp;
Idle = Idle_tmp;
WillDoFoo = WillDoFoo_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
index 059961889707d7edefa1fd55d1593761b0b071c2..bc9334eec11d7af2e8fcb00eb21f5fb24d1a832f 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_recursion5.res.oracle
@@ -123,24 +123,10 @@ enum aorai_OpStatusList {
Idle_tmp = Idle;
IgnoreFoo_tmp = IgnoreFoo;
WillDoFoo_tmp = WillDoFoo;
- if (Idle == 1) {
- if (res == -1) WillDoFoo_tmp = 1; else goto _LAND;
- }
- else {
- _LAND: ;
- if (WillDoFoo == 1)
- if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
- else WillDoFoo_tmp = 0;
- }
- if (Idle == 1) {
- if (res != -1) IgnoreFoo_tmp = 1; else goto _LAND_0;
- }
- else {
- _LAND_0: ;
- if (IgnoreFoo == 1)
- if (res != -1) IgnoreFoo_tmp = 1; else IgnoreFoo_tmp = 0;
- else IgnoreFoo_tmp = 0;
- }
+ if (Idle == 1 && res == -1 || WillDoFoo == 1 && res == -1) WillDoFoo_tmp = 1;
+ else WillDoFoo_tmp = 0;
+ if (Idle == 1 && res != -1 || IgnoreFoo == 1 && res != -1) IgnoreFoo_tmp = 1;
+ else IgnoreFoo_tmp = 0;
Idle_tmp = 0;
End_tmp = 0;
End = End_tmp;
@@ -292,14 +278,11 @@ int isPresentRec(int *t, int i, int max, int val)
Idle_tmp = Idle;
IgnoreFoo_tmp = IgnoreFoo;
WillDoFoo_tmp = WillDoFoo;
- if (WillDoFoo == 1)
- if (res == -1) WillDoFoo_tmp = 1; else WillDoFoo_tmp = 0;
+ if (WillDoFoo == 1 && res == -1) WillDoFoo_tmp = 1;
else WillDoFoo_tmp = 0;
IgnoreFoo_tmp = 0;
Idle_tmp = 0;
- if (IgnoreFoo == 1)
- if (res != -1) End_tmp = 1; else End_tmp = 0;
- else End_tmp = 0;
+ if (IgnoreFoo == 1 && res != -1) End_tmp = 1; else End_tmp = 0;
End = End_tmp;
Idle = Idle_tmp;
IgnoreFoo = IgnoreFoo_tmp;
diff --git a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
index 0916e902014b3cb6b3c85b722d2a0b894c791b12..0e102ceda9633ce37d9262207c569e610ce0a69b 100644
--- a/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
+++ b/src/plugins/aorai/tests/ya/oracle/test_struct.res.oracle
@@ -47,9 +47,7 @@ int myAge = 0;
S1_tmp = S1;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1)
- if (nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
- else S1_tmp = 0;
+ if (S1 == 1 && nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
main_0 = main_0_tmp;
return;
@@ -84,9 +82,7 @@ int myAge = 0;
S1_tmp = S1;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1)
- if (nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
- else S1_tmp = 0;
+ if (S1 == 1 && nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
main_0 = main_0_tmp;
return;
@@ -138,9 +134,7 @@ void increment(void)
S1_tmp = S1;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (main_0 == 1)
- if (nobody.Age == 0) S1_tmp = 1; else S1_tmp = 0;
- else S1_tmp = 0;
+ if (main_0 == 1 && nobody.Age == 0) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
main_0 = main_0_tmp;
return;
@@ -175,9 +169,7 @@ void increment(void)
S1_tmp = S1;
main_0_tmp = main_0;
main_0_tmp = 0;
- if (S1 == 1)
- if (nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
- else S1_tmp = 0;
+ if (S1 == 1 && nobody.Age == 1) S1_tmp = 1; else S1_tmp = 0;
S1 = S1_tmp;
main_0 = main_0_tmp;
return;