diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle index 3e32676531171339c4abaa8fc6cc16846c252ecc..22064c851cd062a80ea9366ae6fbe6eddcaee5d7 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.0.res.oracle @@ -165,7 +165,7 @@ Assume { is_sint32(x_4) /\ is_sint32(x_5) /\ is_sint32(x_6) /\ is_sint32(x_7). (* Heap *) Type: (region(a.base) <= 0) /\ (region(r.base) <= 0). - (* Pre-condition *) + (* Pre-condition 'KO' *) Have: P_OBS(x, x_1, x_2). } Prove: P_OBS(x_5, x_6, x_7). diff --git a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle index 7f6f4e1316280036e5df8c8d578bbb2b5e487f1b..2801d3fd0e5afd585bb844ef63230ad83c9c7b30 100644 --- a/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle +++ b/src/plugins/wp/tests/wp_usage/oracle/caveat.1.res.oracle @@ -62,7 +62,7 @@ Let x_4 = x + x_1. Assume { Type: is_sint32(r) /\ is_sint32(x) /\ is_sint32(x_1) /\ is_sint32(x_2) /\ is_sint32(x_3) /\ is_sint32(x_4). - (* Pre-condition *) + (* Pre-condition 'KO' *) Have: P_OBS(x, x_1, r). } Prove: P_OBS(x_2, x_3, x_4).