domain Embfn$$0 {
  
  
}

domain Equality[T] {
  
  function eq(l: T, r: T): Bool
  
  axiom {
    (forall l: T, r: T :: { eq(l, r) } eq(l, r) == (l == r))
  }
}

function arrayDefault_fn$$2(): Embfn$$0
  ensures (forall idx: Int :: { unbox_Embfn$$0(result)[idx] } 0 <= idx && idx < 20 ==> unbox_Embfn$$0(result)[idx] == 0)


function box_Embfn$$0(x: Seq[Int]): Embfn$$0
  requires |x| == 20
  ensures unbox_Embfn$$0(result) == x


function unbox_Embfn$$0(y: Embfn$$0): Seq[Int]
  ensures |result| == 20
  ensures box_Embfn$$0(result) == y


function assertArg(b: Bool): Bool
  requires b
{
  true
}

function test_pkg_F(s_pkg_V0: Embfn$$0, n_pkg_V0: Int): Int
{
  (let localvar_s_pkg_V0_CN0_1 == (arrayDefault_fn$$2()) in
  (let localvar_n_pkg_V0_CN1_2 == (0) in
  (let localvar_res_pkg_V0_CN2_3 == (0) in
  (let localvar_s_pkg_V0_CN0_4 == (s_pkg_V0) in
  (let localvar_n_pkg_V0_CN1_5 == (n_pkg_V0) in
  (let localvar_res_pkg_V0_6 == (test_internal_pkg_F(localvar_s_pkg_V0_CN0_4, localvar_n_pkg_V0_CN1_5, 0)) in
  (let returnvar_7 == (false) in
  (let localvar_res_pkg_V0_8 == ((returnvar_7 ? localvar_res_pkg_V0_CN2_3 : localvar_res_pkg_V0_6)) in
  localvar_res_pkg_V0_8))))))))
}

function test_internal_pkg_F(s_pkg_V1: Embfn$$0, needle_pkg_V1: Int, i_pkg_V1: Int): Int
  requires i_pkg_V1 >= 0
  requires i_pkg_V1 < 20
{
  (let localvar_s_pkg_V1_CN4_1 == (arrayDefault_fn$$2()) in
  (let localvar_needle_pkg_V1_CN5_2 == (0) in
  (let localvar_i_pkg_V1_CN6_3 == (0) in
  (let localvar_res_pkg_V1_CN7_4 == (0) in
  (let localvar_s_pkg_V1_CN4_5 == (s_pkg_V1) in
  (let localvar_needle_pkg_V1_CN5_6 == (needle_pkg_V1) in
  (let localvar_i_pkg_V1_CN6_7 == (i_pkg_V1) in
  (let localvar_found_pkg_V2_8 == (0) in
  (let localvar_found_pkg_V2_9 == (0) in
  (let localvar_found_pkg_V2_10 == ((true && unbox_Embfn$$0(localvar_s_pkg_V1_CN4_5)[localvar_i_pkg_V1_CN6_7] == localvar_needle_pkg_V1_CN5_6 ? localvar_found_pkg_V2_9 + 1 : localvar_found_pkg_V2_9)) in
  (let localvar_i_pkg_V1_CN6_11 == (localvar_i_pkg_V1_CN6_7 + 1) in
  (let localvar_res_pkg_V1_12 == ((true && localvar_i_pkg_V1_CN6_11 == |unbox_Embfn$$0(localvar_s_pkg_V1_CN4_5)| ? localvar_found_pkg_V2_10 : 0)) in
  (let returnvar_13 == ((localvar_i_pkg_V1_CN6_11 == |unbox_Embfn$$0(localvar_s_pkg_V1_CN4_5)| ? false : true)) in
  (let localvar_res_pkg_V1_14 == ((returnvar_13 ? test_internal_pkg_F(localvar_s_pkg_V1_CN4_5, localvar_needle_pkg_V1_CN5_6 + localvar_found_pkg_V2_10, localvar_i_pkg_V1_CN6_11) : localvar_res_pkg_V1_12)) in
  (let returnvar_15 == (false) in
  (let localvar_res_pkg_V1_16 == ((returnvar_15 ? localvar_res_pkg_V1_CN7_4 : localvar_res_pkg_V1_14)) in
  localvar_res_pkg_V1_16))))))))))))))))
}