structs-0.vpr

domain WellFoundedOrder[T]  {

  function bounded(v: T): Bool

  function decreasing(v1: T, v2: T): Bool
}

domain IntOrder  {

  axiom {
    (forall i: Int ::0 <= i == (bounded(i): Bool))
  }

  axiom {
    (forall i: Int ::(forall j: Int ::i < j == (decreasing(i, j): Bool)))
  }
}

domain Void  {

  function unit(): Void

  axiom {
    (forall v: Void ::true ==> unit() == v)
  }
}

domain Block  {

  function block_length(b: Block): Int

  function loc(b: Block, i: Int): Ref

  function loc_inv_1(r: Ref): Block

  function loc_inv_2(r: Ref): Int

  axiom {
    (forall b: Block ::block_length(b) >= 0)
  }

  axiom {
    (forall b: Block, i: Int ::
      { loc(b, i) }
      loc_inv_1(loc(b, i)) == b && loc_inv_2(loc(b, i)) == i)
  }
}

domain Pointer  {

  function pointer_of(b: Block, offset: Int): Pointer

  function pointer_block(p: Pointer): Block

  function pointer_offset(p: Pointer): Int

  function pointer_inv(r: Ref): Pointer

  axiom {
    (forall p: Pointer ::pointer_offset(p) >= 0 &&
      pointer_offset(p) < block_length(pointer_block(p)))
  }

  axiom {
    (forall b: Block, offset: Int ::
      { pointer_block(pointer_of(b, offset)), pointer_offset(pointer_of(b, offset)) }
      pointer_block(pointer_of(b, offset)) == b &&
      pointer_offset(pointer_of(b, offset)) == offset)
  }

  axiom {
    (forall r: Ref :: { pointer_inv(r) } ptrDeref(pointer_inv(r)) == r)
  }

  axiom {
    (forall p: Pointer :: { ptrDeref(p) } pointer_inv(ptrDeref(p)) == p)
  }
}

domain Point  {

  function index_point(pointer: Pointer): Int

  function x(x2: Point): Pointer

  function y(y1: Point): Pointer

  function inv_x(x2: Pointer): Point

  function inv_y(y1: Pointer): Point

  axiom {
    (forall i: Point, i1: Point ::
      { x(i), x(i1) }
      { y(i), y(i1) }
      (x(i) == x(i1) ==> i == i1) && (y(i) == y(i1) ==> i == i1))
  }

  axiom {
    (forall i: Point :: { x(i) } inv_x(x(i)) == i)
  }

  axiom {
    (forall i: Point :: { y(i) } inv_y(y(i)) == i)
  }

  axiom {
    (forall i: Point :: { x(i) } index_point(x(i)) == 0)
  }

  axiom {
    (forall i: Point :: { y(i) } index_point(y(i)) == 1)
  }

  axiom {
    (forall i: Point ::
      { (value_as_int(i): Pointer) }
      (value_as_int(i): Pointer) == x(i))
  }

  axiom {
    (forall i: Point ::
      { (value_as_int(i): Pointer) }
      (value_as_int(i): Pointer) == as_int(x(i)))
  }
}

domain Triangle  {

  function index_triangle(pointer: Pointer): Int

  function p_1(p1: Triangle): Pointer

  function p_2(p2: Triangle): Pointer

  function p_3(p3: Triangle): Pointer

  function inv_p1(p1: Pointer): Triangle

  function inv_p2(p2: Pointer): Triangle

  function inv_p3(p3: Pointer): Triangle

  axiom {
    (forall i: Triangle, i1: Triangle ::
      { p_1(i), p_1(i1) }
      { p_2(i), p_2(i1) }
      { p_3(i), p_3(i1) }
      (p_1(i) == p_1(i1) ==> i == i1) && (p_2(i) == p_2(i1) ==> i == i1) &&
      (p_3(i) == p_3(i1) ==> i == i1))
  }

  axiom {
    (forall i: Triangle :: { p_1(i) } inv_p1(p_1(i)) == i)
  }

  axiom {
    (forall i: Triangle :: { p_2(i) } inv_p2(p_2(i)) == i)
  }

  axiom {
    (forall i: Triangle :: { p_3(i) } inv_p3(p_3(i)) == i)
  }

  axiom {
    (forall i: Triangle :: { p_1(i) } index_triangle(p_1(i)) == 0)
  }

  axiom {
    (forall i: Triangle :: { p_2(i) } index_triangle(p_2(i)) == 1)
  }

  axiom {
    (forall i: Triangle :: { p_3(i) } index_triangle(p_3(i)) == 2)
  }

  axiom {
    (forall i: Triangle ::
      { (value_as_point_105093469(i): Pointer) }
      (value_as_point_105093469(i): Pointer) == p_1(i))
  }

  axiom {
    (forall i: Triangle ::
      { (value_as_int(i): Pointer) }
      (value_as_int(i): Pointer) == as_int(p_1(i)))
  }

  axiom {
    (forall i: Triangle ::
      { (value_as_point_105093469(i): Pointer) }
      (value_as_point_105093469(i): Pointer) == as_point_1003792263(p_1(i)))
  }
}

domain Polygon  {

  function index_polygon(pointer: Pointer): Int

  function ps(ps1: Polygon): Pointer

  function inv_ps(ps1: Pointer): Polygon

  axiom {
    (forall i: Polygon, i1: Polygon ::
      { ps(i), ps(i1) }
      ps(i) == ps(i1) ==> i == i1)
  }

  axiom {
    (forall i: Polygon :: { ps(i) } inv_ps(ps(i)) == i)
  }

  axiom {
    (forall i: Polygon :: { ps(i) } index_polygon(ps(i)) == 0)
  }

  axiom {
    (forall i: Polygon ::
      { (value_as_pointer_point_105093469_(i): Pointer) }
      (value_as_pointer_point_105093469_(i): Pointer) == ps(i))
  }

  axiom {
    (forall i: Polygon ::
      { (value_as_pointer_point_105093469_(i): Pointer) }
      (value_as_pointer_point_105093469_(i): Pointer) ==
      as_pointer_point_1003792263_(ps(i)))
  }
}

domain LinkedList  {

  function index_linked_list(pointer: Pointer): Int

  function p_4(p1: LinkedList): Pointer

  function x1(x2: LinkedList): Pointer

  function inv_p4(p1: Pointer): LinkedList

  function inv_x1(x2: Pointer): LinkedList

  axiom {
    (forall i: LinkedList, i1: LinkedList ::
      { p_4(i), p_4(i1) }
      { x1(i), x1(i1) }
      (p_4(i) == p_4(i1) ==> i == i1) && (x1(i) == x1(i1) ==> i == i1))
  }

  axiom {
    (forall i: LinkedList :: { p_4(i) } inv_p4(p_4(i)) == i)
  }

  axiom {
    (forall i: LinkedList :: { x1(i) } inv_x1(x1(i)) == i)
  }

  axiom {
    (forall i: LinkedList :: { p_4(i) } index_linked_list(p_4(i)) == 0)
  }

  axiom {
    (forall i: LinkedList :: { x1(i) } index_linked_list(x1(i)) == 1)
  }

  axiom {
    (forall i: LinkedList ::
      { (value_as_pointer_linkedlist_1912857409_(i): Pointer) }
      (value_as_pointer_linkedlist_1912857409_(i): Pointer) == p_4(i))
  }

  axiom {
    (forall i: LinkedList ::
      { (value_as_pointer_linkedlist_1912857409_(i): Pointer) }
      (value_as_pointer_linkedlist_1912857409_(i): Pointer) ==
      as_pointer_linkedlist_559086864_(p_4(i)))
  }
}

domain Any  {


}

domain Option[T1]  {

  function none1(): Option[T1]

  function some(x2: T1): Option[T1]

  function option_get(opt: Option[T1]): T1

  axiom {
    (forall x2: T1 ::
      { (some(x2): Option[T1]) }
      (none1(): Option[T1]) != (some(x2): Option[T1]))
  }

  axiom {
    (forall x2: T1 ::
      { (some(x2): Option[T1]) }
      (option_get((some(x2): Option[T1])): T1) == x2)
  }

  axiom {
    (forall opt: Option[T1] ::
      { (some((option_get(opt): T1)): Option[T1]) }
      (some((option_get(opt): T1)): Option[T1]) == opt)
  }
}

domain Nothing  {


}

domain Value[V]  {

  function value_as_pointer_point_105093469_(v: V): Pointer

  function value_as_pointer_linkedlist_1912857409_(v: V): Pointer

  function value_as_point_105093469(v: V): Pointer

  function value_as_int(v: V): Pointer
}

field int: Int

field opt_pointer: Option[Pointer]

field point: Point

field triangle: Triangle

field polygon: Polygon

function ptrDeref(p: Pointer): Ref
  decreases
{
  loc(pointer_block(p), pointer_offset(p))
}

function ptrAdd(p: Pointer, offset: Int): Pointer
  requires 0 <= pointer_offset(p) + offset
  requires pointer_offset(p) + offset < block_length(pointer_block(p))
  decreases
{
  pointer_of(pointer_block(p), pointer_offset(p) + offset)
}

function as_int(value: Pointer): Pointer
  decreases


function as_point_1003792263(value: Pointer): Pointer
  decreases


function as_pointer_point_1003792263_(value: Pointer): Pointer
  decreases


function as_pointer_linkedlist_559086864_(value: Pointer): Pointer
  decreases


function anyAs(t: Any): Any
  decreases


function asAny(t: Any): Any
  decreases
  ensures anyAs(result) == t


function optGet(opt: Option[Any]): Any
  requires opt != (none1(): Option[Any])
  decreases
  ensures (some(result): Option[Any]) == opt
{
  (option_get(opt): Any)
}

function optOrElse(opt: Option[Any], alt: Any): Any
  decreases
  ensures opt == (none1(): Option[Any]) ==> result == alt
  ensures opt != (none1(): Option[Any]) ==> result == optGet(opt)
{
  (opt == (none1(): Option[Any]) ? alt : optGet(opt))
}

function nothingAs(value: Nothing): Any
  decreases


function nothingAs1(value: Nothing): Pointer
  decreases


function optGet1(opt: Option[Nothing]): Nothing
  requires opt != (none1(): Option[Nothing])
  decreases
  ensures (some(result): Option[Nothing]) == opt
{
  (option_get(opt): Nothing)
}

function optGet2(opt: Option[Pointer]): Pointer
  requires opt != (none1(): Option[Pointer])
  decreases
  ensures (some(result): Option[Pointer]) == opt
{
  (option_get(opt): Pointer)
}

function truncdiv(a: Int, b: Int): Int
  requires b != 0
  decreases
{
  (let i ==
    (a / b) in
    (let i1 ==
      (a % b) in
      (a >= 0 || i1 == 0 ? i : i + (b > 0 ? 1 : -1))))
}

function inpToSeq1(inp: Option[Pointer], n: Int): Seq[Int]
  requires 0 <= n
  requires inp !=
    ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
      (none1(): Option[Pointer]) :
      (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
  requires n <=
    block_length(pointer_block(optGet2(inp))) -
    pointer_offset(optGet2(inp))
  requires (forall i: Int ::
      { ptrDeref(ptrAdd(optGet2(inp), i)) }
      0 <= i && i < n ==>
      acc(ptrDeref(ptrAdd(optGet2(inp), i)).point, 1 * write / 10))
  requires (forall i: Int, j: Int ::
      { ptrDeref(ptrAdd(optGet2(inp), i)), ptrDeref(ptrAdd(optGet2(inp), j)) }
      0 <= i && i < n && 0 <= j && j < n && i != j ==>
      ptrDeref(ptrAdd(optGet2(inp), i)).point !=
      ptrDeref(ptrAdd(optGet2(inp), j)).point)
  requires (forall i: Int ::
      { ptrDeref(ptrAdd(optGet2(inp), i)) }
      0 <= i && i < n ==>
      acc(ptrDeref(x(ptrDeref(ptrAdd(optGet2(inp), i)).point)).int, 1 *
      write /
      10))
  decreases _
  ensures |result| == n
  ensures (forall i: Int ::
      { result[i] }
      0 <= i && i < n ==>
      result[i] ==
      ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(inp), i)).point), 0)).int)
{
  (n == 0 ?
    Seq[Int]() :
    inpToSeq1(inp, n - 1) ++
    Seq(ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(inp), n - 1)).point), 0)).int))
}

function sumSeq1(xs: Seq[Int]): Int
  decreases |xs|
  ensures |xs| == 0 ==> result == 0
  ensures 0 < |xs| ==> result == sumSeq1(xs[..|xs| - 1]) + xs[|xs| - 1]
{
  (|xs| == 0 ? 0 : sumSeq1(xs[..|xs| - 1]) + xs[|xs| - 1])
}

function type1(type2: Ref): Int
  decreases
  ensures result >= 0
  ensures result <= 4
  ensures type2 == null ==> result == 0
  ensures type2 != null ==> result != 0


function subtype1(subtype2: Int, subtype3: Int): Bool
  requires subtype2 >= 0
  requires subtype2 <= 4
  requires subtype3 >= 0
  requires subtype3 <= 4
  decreases
{
  (subtype2 == 0 ==> true) &&
  ((subtype2 == 2 ==> subtype3 == 2) && (subtype2 == 4 ==> subtype3 == 4) &&
  (subtype2 == 3 ==> subtype3 == 3) &&
  (subtype2 == 1 ==> subtype3 == 1))
}

method assert2(tid: Int, expression: Bool) returns (res: Void)
  requires expression


method alterStruct1(tid: Int, p: Option[Pointer]) returns (res: Void)
  requires p !=
    ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
      (none1(): Option[Pointer]) :
      (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
  requires acc(ptrDeref(optGet2(p)).point, write)
  requires acc(ptrDeref(x(ptrDeref(ptrAdd(optGet2(p), 0)).point)).int, write)
  requires acc(ptrDeref(y(ptrDeref(ptrAdd(optGet2(p), 0)).point)).int, write)
  ensures p !=
    ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
      (none1(): Option[Pointer]) :
      (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
  ensures acc(ptrDeref(optGet2(p)).point, write)
  ensures acc(ptrDeref(x(ptrDeref(ptrAdd(optGet2(p), 0)).point)).int, write)
  ensures acc(ptrDeref(y(ptrDeref(ptrAdd(optGet2(p), 0)).point)).int, write)
  ensures ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(p), 0)).point), 0)).int ==
    0
  ensures ptrDeref(ptrAdd(y(ptrDeref(ptrAdd(optGet2(p), 0)).point), 0)).int ==
    0
  ensures old(ptrDeref(ptrAdd(optGet2(p), 0)).point) ==
    ptrDeref(ptrAdd(optGet2(p), 0)).point
{
  {
    var exc: Ref
    var return: Void
    var flatten: Point
    var flatten1: Int
    var flatten2: Point
    var flatten3: Int
    exc := null
    flatten := ptrDeref(ptrAdd(optGet2(p), 0)).point
    flatten1 := 0
    ptrDeref(ptrAdd(x(flatten), 0)).int := flatten1
    flatten2 := ptrDeref(ptrAdd(optGet2(p), 0)).point
    flatten3 := 0
    ptrDeref(ptrAdd(y(flatten2), 0)).int := flatten3
    label END
    res := return
    label BUBBLE
    assert exc == null
  }
}

method alterStruct3(tid: Int, p: Option[Pointer]) returns (res: Void)
  requires p !=
    ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
      (none1(): Option[Pointer]) :
      (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
  requires acc(ptrDeref(optGet2(p)).point, write)
  requires acc(ptrDeref(x(ptrDeref(ptrAdd(optGet2(p), 0)).point)).int, write)
  requires acc(ptrDeref(y(ptrDeref(ptrAdd(optGet2(p), 0)).point)).int, write)
  ensures p !=
    ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
      (none1(): Option[Pointer]) :
      (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
  ensures acc(ptrDeref(optGet2(p)).point, write)
  ensures acc(ptrDeref(x(ptrDeref(ptrAdd(optGet2(p), 0)).point)).int, write)
  ensures acc(ptrDeref(y(ptrDeref(ptrAdd(optGet2(p), 0)).point)).int, write)
  ensures ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(p), 0)).point), 0)).int ==
    old(ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(p), 0)).point), 0)).int +
    1)
  ensures ptrDeref(ptrAdd(y(ptrDeref(ptrAdd(optGet2(p), 0)).point), 0)).int ==
    old(ptrDeref(ptrAdd(y(ptrDeref(ptrAdd(optGet2(p), 0)).point), 0)).int +
    1)
  ensures old(ptrDeref(ptrAdd(optGet2(p), 0)).point) ==
    ptrDeref(ptrAdd(optGet2(p), 0)).point
{
  {
    var exc: Ref
    var return: Void
    var flatten: Point
    var flatten1: Int
    var flatten2: Point
    var flatten3: Int
    exc := null
    flatten := ptrDeref(ptrAdd(optGet2(p), 0)).point
    flatten1 := ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(p), 0)).point), 0)).int +
      1
    ptrDeref(ptrAdd(x(flatten), 0)).int := flatten1
    flatten2 := ptrDeref(ptrAdd(optGet2(p), 0)).point
    flatten3 := ptrDeref(ptrAdd(y(ptrDeref(ptrAdd(optGet2(p), 0)).point), 0)).int +
      1
    ptrDeref(ptrAdd(y(flatten2), 0)).int := flatten3
    label END
    res := return
    label BUBBLE
    assert exc == null
  }
}

method alterCopyStruct1(tid: Int, p: Point) returns (res: Void)
  requires acc(ptrDeref(x(p)).int, 1 * write)
  requires acc(ptrDeref(y(p)).int, 1 * write)
  ensures acc(ptrDeref(x(p)).int, 1 * write)
  ensures acc(ptrDeref(y(p)).int, 1 * write)
{
  {
    var exc: Ref
    var return: Void
    var flatten: Int
    var flatten1: Int
    exc := null
    flatten := 0
    ptrDeref(ptrAdd(x(p), 0)).int := flatten
    flatten1 := 0
    ptrDeref(ptrAdd(y(p), 0)).int := flatten1
    label END
    res := return
    label BUBBLE
    assert exc == null
  }
}

method alterCopyStruct3(tid: Int, p: Point) returns (res: Void)
  requires acc(ptrDeref(x(p)).int, 1 * write)
  requires acc(ptrDeref(y(p)).int, 1 * write)
  ensures acc(ptrDeref(x(p)).int, 1 * write)
  ensures acc(ptrDeref(y(p)).int, 1 * write)
{
  {
    var exc: Ref
    var return: Void
    var flatten: Int
    var flatten1: Int
    exc := null
    flatten := 0
    ptrDeref(ptrAdd(x(p), 0)).int := flatten
    flatten1 := 0
    ptrDeref(ptrAdd(y(p), 0)).int := flatten1
    label END
    res := return
    label BUBBLE
    assert exc == null
  }
}

method avrX1(tid: Int, r: Option[Pointer]) returns (res: Int)
  requires r !=
    ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
      (none1(): Option[Pointer]) :
      (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
  requires acc(ptrDeref(optGet2(r)).triangle, 1 * write / 2)
  requires acc(ptrDeref(p_1(ptrDeref(ptrAdd(optGet2(r), 0)).triangle)).point, 1 *
    write /
    2)
  requires acc(ptrDeref(x(ptrDeref(ptrAdd(p_1(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point)).int, 1 * write / 2)
  requires acc(ptrDeref(y(ptrDeref(ptrAdd(p_1(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point)).int, 1 * write / 2)
  requires acc(ptrDeref(p_2(ptrDeref(ptrAdd(optGet2(r), 0)).triangle)).point, 1 *
    write /
    2)
  requires acc(ptrDeref(x(ptrDeref(ptrAdd(p_2(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point)).int, 1 * write / 2)
  requires acc(ptrDeref(y(ptrDeref(ptrAdd(p_2(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point)).int, 1 * write / 2)
  requires acc(ptrDeref(p_3(ptrDeref(ptrAdd(optGet2(r), 0)).triangle)).point, 1 *
    write /
    2)
  requires acc(ptrDeref(x(ptrDeref(ptrAdd(p_3(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point)).int, 1 * write / 2)
  requires acc(ptrDeref(y(ptrDeref(ptrAdd(p_3(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point)).int, 1 * write / 2)
  ensures r !=
    ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
      (none1(): Option[Pointer]) :
      (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
  ensures acc(ptrDeref(optGet2(r)).triangle, 1 * write / 2)
  ensures acc(ptrDeref(p_1(ptrDeref(ptrAdd(optGet2(r), 0)).triangle)).point, 1 *
    write /
    2)
  ensures acc(ptrDeref(x(ptrDeref(ptrAdd(p_1(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point)).int, 1 * write / 2)
  ensures acc(ptrDeref(y(ptrDeref(ptrAdd(p_1(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point)).int, 1 * write / 2)
  ensures acc(ptrDeref(p_2(ptrDeref(ptrAdd(optGet2(r), 0)).triangle)).point, 1 *
    write /
    2)
  ensures acc(ptrDeref(x(ptrDeref(ptrAdd(p_2(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point)).int, 1 * write / 2)
  ensures acc(ptrDeref(y(ptrDeref(ptrAdd(p_2(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point)).int, 1 * write / 2)
  ensures acc(ptrDeref(p_3(ptrDeref(ptrAdd(optGet2(r), 0)).triangle)).point, 1 *
    write /
    2)
  ensures acc(ptrDeref(x(ptrDeref(ptrAdd(p_3(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point)).int, 1 * write / 2)
  ensures acc(ptrDeref(y(ptrDeref(ptrAdd(p_3(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point)).int, 1 * write / 2)
  ensures res ==
    truncdiv(ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(p_1(ptrDeref(ptrAdd(optGet2(r),
    0)).triangle), 0)).point), 0)).int +
    ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(p_2(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point), 0)).int +
    ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(p_3(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
    0)).point), 0)).int, 3)
{
  {
    var exc: Ref
    var return: Int
    var flatten: Int
    exc := null
    flatten := truncdiv(ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(p_1(ptrDeref(ptrAdd(optGet2(r),
      0)).triangle), 0)).point), 0)).int +
      ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(p_2(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
      0)).point), 0)).int +
      ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(p_3(ptrDeref(ptrAdd(optGet2(r), 0)).triangle),
      0)).point), 0)).int, 3)
    return := flatten
    goto END
    label END
    res := return
    label BUBBLE
    assert exc == null
  }
}

method avrXPol1(tid: Int, p: Option[Pointer], len: Int) returns (res: Int)
  requires 0 < len
  requires p !=
    ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
      (none1(): Option[Pointer]) :
      (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
  requires acc(ptrDeref(optGet2(p)).polygon, 1 * write / 2)
  requires acc(ptrDeref(ps(ptrDeref(ptrAdd(optGet2(p), 0)).polygon)).opt_pointer, 1 *
    write /
    2)
  requires ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p), 0)).polygon), 0)).opt_pointer !=
    ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
      (none1(): Option[Pointer]) :
      (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
  requires len <=
    block_length(pointer_block(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
    0)).polygon), 0)).opt_pointer))) -
    pointer_offset(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p), 0)).polygon),
    0)).opt_pointer))
  requires (forall i: Int ::
      { ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)) }
      0 <= i && i < len ==>
      acc(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)).point, 1 * write / 2))
  requires (forall i: Int, j: Int ::
      { ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)), ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), j)) }
      0 <= i && i < len && 0 <= j && j < len && i != j ==>
      ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)).point !=
      ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), j)).point)
  requires (forall i: Int ::
      { ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)) }
      0 <= i && i < len ==>
      acc(ptrDeref(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)).point)).int, 1 * write / 2)) &&
    (forall i: Int ::
      { ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)) }
      0 <= i && i < len ==>
      acc(ptrDeref(y(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)).point)).int, 1 * write / 2))
  ensures p !=
    ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
      (none1(): Option[Pointer]) :
      (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
  ensures acc(ptrDeref(optGet2(p)).polygon, 1 * write / 2)
  ensures acc(ptrDeref(ps(ptrDeref(ptrAdd(optGet2(p), 0)).polygon)).opt_pointer, 1 *
    write /
    2)
  ensures ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p), 0)).polygon), 0)).opt_pointer !=
    ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
      (none1(): Option[Pointer]) :
      (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
  ensures len <=
    block_length(pointer_block(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
    0)).polygon), 0)).opt_pointer))) -
    pointer_offset(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p), 0)).polygon),
    0)).opt_pointer))
  ensures (forall i: Int ::
      { ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)) }
      0 <= i && i < len ==>
      acc(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)).point, 1 * write / 2))
  ensures (forall i: Int, j: Int ::
      { ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)), ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), j)) }
      0 <= i && i < len && 0 <= j && j < len && i != j ==>
      ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)).point !=
      ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), j)).point)
  ensures (forall i: Int ::
      { ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)) }
      0 <= i && i < len ==>
      acc(ptrDeref(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)).point)).int, 1 * write / 2)) &&
    (forall i: Int ::
      { ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)) }
      0 <= i && i < len ==>
      acc(ptrDeref(y(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
      0)).polygon), 0)).opt_pointer), i)).point)).int, 1 * write / 2))
  ensures len == 3 ==>
    res ==
    truncdiv(ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
    0)).polygon), 0)).opt_pointer), 0)).point), 0)).int +
    ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
    0)).polygon), 0)).opt_pointer), 1)).point), 0)).int +
    ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
    0)).polygon), 0)).opt_pointer), 2)).point), 0)).int, len)
{
  {
    var exc: Ref
    var return: Int
    var sum: Int
    var i: Int
    var flatten: Int
    var flatten1: Int
    var flatten2: Int
    var flatten3: Int
    var flatten4: Int
    var excbeforeloop: Ref
    exc := null
    flatten := 0
    sum := flatten
    label LOOP
    excbeforeloop := exc
    flatten1 := 0
    i := flatten1
    while (i < len)
      invariant exc == excbeforeloop
      invariant 0 <= i
      invariant i < len + 1
      invariant p !=
        ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
          (none1(): Option[Pointer]) :
          (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
      invariant acc(ptrDeref(optGet2(p)).polygon, 1 * write / 2)
      invariant acc(ptrDeref(ps(ptrDeref(ptrAdd(optGet2(p), 0)).polygon)).opt_pointer, 1 *
        write /
        2)
      invariant ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p), 0)).polygon),
        0)).opt_pointer !=
        ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
          (none1(): Option[Pointer]) :
          (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
      invariant len <=
        block_length(pointer_block(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
        0)).polygon), 0)).opt_pointer))) -
        pointer_offset(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
        0)).polygon), 0)).opt_pointer))
      invariant (forall i1: Int ::
          { ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
          0)).polygon), 0)).opt_pointer), i1)) }
          0 <= i1 && i1 < len ==>
          acc(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
          0)).polygon), 0)).opt_pointer), i1)).point, 1 * write / 2))
      invariant (forall i1: Int, j: Int ::
          { ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
          0)).polygon), 0)).opt_pointer), i1)), ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
          0)).polygon), 0)).opt_pointer), j)) }
          0 <= i1 && i1 < len && 0 <= j && j < len && i1 != j ==>
          ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
          0)).polygon), 0)).opt_pointer), i1)).point !=
          ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
          0)).polygon), 0)).opt_pointer), j)).point)
      invariant (forall i1: Int ::
          { ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
          0)).polygon), 0)).opt_pointer), i1)) }
          0 <= i1 && i1 < len ==>
          acc(ptrDeref(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
          0)).polygon), 0)).opt_pointer), i1)).point)).int, 1 * write / 2)) &&
        (forall i1: Int ::
          { ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
          0)).polygon), 0)).opt_pointer), i1)) }
          0 <= i1 && i1 < len ==>
          acc(ptrDeref(y(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
          0)).polygon), 0)).opt_pointer), i1)).point)).int, 1 * write / 2))
      invariant i == 0 ==> sum == 0
      invariant i == 1 ==>
        sum ==
        ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
        0)).polygon), 0)).opt_pointer), 0)).point), 0)).int
      invariant i == 2 ==>
        sum ==
        ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
        0)).polygon), 0)).opt_pointer), 0)).point), 0)).int +
        ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
        0)).polygon), 0)).opt_pointer), 1)).point), 0)).int
      invariant i == 3 ==>
        sum ==
        ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
        0)).polygon), 0)).opt_pointer), 0)).point), 0)).int +
        ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
        0)).polygon), 0)).opt_pointer), 1)).point), 0)).int +
        ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
        0)).polygon), 0)).opt_pointer), 2)).point), 0)).int
    {
      flatten3 := sum +
        ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(ptrDeref(ptrAdd(ps(ptrDeref(ptrAdd(optGet2(p),
        0)).polygon), 0)).opt_pointer), i)).point), 0)).int
      sum := flatten3
      flatten2 := i
      i := i + 1
    }
    flatten4 := truncdiv(sum, len)
    return := flatten4
    goto END
    label END
    res := return
    label BUBBLE
    assert exc == null
  }
}

method make_pointer_array_point_710117686(tid: Int, size: Int)
  returns (res: Option[Pointer])
  requires 0 <= size
  ensures res !=
    ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
      (none1(): Option[Pointer]) :
      (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer]))
  ensures block_length(pointer_block(optGet2(res))) == size
  ensures pointer_offset(optGet2(res)) == 0
  ensures (forall i: Int ::
      { ptrDeref(ptrAdd(optGet2(res), i)) }
      0 <= i && i < size ==>
      acc(ptrDeref(ptrAdd(optGet2(res), i)).point, write))
  ensures (forall i: Int, j: Int ::
      { ptrDeref(ptrAdd(optGet2(res), i)), ptrDeref(ptrAdd(optGet2(res), j)) }
      0 <= i && i < size && (0 <= j && j < size) &&
      ptrDeref(ptrAdd(optGet2(res), i)).point ==
      ptrDeref(ptrAdd(optGet2(res), j)).point ==>
      i == j)
  ensures (forall i: Int ::
      { ptrDeref(ptrAdd(optGet2(res), i)) }
      0 <= i && i < size ==>
      acc(ptrDeref(x(ptrDeref(ptrAdd(optGet2(res), i)).point)).int, write))
  ensures (forall i: Int ::
      { ptrDeref(ptrAdd(optGet2(res), i)) }
      0 <= i && i < size ==>
      acc(ptrDeref(y(ptrDeref(ptrAdd(optGet2(res), i)).point)).int, write))


method point2() returns (res: Point)
  decreases
  ensures acc(ptrDeref(x(res)).int, write)
  ensures acc(ptrDeref(y(res)).int, write)


method triangle2() returns (res: Triangle)
  decreases
  ensures acc(ptrDeref(p_1(res)).point, write)
  ensures acc(ptrDeref(x(ptrDeref(ptrAdd(p_1(res), 0)).point)).int, write)
  ensures acc(ptrDeref(y(ptrDeref(ptrAdd(p_1(res), 0)).point)).int, write)
  ensures acc(ptrDeref(p_2(res)).point, write)
  ensures acc(ptrDeref(x(ptrDeref(ptrAdd(p_2(res), 0)).point)).int, write)
  ensures acc(ptrDeref(y(ptrDeref(ptrAdd(p_2(res), 0)).point)).int, write)
  ensures acc(ptrDeref(p_3(res)).point, write)
  ensures acc(ptrDeref(x(ptrDeref(ptrAdd(p_3(res), 0)).point)).int, write)
  ensures acc(ptrDeref(y(ptrDeref(ptrAdd(p_3(res), 0)).point)).int, write)


method polygon2() returns (res: Polygon)
  decreases
  ensures acc(ptrDeref(ps(res)).opt_pointer, write)


method create_nonnull_pointer_point_703118078() returns (res: Pointer)
  decreases
  ensures block_length(pointer_block(res)) == 1
  ensures pointer_offset(res) == 0
  ensures acc(ptrDeref(res).point, write)


method create_nonnull_pointer_triangle_420754499() returns (res: Pointer)
  decreases
  ensures block_length(pointer_block(res)) == 1
  ensures pointer_offset(res) == 0
  ensures acc(ptrDeref(res).triangle, write)


method create_nonnull_pointer_polygon_968426744() returns (res: Pointer)
  decreases
  ensures block_length(pointer_block(res)) == 1
  ensures pointer_offset(res) == 0
  ensures acc(ptrDeref(res).polygon, write)


method main1(tid: Int) returns (res: Int)
{
  {
    var exc: Ref
    var return: Int
    var pp: Option[Pointer]
    var rr: Option[Pointer]
    var ps1: Option[Pointer]
    var ppols: Option[Pointer]
    var avrPol: Int
    var original: Point
    var copy: Point
    var original1: Point
    var copy1: Point
    var original2: Point
    var copy2: Point
    var original3: Point
    var copy3: Point
    var original4: Point
    var copy4: Point
    var original5: Point
    var copy5: Point
    var original6: Point
    var copy6: Point
    var flatten: Pointer
    var res1: Point
    var flatten1: Point
    var flatten2: Pointer
    var res2: Void
    var flatten3: Point
    var flatten4: Int
    var flatten5: Point
    var flatten6: Int
    var res3: Void
    var res4: Void
    var res5: Void
    var flatten7: Point
    var res6: Point
    var flatten8: Point
    var flatten9: Point
    var flatten10: Int
    var flatten11: Int
    var res7: Void
    var res8: Void
    var res9: Void
    var res10: Void
    var res11: Void
    var res12: Void
    var res13: Void
    var flatten12: Pointer
    var res14: Point
    var flatten13: Point
    var flatten14: Pointer
    var res15: Point
    var flatten15: Point
    var flatten16: Pointer
    var res16: Point
    var flatten17: Point
    var flatten18: Point
    var flatten19: Int
    var flatten20: Point
    var flatten21: Int
    var flatten22: Point
    var flatten23: Int
    var flatten24: Point
    var flatten25: Int
    var flatten26: Point
    var flatten27: Int
    var flatten28: Point
    var flatten29: Int
    var flatten30: Pointer
    var res17: Triangle
    var flatten31: Triangle
    var flatten32: Pointer
    var flatten33: Triangle
    var flatten34: Point
    var res18: Point
    var flatten35: Point
    var flatten36: Point
    var flatten37: Int
    var flatten38: Int
    var flatten39: Point
    var flatten40: Triangle
    var flatten41: Point
    var res19: Point
    var flatten42: Point
    var flatten43: Point
    var flatten44: Int
    var flatten45: Int
    var flatten46: Point
    var flatten47: Triangle
    var flatten48: Point
    var res20: Point
    var flatten49: Point
    var flatten50: Point
    var flatten51: Int
    var flatten52: Int
    var flatten53: Point
    var res21: Void
    var res22: Int
    var res23: Option[Pointer]
    var flatten54: Option[Pointer]
    var flatten55: Int
    var flatten56: Point
    var res24: Point
    var flatten57: Point
    var flatten58: Point
    var flatten59: Int
    var flatten60: Int
    var flatten61: Point
    var flatten62: Int
    var flatten63: Point
    var res25: Point
    var flatten64: Point
    var flatten65: Point
    var flatten66: Int
    var flatten67: Int
    var flatten68: Point
    var flatten69: Int
    var flatten70: Point
    var res26: Point
    var flatten71: Point
    var flatten72: Point
    var flatten73: Int
    var flatten74: Int
    var flatten75: Point
    var flatten76: Pointer
    var res27: Polygon
    var flatten77: Polygon
    var flatten78: Pointer
    var flatten79: Polygon
    var res28: Int
    var flatten80: Int
    var res29: Void
    var flatten81: Int
    var p: Pointer
    var p1: Pointer
    var p2: Pointer
    var p3: Pointer
    var r: Pointer
    var pol: Pointer
    p := create_nonnull_pointer_point_703118078()
    p1 := create_nonnull_pointer_point_703118078()
    p2 := create_nonnull_pointer_point_703118078()
    p3 := create_nonnull_pointer_point_703118078()
    r := create_nonnull_pointer_triangle_420754499()
    pol := create_nonnull_pointer_polygon_968426744()
    exc := null
    flatten := p
    res1 := point2()
    flatten1 := res1
    ptrDeref(ptrAdd(flatten, 0)).point := flatten1
    flatten2 := p
    pp := (some(flatten2): Option[Pointer])
    res2 := assert2(tid, pp !=
      ((none1(): Option[Nothing]) == (none1(): Option[Nothing]) ?
        (none1(): Option[Pointer]) :
        (some(nothingAs1(optGet1((none1(): Option[Nothing])))): Option[Pointer])))
    flatten3 := ptrDeref(ptrAdd(p, 0)).point
    flatten4 := 1
    ptrDeref(ptrAdd(x(flatten3), 0)).int := flatten4
    flatten5 := ptrDeref(ptrAdd(p, 0)).point
    flatten6 := 2
    ptrDeref(ptrAdd(y(flatten5), 0)).int := flatten6
    res3 := assert2(tid, ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(pp), 0)).point),
      0)).int ==
      1)
    res4 := assert2(tid, ptrDeref(ptrAdd(y(ptrDeref(ptrAdd(optGet2(pp), 0)).point),
      0)).int ==
      2)
    flatten7 := ptrDeref(ptrAdd(p, 0)).point
    original := flatten7
    res6 := point2()
    flatten8 := res6
    copy := flatten8
    flatten9 := flatten8
    flatten10 := ptrDeref(ptrAdd(x(original), 0)).int
    ptrDeref(ptrAdd(x(copy), 0)).int := flatten10
    flatten11 := ptrDeref(ptrAdd(y(original), 0)).int
    ptrDeref(ptrAdd(y(copy), 0)).int := flatten11
    res5 := alterCopyStruct1(tid, flatten9)
    res7 := assert2(tid, ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(p, 0)).point), 0)).int ==
      1)
    res8 := assert2(tid, ptrDeref(ptrAdd(y(ptrDeref(ptrAdd(p, 0)).point), 0)).int ==
      2)
    res9 := alterStruct1(tid, pp)
    res10 := assert2(tid, ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(optGet2(pp), 0)).point),
      0)).int ==
      0)
    res11 := assert2(tid, ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(p, 0)).point), 0)).int ==
      0)
    res12 := alterStruct3(tid, pp)
    res13 := assert2(tid, ptrDeref(ptrAdd(x(ptrDeref(ptrAdd(p, 0)).point), 0)).int ==
      1 &&
      ptrDeref(ptrAdd(y(ptrDeref(ptrAdd(p, 0)).point), 0)).int == 1)
    flatten12 := p1
    res14 := point2()
    flatten13 := res14
    ptrDeref(ptrAdd(flatten12, 0)).point := flatten13
    flatten14 := p2
    res15 := point2()
    flatten15 := res15
    ptrDeref(ptrAdd(flatten14, 0)).point := flatten15
    flatten16 := p3
    res16 := point2()
    flatten17 := res16
    ptrDeref(ptrAdd(flatten16, 0)).point := flatten17
    flatten18 := ptrDeref(ptrAdd(p1, 0)).point
    flatten19 := 1
    ptrDeref(ptrAdd(x(flatten18), 0)).int := flatten19
    flatten20 := ptrDeref(ptrAdd(p1, 0)).point
    flatten21 := 1
    ptrDeref(ptrAdd(y(flatten20), 0)).int := flatten21
    flatten22 := ptrDeref(ptrAdd(p2, 0)).point
    flatten23 := 2
    ptrDeref(ptrAdd(x(flatten22), 0)).int := flatten23
    flatten24 := ptrDeref(ptrAdd(p1, 0)).point
    flatten25 := 2
    ptrDeref(ptrAdd(y(flatten24), 0)).int := flatten25
    flatten26 := ptrDeref(ptrAdd(p3, 0)).point
    flatten27 := 3
    ptrDeref(ptrAdd(x(flatten26), 0)).int := flatten27
    flatten28 := ptrDeref(ptrAdd(p1, 0)).point
    flatten29 := 3
    ptrDeref(ptrAdd(y(flatten28), 0)).int := flatten29
    flatten30 := r
    res17 := triangle2()
    flatten31 := res17
    ptrDeref(ptrAdd(flatten30, 0)).triangle := flatten31
    flatten32 := r
    rr := (some(flatten32): Option[Pointer])
    flatten33 := ptrDeref(ptrAdd(r, 0)).triangle
    flatten34 := ptrDeref(ptrAdd(p1, 0)).point
    original1 := flatten34
    res18 := point2()
    flatten35 := res18
    copy1 := flatten35
    flatten36 := flatten35
    flatten37 := ptrDeref(ptrAdd(x(original1), 0)).int
    ptrDeref(ptrAdd(x(copy1), 0)).int := flatten37
    flatten38 := ptrDeref(ptrAdd(y(original1), 0)).int
    ptrDeref(ptrAdd(y(copy1), 0)).int := flatten38
    flatten39 := flatten36
    ptrDeref(ptrAdd(p_1(flatten33), 0)).point := flatten39
    flatten40 := ptrDeref(ptrAdd(r, 0)).triangle
    flatten41 := ptrDeref(ptrAdd(p2, 0)).point
    original2 := flatten41
    res19 := point2()
    flatten42 := res19
    copy2 := flatten42
    flatten43 := flatten42
    flatten44 := ptrDeref(ptrAdd(x(original2), 0)).int
    ptrDeref(ptrAdd(x(copy2), 0)).int := flatten44
    flatten45 := ptrDeref(ptrAdd(y(original2), 0)).int
    ptrDeref(ptrAdd(y(copy2), 0)).int := flatten45
    flatten46 := flatten43
    ptrDeref(ptrAdd(p_2(flatten40), 0)).point := flatten46
    flatten47 := ptrDeref(ptrAdd(r, 0)).triangle
    flatten48 := ptrDeref(ptrAdd(p3, 0)).point
    original3 := flatten48
    res20 := point2()
    flatten49 := res20
    copy3 := flatten49
    flatten50 := flatten49
    flatten51 := ptrDeref(ptrAdd(x(original3), 0)).int
    ptrDeref(ptrAdd(x(copy3), 0)).int := flatten51
    flatten52 := ptrDeref(ptrAdd(y(original3), 0)).int
    ptrDeref(ptrAdd(y(copy3), 0)).int := flatten52
    flatten53 := flatten50
    ptrDeref(ptrAdd(p_3(flatten47), 0)).point := flatten53
    res22 := avrX1(tid, rr)
    res21 := assert2(tid, res22 == 2)
    res23 := make_pointer_array_point_710117686(tid, 3)
    flatten54 := res23
    ps1 := flatten54
    flatten55 := 0
    flatten56 := ptrDeref(ptrAdd(p1, 0)).point
    original4 := flatten56
    res24 := point2()
    flatten57 := res24
    copy4 := flatten57
    flatten58 := flatten57
    flatten59 := ptrDeref(ptrAdd(x(original4), 0)).int
    ptrDeref(ptrAdd(x(copy4), 0)).int := flatten59
    flatten60 := ptrDeref(ptrAdd(y(original4), 0)).int
    ptrDeref(ptrAdd(y(copy4), 0)).int := flatten60
    flatten61 := flatten58
    ptrDeref(ptrAdd(optGet2(ps1), flatten55)).point := flatten61
    flatten62 := 1
    flatten63 := ptrDeref(ptrAdd(p2, 0)).point
    original5 := flatten63
    res25 := point2()
    flatten64 := res25
    copy5 := flatten64
    flatten65 := flatten64
    flatten66 := ptrDeref(ptrAdd(x(original5), 0)).int
    ptrDeref(ptrAdd(x(copy5), 0)).int := flatten66
    flatten67 := ptrDeref(ptrAdd(y(original5), 0)).int
    ptrDeref(ptrAdd(y(copy5), 0)).int := flatten67
    flatten68 := flatten65
    ptrDeref(ptrAdd(optGet2(ps1), flatten62)).point := flatten68
    flatten69 := 2
    flatten70 := ptrDeref(ptrAdd(p3, 0)).point
    original6 := flatten70
    res26 := point2()
    flatten71 := res26
    copy6 := flatten71
    flatten72 := flatten71
    flatten73 := ptrDeref(ptrAdd(x(original6), 0)).int
    ptrDeref(ptrAdd(x(copy6), 0)).int := flatten73
    flatten74 := ptrDeref(ptrAdd(y(original6), 0)).int
    ptrDeref(ptrAdd(y(copy6), 0)).int := flatten74
    flatten75 := flatten72
    ptrDeref(ptrAdd(optGet2(ps1), flatten69)).point := flatten75
    flatten76 := pol
    res27 := polygon2()
    flatten77 := res27
    ptrDeref(ptrAdd(flatten76, 0)).polygon := flatten77
    flatten78 := pol
    ppols := (some(flatten78): Option[Pointer])
    flatten79 := ptrDeref(ptrAdd(pol, 0)).polygon
    ptrDeref(ptrAdd(ps(flatten79), 0)).opt_pointer := ps1
    res28 := avrXPol1(tid, ppols, 3)
    flatten80 := res28
    avrPol := flatten80
    res29 := assert2(tid, avrPol == 2)
    flatten81 := 0
    return := flatten81
    goto END
    label END
    res := return
    label BUBBLE
    assert exc == null
  }
}