THEORY bitvectors8
LOGIC  QF_UFBV
SOLVER external

SIGNATURE
  bsearch: Int * (BitVec 8) * (BitVec 8) => result_1;
  u_1: Int * (BitVec 8) * (BitVec 8) * (BitVec 8) => result_1;
  u_2: Int * (BitVec 8) * (BitVec 8) * (BitVec 8) => result_1;
  u_3: Int * (BitVec 8) * (BitVec 8) * (BitVec 8) => result_1;
  error_1: result_1;
  u_4: Int * (BitVec 8) * (BitVec 8) * (BitVec 8) => result_1;
  u_5: Int * (BitVec 8) * (BitVec 8) * (BitVec 8) => result_1;
  u_6: Int * (BitVec 8) * (BitVec 8) * (BitVec 8) => result_1;
  u_7: Int * (BitVec 8) * (BitVec 8) * (BitVec 8) => result_1;
  return_1: (BitVec 8) => result_1;
  u_8: Int * (BitVec 8) * (BitVec 8) * (BitVec 8) => result_1;
  u_9: Int * (BitVec 8) * (BitVec 8) * (BitVec 8) => result_1;
  u_10: Int * (BitVec 8) * (BitVec 8) * (BitVec 8) => result_1;

RULES
  bsearch(k_1, lo_1, hi_1) -> u_1(k_1, lo_1, hi_1, rnd_1);
  u_1(k_1, lo_1, hi_1, mid_2) -> u_2(k_1, lo_1, hi_1, mid_2);
  u_2(k_1, lo_1, hi_1, mid_2) -> u_3(k_1, lo_1, hi_1, z)  [((lo_1 <u.8 hi_1) /\ (((lo_1 +.8 hi_1) /u.8 bv8"#x02") = z))];
  u_3(k_1, lo_1, hi_1, mid_2) -> u_4(k_1, z, hi_1, mid_2)  [((bv2int.8(mid_2) < k_1) /\ (z = (mid_2 +.8 bv8"#x01")))];
  u_4(k_1, lo_1, hi_1, mid_2) -> u_2(k_1, lo_1, hi_1, mid_2);
  u_3(k_1, lo_1, hi_1, mid_2) -> u_6(k_1, lo_1, z, mid_2)  [(((bv2int.8(mid_2) >= k_1) /\ (z = (mid_2 -.8 bv8"#x01"))))];
  u_6(k_1, lo_1, hi_1, mid_2) -> u_2(k_1, lo_1, hi_1, mid_2);
  u_3(k_1, lo_1, hi_1, mid_2) -> return_1(mid_2)  [((((bv2int.8(mid_2) >= k_1) ) /\ (bv2int.8(mid_2) <= k_1)) )];
  u_2(k_1, lo_1, hi_1, mid_2) -> return_1(bv8"#xff")  [(lo_1 >=u.8 hi_1)];

NON-STANDARD IRREGULAR

QUERY loops bsearch(K,L,H)
END OF FILE
QUERY loops bsearch(K,L,H)

int bsearch(int a[], int k, unsigned int lo, unsigned int hi) {
  unsigned int mid;
  while (lo < hi) {
    mid = (lo + hi)/2;
    if (a[mid] < k) {
    lo = mid + 1;
  } else if (a[mid] > k) {
    hi = mid - 1;
  } else {
    return mid;
  }
}
return -1;
}