[wp] test for issue 751 fixed

src/plugins/wp/tests/wp_bts/oracle/issue_751.res.oracle

@@ -9,13 +9,14 @@
 
 Goal Preservation of Invariant 'RANGE' (file tests/wp_bts/issue_751.i, line 7):
 Let x = land(3840, R).
-Let x_1 = lsr(x, 8).
+Let x_1 = x / 256.
 Assume {
-  Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(1 + j) /\ is_sint32(x_1).
+  Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(1 + j) /\
+      is_sint32(lsr(x, 8)).
   (* Heap *)
   Have: (region(Data_0.base) <= 0) /\ linked(Malloc_0).
   (* Pre-condition *)
-  Have: (0 < x) /\ (2048 <= x).
+  Have: (0 < x) /\ (x <= 2303).
   (* Invariant 'RANGE' *)
   Have: (0 <= j) /\ (j <= x_1).
   (* Then *)
@@ -38,15 +39,15 @@ Prove: true.
 Goal Loop assigns (file tests/wp_bts/issue_751.i, line 8) (2/2):
 Effect at line 11
 Let x = land(3840, R).
-Let x_1 = lsr(x, 8).
+Let x_1 = x / 256.
 Assume {
-  Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(x_1).
+  Type: is_sint32(R) /\ is_sint32(j) /\ is_sint32(lsr(x, 8)).
   (* Goal *)
   When: !invalid(Malloc_0, shift_sint32(Data_0, j), 1).
   (* Heap *)
   Have: (region(Data_0.base) <= 0) /\ linked(Malloc_0).
   (* Pre-condition *)
-  Have: (0 < x) /\ (2048 <= x).
+  Have: (0 < x) /\ (x <= 2303).
   (* Invariant 'RANGE' *)
   Have: (0 <= j) /\ (j <= x_1).
   (* Then *)

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.0.session/cache/b5cd216729c3d1203bcb827ee2b80455.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0322,
+  "steps": 47 }

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.0.session/cache/cd5789bbf79065dc289bd8b960a11c23.json

+{ "prover": "why3:Alt-Ergo,2.0.0", "verdict": "valid", "time": 0.0229,
+  "steps": 26 }

src/plugins/wp/tests/wp_bts/oracle_qualif/issue_751.res.oracle

@@ -7,11 +7,11 @@
 [wp] [Alt-Ergo 2.0.0] Goal typed_acquire_loop_invariant_RANGE_preserved : Valid
 [wp] [Qed] Goal typed_acquire_loop_invariant_RANGE_established : Valid
 [wp] [Qed] Goal typed_acquire_loop_assigns_part1 : Valid
-[wp] [Alt-Ergo 2.0.0] Goal typed_acquire_loop_assigns_part2 : Unsuccess
-[wp] Proved goals:    3 / 4
+[wp] [Alt-Ergo 2.0.0] Goal typed_acquire_loop_assigns_part2 : Valid
+[wp] Proved goals:    4 / 4
   Qed:               2 
-  Alt-Ergo 2.0.0:    1  (unsuccess: 1)
+  Alt-Ergo 2.0.0:    2
 ------------------------------------------------------------
  Functions                 WP     Alt-Ergo  Total   Success
-  acquire                   2        1        4      75.0%
+  acquire                   2        2        4       100%
 ------------------------------------------------------------