domain Array  {
  
  function array_loc(a1: Array, i: Int): Ref 
  
  function alen(a1: Array): Int 
  
  function loc_inv_1(loc: Ref): Array 
  
  function loc_inv_2(loc: Ref): Int 
  
  axiom {
    (forall a1: Array, i: Int ::
      { array_loc(a1, i) }
      loc_inv_1(array_loc(a1, i)) == a1 && loc_inv_2(array_loc(a1, i)) == i)
  }
  
  axiom {
    (forall a1: Array :: { alen(a1) } alen(a1) >= 0)
  }
}

domain Option[T1]  {
  
  function none1(): Option[T1] 
  
  function some(x: T1): Option[T1] 
  
  function option_get(opt: Option[T1]): T1 
  
  axiom {
    (forall x: T1 ::
      { (some(x): Option[T1]) }
      (none1(): Option[T1]) != (some(x): Option[T1]))
  }
  
  axiom {
    (forall x: T1 ::
      { (some(x): Option[T1]) }
      (option_get((some(x): Option[T1])): T1) == x)
  }
  
  axiom {
    (forall opt: Option[T1] ::
      { (some((option_get(opt): T1)): Option[T1]) }
      (some((option_get(opt): T1)): Option[T1]) == opt)
  }
}

field int: Int

field c: Option[Array]

field a: Option[Array]

field b: Option[Array]

function aloc(a1: Array, i: Int): Ref
  requires 0 <= i
  requires i < alen(a1)
  decreases 
  ensures loc_inv_1(result) == a1
  ensures loc_inv_2(result) == i
{
  array_loc(a1, i)
}

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

method init1(this: Ref)
  requires this != null
  requires acc(this.a, write)
  requires this.a != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(this.a), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(this.a)) ==>
      acc(aloc(optGet1(this.a), preferred_list_i__).int, write))
  requires acc(this.b, write)
  requires this.b != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(this.b), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(this.b)) ==>
      acc(aloc(optGet1(this.b), preferred_list_i__).int, write))
  requires acc(this.c, write)
  requires this.c != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(this.c), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(this.c)) ==>
      acc(aloc(optGet1(this.c), preferred_list_i__).int, write))
  ensures acc(this.a, write)
  ensures this.a != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(this.a), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(this.a)) ==>
      acc(aloc(optGet1(this.a), preferred_list_i__).int, write))
  ensures acc(this.b, write)
  ensures this.b != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(this.b), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(this.b)) ==>
      acc(aloc(optGet1(this.b), preferred_list_i__).int, write))
  ensures acc(this.c, write)
  ensures this.c != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(this.c), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(this.c)) ==>
      acc(aloc(optGet1(this.c), preferred_list_i__).int, write))

method bar1(c1: Ref)
  requires acc(c1.a, write)
  requires c1.a != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(c1.a), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(c1.a)) ==>
      acc(aloc(optGet1(c1.a), preferred_list_i__).int, write))
  requires acc(c1.b, write)
  requires c1.b != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(c1.b), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(c1.b)) ==>
      acc(aloc(optGet1(c1.b), preferred_list_i__).int, write))
  requires acc(c1.c, write)
  requires c1.c != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(c1.c), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(c1.c)) ==>
      acc(aloc(optGet1(c1.c), preferred_list_i__).int, write))
  ensures acc(c1.a, write)
  ensures c1.a != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(c1.a), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(c1.a)) ==>
      acc(aloc(optGet1(c1.a), preferred_list_i__).int, write))
  ensures acc(c1.b, write)
  ensures c1.b != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(c1.b), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(c1.b)) ==>
      acc(aloc(optGet1(c1.b), preferred_list_i__).int, write))
  ensures acc(c1.c, write)
  ensures c1.c != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(c1.c), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(c1.c)) ==>
      acc(aloc(optGet1(c1.c), preferred_list_i__).int, write))


method foo1(c1: Ref, d: Ref, e: Ref)
  requires acc(c1.a, write)
  requires c1.a != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(c1.a), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(c1.a)) ==>
      acc(aloc(optGet1(c1.a), preferred_list_i__).int, write))
  requires acc(c1.b, write)
  requires c1.b != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(c1.b), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(c1.b)) ==>
      acc(aloc(optGet1(c1.b), preferred_list_i__).int, write))
  requires acc(c1.c, write)
  requires c1.c != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(c1.c), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(c1.c)) ==>
      acc(aloc(optGet1(c1.c), preferred_list_i__).int, write))
  requires acc(d.a, write)
  requires d.a != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(d.a), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(d.a)) ==>
      acc(aloc(optGet1(d.a), preferred_list_i__).int, write))
  requires acc(d.b, write)
  requires d.b != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(d.b), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(d.b)) ==>
      acc(aloc(optGet1(d.b), preferred_list_i__).int, write))
  requires acc(d.c, write)
  requires d.c != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(d.c), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(d.c)) ==>
      acc(aloc(optGet1(d.c), preferred_list_i__).int, write))
  requires acc(e.a, write)
  requires e.a != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(e.a), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(e.a)) ==>
      acc(aloc(optGet1(e.a), preferred_list_i__).int, write))
  requires acc(e.b, write)
  requires e.b != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(e.b), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(e.b)) ==>
      acc(aloc(optGet1(e.b), preferred_list_i__).int, write))
  requires acc(e.c, write)
  requires e.c != (none1(): Option[Array])
  requires (forall preferred_list_i__: Int ::
      { aloc(optGet1(e.c), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(e.c)) ==>
      acc(aloc(optGet1(e.c), preferred_list_i__).int, write))
  ensures acc(c1.a, write)
  ensures c1.a != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(c1.a), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(c1.a)) ==>
      acc(aloc(optGet1(c1.a), preferred_list_i__).int, write))
  ensures acc(c1.b, write)
  ensures c1.b != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(c1.b), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(c1.b)) ==>
      acc(aloc(optGet1(c1.b), preferred_list_i__).int, write))
  ensures acc(c1.c, write)
  ensures c1.c != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(c1.c), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(c1.c)) ==>
      acc(aloc(optGet1(c1.c), preferred_list_i__).int, write))
  ensures acc(d.a, write)
  ensures d.a != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(d.a), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(d.a)) ==>
      acc(aloc(optGet1(d.a), preferred_list_i__).int, write))
  ensures acc(d.b, write)
  ensures d.b != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(d.b), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(d.b)) ==>
      acc(aloc(optGet1(d.b), preferred_list_i__).int, write))
  ensures acc(d.c, write)
  ensures d.c != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(d.c), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(d.c)) ==>
      acc(aloc(optGet1(d.c), preferred_list_i__).int, write))
  ensures acc(e.a, write)
  ensures e.a != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(e.a), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(e.a)) ==>
      acc(aloc(optGet1(e.a), preferred_list_i__).int, write))
  ensures acc(e.b, write)
  ensures e.b != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(e.b), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(e.b)) ==>
      acc(aloc(optGet1(e.b), preferred_list_i__).int, write))
  ensures acc(e.c, write)
  ensures e.c != (none1(): Option[Array])
  ensures (forall preferred_list_i__: Int ::
      { aloc(optGet1(e.c), preferred_list_i__) }
      0 <= preferred_list_i__ && preferred_list_i__ < alen(optGet1(e.c)) ==>
      acc(aloc(optGet1(e.c), preferred_list_i__).int, write))
{
  bar1(c1)
  bar1(d)
}