diff --git a/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle b/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
index 06a4d869938de65e099b171b75d1b271aba60306..7b055f9626f0534549a3ffb75d39d3a6296d29fa 100644
--- a/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
+++ b/src/plugins/wp/tests/wp/oracle/wp_behav.res.oracle
@@ -163,7 +163,7 @@ Goal Preservation of Invariant 'qed_ok' (file wp_behav.c, line 81):
Assume {
Type: is_sint32(i) /\ is_sint32(n) /\ is_sint32(n_1).
(* Goal *)
- When: (0 <= i_1) /\ (i_1 <= i) /\ is_sint32(i_1).
+ When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: n_1 <= 9.
(* Invariant 'qed_ok' *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
index 17f0f3c5cb5a6b4af5b955af99c78f0a485efff9..6a44c5e64ba56925531942883fe890a7f127c378 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/axioms.res.oracle
@@ -112,7 +112,7 @@ Assume {
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (a <= i_1) /\ (i_1 <= i) /\ is_sint32(i_1).
+ When: (a <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, 1 + b - a).
(* Pre-condition *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
index b96c22a4802901437a86971598da3714e9176bf1..e3393701a39b16a09cf88c4f8cccd6b4f1c74752 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/simpl_is_type.res.oracle
@@ -207,7 +207,7 @@ Assume {
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
- When: (0 <= i_1) /\ (i_1 < size_0) /\ is_sint32(i_1).
+ When: (0 <= i_1) /\ (i_1 < size_0).
(* Pre-condition *)
Have: 0 < size_0.
(* Invariant *)
@@ -269,7 +269,7 @@ Assume {
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
- When: (0 <= i_1) /\ (i_1 <= i) /\ is_sint32(i_1).
+ When: (0 <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: 0 < size_0.
(* Invariant *)
@@ -308,7 +308,7 @@ Assume {
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
- When: (i_1 < size_0) /\ (i < i_1) /\ is_sint32(i_1).
+ When: (i_1 < size_0) /\ (i < i_1).
(* Pre-condition *)
Have: 0 < size_0.
(* Invariant *)
@@ -340,7 +340,7 @@ Assume {
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
- When: (0 <= i) /\ (i < size_0) /\ is_sint32(i).
+ When: (0 <= i) /\ (i < size_0).
(* Pre-condition *)
Have: forall i_1 : Z. ((0 <= i_1) -> ((i_1 < size_0) ->
(Mint_0[shift_sint32(t, i_1)] < 0))).
@@ -457,7 +457,7 @@ Assume {
(* Heap *)
Type: region(t.base) <= 0.
(* Goal *)
- When: (0 <= i) /\ (i <= i_1) /\ is_sint32(i).
+ When: (0 <= i) /\ (i <= i_1).
(* Pre-condition *)
Have: 0 < size_0.
(* Invariant *)
diff --git a/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle b/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle
index cd6729ea2d5b979d9cf3e4b7439032f6a16aa32b..f444ed8fb1be46b98d9ba39559eabbf7004d6620 100644
--- a/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle
+++ b/src/plugins/wp/tests/wp_acsl/oracle/unit_bit_test.res.oracle
@@ -16,7 +16,7 @@ Let x_1 = lsr(x, 31).
Assume {
Type: is_uint32(x) /\ is_uint32(x_1).
(* Goal *)
- When: (0 <= i) /\ (i <= 30) /\ is_sint32(i).
+ When: (0 <= i) /\ (i <= 30).
}
Prove: (land(lor(x_1, to_uint32(lsl(x, 1))), lsl(1, 1 + i)) != 0) <->
(land(x, lsl(1, i)) != 0).
diff --git a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
index 2bbbd17af44cf460bbbc0b1e8d1139e9df2fbf38..a9679b500c90b55ba77f83446cce7da4423edf0c 100644
--- a/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
+++ b/src/plugins/wp/tests/wp_gallery/oracle_qualif/binary-multiplication.0.session/script/BinaryMultiplication_loop_invariant_inv1_ok_preserved.json
@@ -1,7 +1,7 @@
[ { "header": "Range", "tactic": "Wp.range",
"params": { "inf": 0, "sup": 1 },
- "select": { "select": "inside-step", "at": 17, "kind": "have",
- "occur": 0, "target": "b_3 mod 2", "pattern": "%$b2" },
+ "select": { "select": "inside-step", "at": 18, "kind": "have",
+ "occur": 0, "target": "b_1 mod 2", "pattern": "%$b2" },
"children": { "Lower 0": [ { "header": "Overflow",
"tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-goal",
@@ -10,52 +10,52 @@
"pattern": "to_uint64.2$x" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 6.9304,
+ "time": 5.0522,
"steps": 47 } ],
"Lower": [ { "prover": "qed",
"verdict": "valid" } ],
"Upper": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 5.6793,
+ "time": 4.8984,
"steps": 48 } ] } } ],
"Value 0": [ { "header": "Overflow",
"tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-step",
"at": 3, "kind": "have",
"occur": 0,
- "target": "(to_uint64 (a_1*b_1))",
+ "target": "(to_uint64 (a_1*b_3))",
"pattern": "to_uint64*$a$b" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 6.3679,
- "steps": 184 } ],
+ "time": 5.0366,
+ "steps": 181 } ],
"Lower": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 5.8854,
+ "time": 4.9686,
"steps": 42 } ],
"Upper": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 6.2747,
+ "time": 4.9181,
"steps": 42 } ] } } ],
"Value 1": [ { "header": "Overflow",
"tactic": "Wp.overflow", "params": {},
"select": { "select": "inside-step",
"at": 3, "kind": "have",
"occur": 0,
- "target": "(to_uint64 (a_1*b_1))",
+ "target": "(to_uint64 (a_1*b_3))",
"pattern": "to_uint64*$a$b" },
"children": { "In-Range": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 6.9832,
- "steps": 222 } ],
+ "time": 5.0078,
+ "steps": 218 } ],
"Lower": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 6.0791,
+ "time": 4.7914,
"steps": 45 } ],
"Upper": [ { "prover": "Alt-Ergo:2.2.0",
"verdict": "valid",
- "time": 5.1665,
+ "time": 4.8087,
"steps": 45 } ] } } ],
"Upper 1": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 6.0617,
+ "verdict": "valid", "time": 4.9897,
"steps": 48 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle
index 13ce327181d2578f82c4d34b8708521ed3719056..8204ab6fa7850bb613a937f6dace22ade03d88ae 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/cint.3.res.oracle
@@ -18,8 +18,7 @@ Prove: P_R(x, a).
------------------------------------------------------------
Goal Post-condition (file cint.i, line 30) in 'signed_downcast':
-Assume { Type: is_sint16(signed_downcast_0) /\ is_sint32(signed_downcast_0).
-}
+Assume { Type: is_sint16(signed_downcast_0). }
Prove: P_R(signed_downcast_0, signed_downcast_0).
------------------------------------------------------------
diff --git a/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
index b346927e4d3c79a87ddca0d6d4f7969962483b14..b35e3645528169c24136512ccd5b11a3779230c7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
+++ b/src/plugins/wp/tests/wp_plugin/oracle/loop.res.oracle
@@ -16,7 +16,7 @@ Assume {
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (i_1 <= b) /\ (a <= i_1) /\ is_sint32(i_1).
+ When: (i_1 <= b) /\ (a <= i_1).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, 1 + b - a).
(* Pre-condition *)
@@ -87,7 +87,7 @@ Assume {
(* Heap *)
Type: (region(t.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (a <= i_1) /\ (i_1 <= i) /\ is_sint32(i_1).
+ When: (a <= i_1) /\ (i_1 <= i).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, 1 + b - a).
(* Pre-condition *)
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json
index c1f541d00af218c3a2c837305606b0681f1e9f7d..ce1db3baf849bcda6d5c7bc45ce2fad9d913cc87 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_n.json
@@ -4,5 +4,5 @@
"pattern": "!bit_test$off15" },
"children": { "Bit #15 (inf)": [ { "prover": "qed", "verdict": "valid" } ],
"Bit #15 (sup)": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0263,
+ "verdict": "valid", "time": 0.0174,
"steps": 32 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json
index 95cf3e5f2953bc7ed7b6c9ad5939b20299677781..6efc632858bf4117e91e9c9f8cb43ca24a57fcc7 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/bitmask0x8000.0.session/script/lemma_res_y.json
@@ -3,6 +3,6 @@
"target": "(bit_test off_0 15)",
"pattern": "bit_test$off15" },
"children": { "Bit #15 (inf)": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0129,
+ "verdict": "valid", "time": 0.0166,
"steps": 32 } ],
"Bit #15 (sup)": [ { "prover": "qed", "verdict": "valid" } ] } } ]
diff --git a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/script/unrolled_loop_ensures_zero.json b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/script/unrolled_loop_ensures_zero.json
index 1c97c0efd6fc200100d43ffe2b726792238d7235..fee182f4fb27d5d514f2a00bb1ea971d893a4636 100644
--- a/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/script/unrolled_loop_ensures_zero.json
+++ b/src/plugins/wp/tests/wp_plugin/oracle_qualif/unroll.0.session/script/unrolled_loop_ensures_zero.json
@@ -1,6 +1,6 @@
[ { "header": "Definition", "tactic": "Wp.unfold", "params": {},
"select": { "select": "clause-goal",
- "target": "(P_zeroed\n Mint_37[(shift_uint32 t_2 0)->0][(shift_uint32 t_2 1)->0]\n [(shift_uint32 t_2 2)->0][(shift_uint32 t_2 3)->0][(shift_uint32 t_2 4)\n ->0][(shift_uint32 t_2 5)->0][(shift_uint32 t_2 6)->0]\n [(shift_uint32 t_2 7)->0][(shift_uint32 t_2 8)->0][(shift_uint32 t_2 9)\n ->0][(shift_uint32 t_2 10)->0][(shift_uint32 t_2 11)->0]\n [(shift_uint32 t_2 12)->0][(shift_uint32 t_2 13)->0]\n [(shift_uint32 t_2 14)->0][(shift_uint32 t_2 15)->0] t_2 0 15)",
+ "target": "(P_zeroed\n Mint_37[(shift_uint32 t_0 0)->0][(shift_uint32 t_0 1)->0]\n [(shift_uint32 t_0 2)->0][(shift_uint32 t_0 3)->0][(shift_uint32 t_0 4)\n ->0][(shift_uint32 t_0 5)->0][(shift_uint32 t_0 6)->0]\n [(shift_uint32 t_0 7)->0][(shift_uint32 t_0 8)->0][(shift_uint32 t_0 9)\n ->0][(shift_uint32 t_0 10)->0][(shift_uint32 t_0 11)->0]\n [(shift_uint32 t_0 12)->0][(shift_uint32 t_0 13)->0]\n [(shift_uint32 t_0 14)->0][(shift_uint32 t_0 15)->0] t_0 0 15)",
"pattern": "P_zeroed[=]$t015[=]shift_uint320" },
"children": { "Unfold 'P_zeroed'": [ { "header": "Range",
"tactic": "Wp.range",
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
index 2a359dbab3ad22d87d88d11534edd84db6f4497e..77a4f51c832cb8e9d049e59dd20d0b4644788ff9 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/induction.0.session/script/lemma_ByInd.json
@@ -3,10 +3,10 @@
"select": { "select": "inside-goal", "occur": 0, "target": "(L_f x_0)",
"pattern": "L_f$x" },
"children": { "Base": [ { "prover": "Alt-Ergo:2.2.0", "verdict": "valid",
- "time": 0.0047, "steps": 6 } ],
+ "time": 0.0074, "steps": 6 } ],
"Induction (sup)": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0041,
+ "verdict": "valid", "time": 0.0098,
"steps": 21 } ],
"Induction (inf)": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0054,
+ "verdict": "valid", "time": 0.0097,
"steps": 20 } ] } } ]
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json
index 9ca995ee6234769c156b30223f2b7d8dcb67e964..255539ba9f34b22d89852d5659ffc0969380c9f1 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_char.json
@@ -5,7 +5,7 @@
"verdict": "valid", "time": 0.0094,
"steps": 25 } ],
"Lower": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0238,
+ "verdict": "valid", "time": 0.0157,
"steps": 53 },
{ "header": "Overflow", "tactic": "Wp.overflow",
"params": {},
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json
index b07a89798751525300ec38be4ef5de65ee73b4cb..97c383396b0c68dc8ea302b5db23e1fe35c93227 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/overflow.0.session/script/lemma_j_incr_short.json
@@ -5,7 +5,7 @@
"verdict": "valid", "time": 0.0098,
"steps": 25 } ],
"Lower": [ { "prover": "Alt-Ergo:2.2.0",
- "verdict": "valid", "time": 0.0248,
+ "verdict": "valid", "time": 0.0198,
"steps": 54 },
{ "header": "Overflow", "tactic": "Wp.overflow",
"params": {},
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json
index 885feb947bdb3b276a90fc8d54f807ae6dd76e79..cadd5e501016b03034d1b6c4b5778d254468abcd 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_LEFT.json
@@ -1,5 +1,4 @@
-[ { "prover": "script", "verdict": "valid" },
- { "header": "Sequence", "tactic": "Wp.sequence",
+[ { "header": "Sequence", "tactic": "Wp.sequence",
"params": { "seq.side": "left" },
"select": { "select": "inside-goal", "occur": 0,
"target": "(repeat a_0 n_0)", "pattern": "repeat$a$n" },
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json
index 75e4064cdb6eb792772488a295e01855174a6132..2c6b678d138d5ffc43f3394c72fe508f44b8b8ec 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_RIGHT.json
@@ -1,5 +1,4 @@
-[ { "prover": "script", "verdict": "valid" },
- { "header": "Sequence", "tactic": "Wp.sequence",
+[ { "header": "Sequence", "tactic": "Wp.sequence",
"params": { "seq.side": "right" },
"select": { "select": "inside-goal", "occur": 0,
"target": "(repeat a_0 n_0)", "pattern": "repeat$a$n" },
diff --git a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json
index 65a87aa59ca69040135319b35d107a49d773886a..60f8f7acd6cea516bf05aa93a1b4cdc243f49e83 100644
--- a/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json
+++ b/src/plugins/wp/tests/wp_tip/oracle_qualif/unroll.0.session/script/lemma_SUM.json
@@ -1,5 +1,4 @@
-[ { "prover": "script", "verdict": "valid" },
- { "header": "Sequence", "tactic": "Wp.sequence",
+[ { "header": "Sequence", "tactic": "Wp.sequence",
"params": { "seq.side": "sum" },
"select": { "select": "inside-goal", "occur": 0,
"target": "(repeat a_0 (p_0+q_0))",
diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
index 207e9befdb79fe21441383cf88a6bebadced293d..91d993407e90198cfac7642dd37c622a3ba79925 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.0.res.oracle
@@ -64,7 +64,7 @@ Goal Post-condition (file cast_fits.i, line 37) in 'fits4':
Let x = Mchar_0[shiftfield_F6_c6(p)].
Let x_1 = Mchar_0[shiftfield_F3_c3(shift_S3(shiftfield_F5_ci5(p), 1))].
Assume {
- Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1).
+ Type: is_sint8(x) /\ is_sint8(x_1).
(* Heap *)
Type: (region(p.base) <= 0) /\ sconst(Mchar_0).
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
index f456415436e1c7639e50fead09a66a353db816f1..76f3b9532f3c8ba5cf43aac5657b1af1bfd9d1c9 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/cast_fits.1.res.oracle
@@ -64,7 +64,7 @@ Goal Post-condition (file cast_fits.i, line 37) in 'fits4':
Let x = Mchar_0[shiftfield_F6_c6(p)].
Let x_1 = Mchar_0[shiftfield_F3_c3(shift_S3(shiftfield_F5_ci5(p), 1))].
Assume {
- Type: is_sint8(x) /\ is_sint32(x) /\ is_sint8(x_1).
+ Type: is_sint8(x) /\ is_sint8(x_1).
(* Heap *)
Type: (region(p.base) <= 0) /\ sconst(Mchar_0).
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle
index 3161feeff647794efb090e0c7c0f7395ff304a68..652ab955538806f8246c98cc19cc31858a25b954 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.0.res.oracle
@@ -31,7 +31,7 @@ Assume {
(* Heap *)
Type: region(p.base) <= 0.
(* Goal *)
- When: (0 <= i) /\ (i <= 9) /\ is_sint32(i).
+ When: (0 <= i) /\ (i <= 9).
(* Pre-condition *)
Have: P_inv(Mint_0, p).
(* Assertion *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle
index 67d2f08869b917c50e09654bbfbf7710c24b16eb..62c3c4fdabf0c30991d0dc18e9945ba998b981aa 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/shift_lemma.1.res.oracle
@@ -31,7 +31,7 @@ Assume {
(* Heap *)
Type: region(p.base) <= 0.
(* Goal *)
- When: (0 <= i) /\ (i <= 9) /\ is_sint32(i).
+ When: (0 <= i) /\ (i <= 9).
(* Pre-condition *)
Have: P_inv(Mint_0, p).
(* Assertion *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
index ea0127e5c7dd06b90b62a784d82ab37136ae8a31..6f871cd6fc4d62ac24e925302c564e5ac6df812a 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_bitwise.0.res.oracle
@@ -16,7 +16,7 @@ Let x_1 = lsr(x, 31).
Assume {
Type: is_uint32(x) /\ is_uint32(x_1).
(* Goal *)
- When: (0 <= i) /\ (i <= 30) /\ is_sint32(i).
+ When: (0 <= i) /\ (i <= 30).
}
Prove: (land(lor(x_1, to_uint32(lsl(x, 1))), lsl(1, 1 + i)) != 0) <->
(land(x, lsl(1, i)) != 0).
@@ -32,7 +32,7 @@ Let x_2 = lsr(x, 32 - n).
Assume {
Type: is_uint32(x) /\ is_sint32(n) /\ is_uint32(x_2).
(* Goal *)
- When: (0 <= i) /\ (i < n) /\ is_sint32(i).
+ When: (0 <= i) /\ (i < n).
(* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 31).
}
@@ -65,7 +65,7 @@ Let x_2 = lsr(x, 64 - n).
Assume {
Type: is_sint32(n) /\ is_uint64(x) /\ is_uint64(x_2).
(* Goal *)
- When: (0 <= i) /\ (i < n) /\ is_sint32(i).
+ When: (0 <= i) /\ (i < n).
(* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 63).
}
@@ -103,7 +103,7 @@ Let x_1 = lsr(x, 1).
Assume {
Type: is_uint32(x) /\ is_uint32(x_1).
(* Goal *)
- When: (0 <= i) /\ (i <= 30) /\ is_sint32(i).
+ When: (0 <= i) /\ (i <= 30).
}
Prove: (land(lor(x_1, to_uint32(lsl(x, 31))), lsl(1, i)) != 0) <->
(land(x, lsl(1, 1 + i)) != 0).
@@ -119,7 +119,7 @@ Let x_2 = -n.
Assume {
Type: is_uint32(x) /\ is_sint32(n) /\ is_uint32(x_1).
(* Goal *)
- When: (0 <= i) /\ (i < n) /\ is_sint32(i).
+ When: (0 <= i) /\ (i < n).
(* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 31).
}
@@ -152,7 +152,7 @@ Let x_2 = -n.
Assume {
Type: is_sint32(n) /\ is_uint64(x) /\ is_uint64(x_1).
(* Goal *)
- When: (0 <= i) /\ (i < n) /\ is_sint32(i).
+ When: (0 <= i) /\ (i < n).
(* Pre-condition 'r' *)
Have: (0 < n) /\ (n <= 63).
}
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
index 3941f8836e33495cea3f23d2e0b01ce118191efc..85d5372254429bead901a25a73e88c6565d6b25c 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.0.res.oracle
@@ -18,7 +18,7 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (0 <= i_1) /\ (i_1 < n) /\ is_sint32(i_1).
+ When: (0 <= i_1) /\ (i_1 < n).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, n).
(* Invariant 'Range' *)
@@ -43,7 +43,7 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (i_1 <= i) /\ (0 <= i_1) /\ is_sint32(i_1).
+ When: (i_1 <= i) /\ (0 <= i_1).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, n).
(* Invariant 'Range' *)
diff --git a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
index df2b7d55d13f031670627d5d6f609d33a08926eb..2abe7e2f668fd269d0ed35cdab8c23f4125e9515 100644
--- a/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
+++ b/src/plugins/wp/tests/wp_typed/oracle/user_init.1.res.oracle
@@ -18,7 +18,7 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (0 <= i_1) /\ (i_1 < n) /\ is_sint32(i_1).
+ When: (0 <= i_1) /\ (i_1 < n).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, n).
(* Invariant 'Range' *)
@@ -43,7 +43,7 @@ Assume {
(* Heap *)
Type: (region(a.base) <= 0) /\ linked(Malloc_0).
(* Goal *)
- When: (i_1 <= i) /\ (0 <= i_1) /\ is_sint32(i_1).
+ When: (i_1 <= i) /\ (0 <= i_1).
(* Pre-condition *)
Have: valid_rw(Malloc_0, a_1, n).
(* Invariant 'Range' *)