Function mk_liveness_array

ir/memory.cpp:1425–1432

}

static expr mk_liveness_array() {
  if (!num_nonlocals)
    return {};

  // consider all non_locals are initially alive
  // block size can still be 0 to invalidate accesses
  return expr::mkInt(-1, num_nonlocals);
}

expr Memory::mkSubByteZExtStoreCond(const Byte &val, const Byte &val2) const {
  bool mk_axiom = &val == &val2;