type addr = { base : int; offset : int
}

function shift(p: addr, k: int) : addr = { base = (p).base; offset =
  ((p).offset + k) }

predicate valid_rd(m: (int,int) farray, p: addr, n: int) = ((0 <  n) ->
  ((0 <= (p).offset) and (((p).offset + n) <= (m[(p).base]))))

logic region : int -> int

logic linked : (int,int) farray -> prop

function shift_sint32(p:addr, k:int) : addr = shift(p, k)

logic is_uint32 : int -> prop

axiom is_uint32_def :
  (forall x:int [is_uint32(x)]. (is_uint32(x) -> (0 <= x)))

logic is_sint32 : int -> prop

logic to_uint32 : int -> int

logic to_uint : int, int -> int

predicate P_ConstantRange
    (Mint_0: (addr,int) farray,
    a: addr,
    first_0: int,
    last_0: int,
    val_0: int) =
    forall i: int. (first_0 <= i) -> (i < last_0) ->
    (Mint_0[shift_sint32(a, i)] = val_0)

predicate P_HasConstantSubRange
    (Mint_0: (addr,int) farray,
    a: addr,
    m: int,
    n: int,
    b: int) =
    exists i: int.
    let x = (n + i): int in
    (0 <= i) and (x <= m) and
    P_ConstantRange(Mint_0, a, i, x, b)

axiom Q_HasConstantSubRangeSizes:
  forall a: addr.
  forall Mint_0: (addr,int) farray.
  forall m,n,v: int.
  is_sint32(v) -> P_HasConstantSubRange(Mint_0, a, m, n, v) -> (n <= m)

(* goal taken from file xxx_via_why3.mlw: *)
goal WP :
  (forall i_7:int. forall i_6:int. forall i_5:int. forall i_4:int.
  forall i_3:int. forall i_2:int. forall i_1:int. forall i:int.
  (forall t:(int,int) farray.
  (forall t_1:(addr,int) farray.
  (forall a:addr. ((region((a).base) <= 0) -> (linked(t) -> (is_uint32(i) ->
  (is_uint32(i_1) -> (is_uint32(i_2) -> (is_uint32(i_3) -> (is_uint32(i_4) ->
  (is_uint32(i_5) -> (is_uint32(i_6) -> (is_sint32(i_7) ->
  ((not P_HasConstantSubRange(t_1, a, i_4, i_2, i_7)) -> (valid_rd(t,
  shift(a, 0), i_4) -> (is_sint32((t_1[shift(a, (i - 1))])) ->
  ((((0 <  i_2) and (((i_2 <= i_4) and ((i_4 = i_3) and ((i_5 = i_3) and
  ((i_5 = i_4) and ((i <= (1 + i_6)) and (P_ConstantRange(t_1, a, i, i_6,
  i_7) and ((not P_HasConstantSubRange(t_1, a, i_6, i_2, i_7)) and
  ((((i_6 <  i_4) and ((i_1 = i) and (((i_1 + i_2) = (1 + i_6)) and
  (((t_1[shift(a, ((i_1 + i_2) - 1))]) = i_7) and
  ((i_1 <= to_uint32((i_1 + i_2))) and (((i_1 + i_2) <= 4294967295) and
  ((to_uint32((i_1 + i_2)) <= (4294967295 + i_1)) and valid_rd(t, shift(a,
  ((i_1 + i_2) - 1)), 1)))))))) or ((not (i_6 <  i_4)) and (i_4 = i_1))) and
  ((0 <  i) -> (not ((t_1[shift(a, (i - 1))]) = i_7))))))))))) or
  ((not (i_2 <= i_4)) and (i_4 = i_1)))) or ((not (0 <  i_2)) and
  (i_1 = 0))) -> (i_4 = i_1)))))))))))))))))))


(* (* original goal: *)
goal search_n_no_match_post_result_xxx:
  forall i_7,i_6,i_5,i_4,i_3,i_2,i_1,i : int.
  forall t : int farray.
  forall t_1 : (addr,int) farray.
  forall a : addr.
  let x = t_1[shift_sint32(a, i - 1)] : int in
  let x_1 = (1 + i_6) : int in
  let x_2 = (i_1 + i_2) : int in
  let a_1 = shift_sint32(a, i_1 + i_2 - 1) : addr in
  let x_3 = to_uint32(x_2) : int in
  (region(a.base) <= 0) ->
  linked(t) ->
  is_uint32(i) ->
  is_uint32(i_1) ->
  is_uint32(i_2) ->
  is_uint32(i_3) ->
  is_uint32(i_4) ->
  is_uint32(i_5) ->
  is_uint32(i_6) ->
  is_sint32(i_7) ->
  (not P_HasConstantSubRange(t_1, a, i_4, i_2, i_7)) ->
  valid_rd(t, shift_sint32(a, 0), i_4) ->
  is_sint32(x) ->
  (((i_2 <= 0) -> (i_1 = 0)) and 
   ((0 < i_2) ->
    (((i_4 < i_2) -> (i_4 = i_1)) and 
     ((i_2 <= i_4) ->
      ((i_4 = i_3) and (i_5 = i_3) and (i_5 = i_4) and (i <= x_1) and 
       P_ConstantRange(t_1, a, i, i_6, i_7) and 
       (not P_HasConstantSubRange(t_1, a, i_6, i_2, i_7)) and 
       (((i_4 <= i_6) -> (i_4 = i_1)) and 
        ((i_6 < i_4) ->
         ((i_1 = i) and (x_2 = x_1) and (t_1[a_1] = i_7) and (i_1 <= x_3) and 
          (x_2 <= 4294967295) and (x_3 <= (4294967295 + i_1)) and
          valid_rd(t, a_1, 1)))) and ((0 < i) -> (x <> i_7))))))) ->
  (i_4 = i_1)
*)