diff --git a/ir/instr.cpp b/ir/instr.cpp
index 58b6d27f1..d21094c16 100644
--- a/ir/instr.cpp
+++ b/ir/instr.cpp
@@ -3774,12 +3774,14 @@ StateValue GEP::toSMT(State &s) const {
   auto scalar = [&](const StateValue &ptrval,
                     vector<pair<uint64_t, StateValue>> &offsets) -> StateValue {
     Pointer ptr(s.getMemory(), ptrval.value);
+    Pointer ptr_log = inbounds ? ptr.toLogical().first : ptr;
     AndExpr non_poison(ptrval.non_poison);
     AndExpr inbounds_np;
     AndExpr idx_all_zeros;
 
+    // FIXME: this is only partially implemented for physical pointers
     if (inbounds)
-      inbounds_np.add(ptr.inbounds());
+      inbounds_np.add(ptr_log.inbounds());
 
     expr offset_sum = expr::mkUInt(0, bits_for_offset);
     for (auto &[sz, idx] : offsets) {
@@ -3794,7 +3796,7 @@ StateValue GEP::toSMT(State &s) const {
       if (nusw) {
         non_poison.add(val.sextOrTrunc(v.bits()) == v);
         non_poison.add(multiplier.mul_no_soverflow(val));
-        non_poison.add(ptr.addNoUSOverflow(inc, inbounds));
+        non_poison.add(ptr_log.addNoUSOverflow(inc, inbounds));
         if (!inbounds) {
           // For non-inbounds gep, we have to explicitly check that adding the
           // offsets without the base address also doesn't wrap.
@@ -3806,7 +3808,7 @@ StateValue GEP::toSMT(State &s) const {
       if (nuw) {
         non_poison.add(val.zextOrTrunc(v.bits()) == v);
         non_poison.add(multiplier.mul_no_uoverflow(val));
-        non_poison.add(ptr.addNoUOverflow(inc, inbounds));
+        non_poison.add(ptr_log.addNoUOverflow(inc, inbounds));
       }
 
 #ifndef NDEBUG
@@ -3818,8 +3820,10 @@ StateValue GEP::toSMT(State &s) const {
       ptr += inc;
       non_poison.add(np);
 
-      if (inbounds)
-        inbounds_np.add(ptr.inbounds());
+      if (inbounds) {
+        ptr_log += inc;
+        inbounds_np.add(ptr_log.inbounds());
+      }
     }
 
     if (inbounds) {
diff --git a/ir/memory.cpp b/ir/memory.cpp
index 4502f7b5c..33ac34ae5 100644
--- a/ir/memory.cpp
+++ b/ir/memory.cpp
@@ -1512,6 +1512,9 @@ expr Memory::mkInput(const char *name, const ParamAttrs &attrs0) {
   unsigned max_bid = has_null_block + num_globals_src + next_ptr_input++;
   assert(max_bid < num_nonlocals_src);
 
+  // FIXME: doesn't consider physical ptrs
+  // consider how to do POR?
+
   auto attrs = attrs0;
   attrs.set(ParamAttrs::IsArg);
   Pointer p(*this, name, false, false, false, attrs);
@@ -2274,86 +2277,10 @@ expr Memory::ptr2int(const expr &ptr) const {
   return p.getAddress();
 }
 
-Pointer Memory::searchPointer(const expr &val0) const {
-  DisjointExpr<Pointer> ret;
-  expr val = val0.zextOrTrunc(bits_ptr_address);
-
-  auto add = [&](unsigned limit, bool local) {
-    for (unsigned i = 0; i != limit; ++i) {
-      Pointer p(*this, i, local);
-      Pointer p_end = p + p.blockSize();
-      ret.add(p + (val - p.getAddress()),
-              !local && i == 0 && has_null_block
-                ? val == 0
-                : val.uge(p.getAddress()) && val.ult(p_end.getAddress()));
-    }
-  };
-  add(numLocals(), true);
-  add(numNonlocals(), false);
-  return *std::move(ret)();
-}
-
-expr Memory::int2ptr(const expr &val0) const {
+expr Memory::int2ptr(const expr &val) const {
   assert(!memory_unused() && observesAddresses());
-  if (isAsmMode()) {
-    DisjointExpr<expr> ret(Pointer::mkNullPointer(*this).release());
-    expr val = val0;
-    OrExpr domain;
-    bool processed_all = true;
-
-    // Try to optimize the conversion
-    // Note that the result of int2ptr is always used to dereference the ptr
-    // Hence we can throw away null & OOB pointers
-    // Also, these pointers must have originated from ptr->int type punning
-    // so they must have a (blk_addr bid) expression in them (+ some offset)
-    for (auto [e, cond] : DisjointExpr<expr>(val, 5)) {
-      auto blks = e.get_apps_of("blk_addr", "local_addr!");
-      if (blks.empty()) {
-        expr subst = false;
-        if (cond.isNot(cond))
-          subst = true;
-        val = val.subst(cond, subst);
-        continue;
-      }
-      // There's only one possible bid in this expression
-      if (blks.size() == 1) {
-        auto &fn = *blks.begin();
-        expr bid;
-        if (fn.fn_name().starts_with("local_addr!")) {
-          for (auto &[bid0, addr] : local_blk_addr) {
-            auto blks = addr.get_apps_of("blk_addr", "local_addr!");
-            assert(blks.size() == 1);
-            if (blks.begin()->eq(fn)) {
-              bid = Pointer::mkLongBid(bid0, true);
-              break;
-            }
-          }
-        } else {
-          // non-local block
-          assert(fn.fn_name() == "blk_addr");
-          bid = Pointer::mkLongBid(fn.getFnArg(0), false);
-        }
-        assert(bid.isValid());
-        Pointer base(*this, bid, expr::mkUInt(0, bits_for_offset));
-        expr offset = (e - base.getAddress()).sextOrTrunc(bits_for_offset);
-        ret.add(Pointer(*this, bid, offset).release(), cond);
-      } else {
-        processed_all = false;
-      }
-      domain.add(std::move(cond));
-    }
-    state->addUB(std::move(domain)());
-
-    if (processed_all)
-      return std::move(ret)()->simplify();
-
-    return searchPointer(val.simplify()).release();
-  }
-
-  expr null = Pointer::mkNullPointer(*this).release();
-  expr fn = expr::mkUF("int2ptr", { val0 }, null);
-  state->doesApproximation("inttoptr", fn);
-  return expr::mkIf(val0 == 0, null, fn);
+  return
+    Pointer::mkPhysical(*this, val.zextOrTrunc(bits_ptr_address)).release();
 }
 
 expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local,
diff --git a/ir/memory.h b/ir/memory.h
index ce1a1f0c7..e3b9acc75 100644
--- a/ir/memory.h
+++ b/ir/memory.h
@@ -349,7 +349,6 @@ class Memory {
 
   smt::expr ptr2int(const smt::expr &ptr) const;
   smt::expr int2ptr(const smt::expr &val) const;
-  Pointer searchPointer(const smt::expr &val) const;
 
   std::tuple<smt::expr, Pointer, std::set<smt::expr>>
     refined(const Memory &other, bool fncall,
diff --git a/ir/pointer.cpp b/ir/pointer.cpp
index df5bf370e..41e625cc9 100644
--- a/ir/pointer.cpp
+++ b/ir/pointer.cpp
@@ -13,6 +13,38 @@ using namespace smt;
 using namespace std;
 using namespace util;
 
+#define return_mkIf_phy(T, phy, log) \
+  auto islogical = isLogical();      \
+  if (islogical.isTrue())            \
+    return log;                      \
+  if (islogical.isFalse())           \
+    return phy;                      \
+  return T::mkIf(islogical, log, phy)
+
+static bool hasLogicalBit() {
+  return true;
+}
+
+static unsigned total_bits_logical() {
+  return hasLogicalBit() + bits_for_ptrattrs + bits_for_bid + bits_for_offset;
+}
+
+static unsigned total_bits_physical() {
+  return hasLogicalBit() * (1 + bits_for_ptrattrs + bits_ptr_address);
+}
+
+static unsigned padding_logical() {
+  auto l = total_bits_logical();
+  auto p = total_bits_physical();
+  return l > p ? 0 : p - l;
+}
+
+static unsigned padding_physical() {
+  auto l = total_bits_logical();
+  auto p = total_bits_physical();
+  return p > l ? 0 : l - p;
+}
+
 static expr prepend_if(const expr &pre, expr &&e, bool prepend) {
   return prepend ? pre.concat(e) : std::move(e);
 }
@@ -50,7 +82,9 @@ static expr attr_to_bitvec(const ParamAttrs &attrs) {
 namespace IR {
 
 Pointer::Pointer(const Memory &m, const expr &bid, const expr &offset,
-                 const expr &attr) : m(m), p(bid.concat(offset)) {
+                 const expr &attr) : m(m),
+  p(prepend_if(expr::mkUInt(0, 1 + padding_logical()),
+               bid.concat(offset), hasLogicalBit())) {
   if (bits_for_ptrattrs)
     p = p.concat(attr);
   assert(!bid.isValid() || !offset.isValid() || p.bits() == totalBits());
@@ -59,8 +93,10 @@ Pointer::Pointer(const Memory &m, const expr &bid, const expr &offset,
 Pointer::Pointer(const Memory &m, const char *var_name, const expr &local,
                  bool unique_name, bool align, const ParamAttrs &attr) : m(m) {
   unsigned bits = total_bits_short() + !align * zeroBitsShortOffset();
-  p = prepend_if(local.toBVBool(),
-                 expr::mkVar(var_name, bits, unique_name), hasLocalBit());
+  p = prepend_if(expr::mkUInt(0, 1 + padding_logical()),
+                 prepend_if(local.toBVBool(),
+                   expr::mkVar(var_name, bits, unique_name), hasLocalBit()),
+                 hasLogicalBit());
   if (align)
     p = p.concat_zeros(zeroBitsShortOffset());
   if (bits_for_ptrattrs)
@@ -74,10 +110,12 @@ Pointer::Pointer(const Memory &m, expr repr) : m(m), p(std::move(repr)) {
 
 Pointer::Pointer(const Memory &m, unsigned bid, bool local)
   : m(m), p(
-    prepend_if(expr::mkUInt(local, 1),
-               expr::mkUInt(bid, bitsShortBid())
-                 .concat_zeros(bits_for_offset + bits_for_ptrattrs),
-               hasLocalBit())) {
+    prepend_if(expr::mkUInt(0, 1 + padding_logical()),
+      prepend_if(expr::mkUInt(local, 1),
+                 expr::mkUInt(bid, bitsShortBid())
+                   .concat_zeros(bits_for_offset + bits_for_ptrattrs),
+                 hasLocalBit()),
+              hasLogicalBit())) {
   assert((local && bid < m.numLocals()) || (!local && bid < num_nonlocals));
   assert(p.bits() == totalBits());
 }
@@ -86,6 +124,22 @@ Pointer::Pointer(const Memory &m, const expr &bid, const expr &offset,
                  const ParamAttrs &attr)
   : Pointer(m, bid, offset, attr_to_bitvec(attr)) {}
 
+Pointer Pointer::mkPhysical(const Memory &m, const expr &addr) {
+  return mkPhysical(m, addr, expr::mkUInt(0, bits_for_ptrattrs));
+}
+
+Pointer Pointer::mkPhysical(const Memory &m, const expr &addr,
+                            const expr &attr) {
+  assert(hasLogicalBit());
+  assert(addr.bits() == bits_ptr_address);
+  auto p = expr::mkUInt(1, 1)
+           .concat_zeros(padding_physical())
+           .concat(addr);
+  if (bits_for_ptrattrs)
+    p = p.concat(attr);
+  return { m, std::move(p) };
+}
+
 expr Pointer::mkLongBid(const expr &short_bid, bool local) {
   assert((local  && (num_locals_src || num_locals_tgt)) ||
          (!local && num_nonlocals));
@@ -111,11 +165,13 @@ expr Pointer::mkUndef(State &s) {
   if (force_local || force_nonlocal)
     var = mkLongBid(var, force_local);
 
-  return var.concat_zeros(bits_for_ptrattrs);
+  // TODO: support undef phy pointers
+  return expr::mkUInt(0, 1 + padding_logical())
+           .concat(var).concat_zeros(bits_for_ptrattrs);
 }
 
 unsigned Pointer::totalBits() {
-  return bits_for_ptrattrs + bits_for_bid + bits_for_offset;
+  return max(total_bits_logical(), total_bits_physical());
 }
 
 unsigned Pointer::bitsShortBid() {
@@ -135,13 +191,17 @@ bool Pointer::hasLocalBit() {
   return (num_locals_src || num_locals_tgt) && num_nonlocals;
 }
 
-expr Pointer::isLocal(bool simplify) const {
+expr Pointer::isLogical() const {
+  return hasLogicalBit() ? p.sign() == 0 : true;
+}
+
+expr Pointer::isLogLocal(bool simplify) const {
   if (m.numLocals() == 0)
     return false;
   if (m.numNonlocals() == 0)
     return true;
 
-  auto bit = totalBits() - 1;
+  auto bit = bits_for_bid - 1 + bits_for_offset + bits_for_ptrattrs;
   expr local = p.extract(bit, bit);
 
   if (simplify) {
@@ -161,6 +221,15 @@ expr Pointer::isLocal(bool simplify) const {
   return local == 1;
 }
 
+expr Pointer::isLocal(bool simplify) const {
+  if (m.numLocals() == 0)
+    return false;
+  if (m.numNonlocals() == 0)
+    return true;
+
+  return toLogical().first.isLogLocal(simplify);
+}
+
 expr Pointer::isConstGlobal() const {
   auto bid = getShortBid();
   auto generic = bid.uge(has_null_block) &&
@@ -180,17 +249,30 @@ expr Pointer::isWritableGlobal() const {
          bid.ule(has_null_block + num_globals_src - 1);
 }
 
+expr Pointer::getLogBid() const {
+  auto start = bits_for_offset + bits_for_ptrattrs;
+  return p.extract(start + bits_for_bid - 1, start);
+}
+
+expr Pointer::getLogShortBid() const {
+  auto start = bits_for_offset + bits_for_ptrattrs;
+  return p.extract(start + bits_for_bid - 1 - hasLocalBit(), start);
+}
+
+expr Pointer::getLogOffset() const {
+  return p.extract(bits_for_offset + bits_for_ptrattrs - 1, bits_for_ptrattrs);
+}
+
 expr Pointer::getBid() const {
-  return p.extract(totalBits() - 1, bits_for_offset + bits_for_ptrattrs);
+  return toLogical().first.getLogBid();
 }
 
 expr Pointer::getShortBid() const {
-  return p.extract(totalBits() - 1 - hasLocalBit(),
-                   bits_for_offset + bits_for_ptrattrs);
+  return toLogical().first.getLogShortBid();
 }
 
 expr Pointer::getOffset() const {
-  return p.extract(bits_for_offset + bits_for_ptrattrs - 1, bits_for_ptrattrs);
+  return toLogical().first.getLogOffset();
 }
 
 expr Pointer::getOffsetSizet() const {
@@ -199,8 +281,8 @@ expr Pointer::getOffsetSizet() const {
 }
 
 expr Pointer::getShortOffset() const {
-  return p.extract(bits_for_offset + bits_for_ptrattrs - 1,
-                   bits_for_ptrattrs + zeroBitsShortOffset());
+  return toLogical().first.p.extract(bits_for_offset + bits_for_ptrattrs - 1,
+                                     bits_for_ptrattrs + zeroBitsShortOffset());
 }
 
 expr Pointer::getAttrs() const {
@@ -231,7 +313,7 @@ expr Pointer::getValue(const char *name, const FunctionExpr &local_fn,
 expr Pointer::getBlockBaseAddress(bool simplify) const {
   assert(Memory::observesAddresses());
 
-  auto bid = getShortBid();
+  auto bid = getLogShortBid();
   auto zero = expr::mkUInt(0, bits_ptr_address - hasLocalBit());
   // fast path for null ptrs
   auto non_local
@@ -244,14 +326,22 @@ expr Pointer::getBlockBaseAddress(bool simplify) const {
   if (auto local = m.local_blk_addr(bid)) {
     // Local block area is the upper half of the memory
     expr lc = hasLocalBit() ? expr::mkUInt(1, 1).concat(*local) : *local;
-    return expr::mkIf(isLocal(), lc, non_local);
+    return expr::mkIf(isLogLocal(), lc, non_local);
   } else
     return non_local;
 }
 
+expr Pointer::getLogAddress(bool simplify) const {
+  return getBlockBaseAddress(simplify)
+           + getLogOffset().zextOrTrunc(bits_ptr_address);
+}
+
 expr Pointer::getAddress(bool simplify) const {
-  return
-    getBlockBaseAddress(simplify) + getOffset().zextOrTrunc(bits_ptr_address);
+  return_mkIf_phy(expr, getPhysicalAddress(), getLogAddress(simplify));
+}
+
+expr Pointer::getPhysicalAddress() const {
+  return p.extract(bits_for_ptrattrs + bits_ptr_address - 1, bits_for_ptrattrs);
 }
 
 expr Pointer::blockSize() const {
@@ -273,8 +363,11 @@ Pointer Pointer::mkPointerFromNoAttrs(const Memory &m, const expr &e) {
 }
 
 Pointer Pointer::operator+(const expr &bytes) const {
-  return { m, getBid(), getOffset() + bytes.zextOrTrunc(bits_for_offset),
-           getAttrs() };
+  return_mkIf_phy(Pointer,
+    mkPhysical(m, getPhysicalAddress() + bytes.zextOrTrunc(bits_ptr_address),
+               getAttrs()),
+    (Pointer{m, getLogBid(),
+             getLogOffset() + bytes.zextOrTrunc(bits_for_offset), getAttrs()}));
 }
 
 Pointer Pointer::operator+(unsigned bytes) const {
@@ -282,14 +375,17 @@ Pointer Pointer::operator+(unsigned bytes) const {
 }
 
 void Pointer::operator+=(const expr &bytes) {
-  p = (*this + bytes).p;
+  *this = *this + bytes;
 }
 
 Pointer Pointer::maskOffset(const expr &mask) const {
-  return { m, getBid(),
-           ((getAddress() & mask.zextOrTrunc(bits_ptr_address))
-               - getBlockBaseAddress()).zextOrTrunc(bits_for_offset),
-           getAttrs() };
+  return_mkIf_phy(Pointer,
+    mkPhysical(m, getPhysicalAddress() & mask.zextOrTrunc(bits_ptr_address),
+               getAttrs()),
+    (Pointer{ m, getLogBid(),
+              ((getLogAddress() & mask.zextOrTrunc(bits_ptr_address))
+                 - getBlockBaseAddress()).zextOrTrunc(bits_for_offset),
+              getAttrs() }));
 }
 
 expr Pointer::addNoUSOverflow(const expr &offset, bool offset_only) const {
@@ -372,7 +468,7 @@ expr Pointer::isAligned(uint64_t align) {
 
   // TODO: allow this in more cases. for example when the block is local
   // and addresses are not observed.
-  if (blk_align.isConst() && offset.isConst()) {
+  if (blk_align.isConst() && offset.isConst() && isLogical().isTrue()) {
     // This is stricter than checking getAddress(), but as addresses are not
     // observed, program shouldn't be able to distinguish this from checking
     // getAddress()
@@ -443,7 +539,7 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
   DisjointExpr<expr> UB(expr(false)), is_aligned(expr(false)), all_ptrs;
 
   for (auto &[ptr_expr, domain] : DisjointExpr<expr>(p, 3)) {
-    Pointer ptr(m, ptr_expr);
+    auto [ptr, inboundsd] = Pointer(m, ptr_expr).toLogical();
     auto [ub, aligned] = ::is_dereferenceable(ptr, bytes_off, bytes, align,
                                               iswrite, ignore_accessability);
 
@@ -451,8 +547,8 @@ Pointer::isDereferenceable(const expr &bytes0, uint64_t align,
     if (!ub.isFalse() && !aligned.isFalse() && !ptr.blockSize().isZero())
       all_ptrs.add(std::move(ptr).release(), domain);
 
-    UB.add(std::move(ub), domain);
-    is_aligned.add(std::move(aligned), domain);
+    UB.add(ub && inboundsd, domain);
+    is_aligned.add(std::move(aligned), std::move(domain));
   }
 
   AndExpr exprs;
@@ -523,27 +619,32 @@ expr Pointer::isHeapAllocated() const {
 
 expr Pointer::refined(const Pointer &other) const {
   bool is_asm = other.m.isAsmMode();
+  auto [p1l, d1] = toLogical();
+  auto [p2l, d2] = other.toLogical();
 
   // This refers to a block that was malloc'ed within the function
-  expr local = other.isLocal();
-  local &= getAllocType() == other.getAllocType();
-  local &= blockSize() == other.blockSize();
-  local &= getOffset() == other.getOffset();
+  expr local = p2l.isLocal();
+  local &= p1l.getAllocType() == p2l.getAllocType();
+  local &= p1l.blockSize() == p2l.blockSize();
+  local &= p1l.getOffset() == p2l.getOffset();
   // Attributes are ignored at refinement.
 
   // TODO: this induces an infinite loop
   //local &= block_refined(other);
 
-  expr nonlocal = is_asm ? getAddress() == other.getAddress() : *this == other;
+  auto l1 = isLogical();
+  auto l2 = other.isLogical();
 
-  Pointer other_deref
-    = is_asm ? other.m.searchPointer(other.getAddress()) : other;
+  // FIXME: physical pointer refinement
+  expr nonlocal = expr::mkIf((l1 && l2) && !is_asm,
+                             *this == other,
+                             getAddress() == other.getAddress());
 
   return expr::mkIf(isNull(), other.isNull(),
-                    expr::mkIf(isLocal(), std::move(local), nonlocal) &&
-                      // FIXME: this should be disabled just for phy pointers
+                    expr::mkIf(p1l.isLocal(), std::move(local), nonlocal) &&
                       (is_asm ? expr(true)
-                        : isBlockAlive().implies(other_deref.isBlockAlive())));
+                              : (d1 && p1l.isBlockAlive())
+                                  .implies(p2l.isBlockAlive())));
 }
 
 expr Pointer::fninputRefined(const Pointer &other, set<expr> &undef,
@@ -577,16 +678,18 @@ expr Pointer::fninputRefined(const Pointer &other, set<expr> &undef,
   // TODO: this induces an infinite loop
   // block_refined(other);
 
-  expr nonlocal = is_asm ? getAddress() == other.getAddress() : *this == other;
+  auto l1 = isLogical();
+  auto l2 = other.isLogical();
 
-  Pointer other_deref
-    = is_asm ? other.m.searchPointer(other.getAddress()) : other;
+  // FIXME: physical pointer refinement
+  expr nonlocal = expr::mkIf((l1 && l2) && !is_asm,
+                             *this == other,
+                             getAddress() == other.getAddress());
 
   return expr::mkIf(isNull(), other.isNull(),
                     expr::mkIf(isLocal(), local, nonlocal) &&
-                      // FIXME: this should be disabled just for phy pointers
                       (is_asm ? expr(true)
-                        : isBlockAlive().implies(other_deref.isBlockAlive())));
+                              : isBlockAlive().implies(other.isBlockAlive())));
 }
 
 expr Pointer::isWritable() const {
@@ -674,6 +777,79 @@ expr Pointer::isNull() const {
   return *this == mkNullPointer(m);
 }
 
+pair<Pointer, expr> Pointer::findLogicalPointer(const expr &addr) const {
+  DisjointExpr<Pointer> ret;
+  expr val = addr.zextOrTrunc(bits_ptr_address);
+
+  auto add = [&](unsigned limit, bool local) {
+    for (unsigned i = 0; i != limit; ++i) {
+      Pointer p(m, i, local);
+      Pointer p_end = p + p.blockSize();
+      ret.add(p + (val - p.getAddress()),
+              !local && i == 0 && has_null_block
+                ? val == 0
+                : val.uge(p.getAddress()) && val.ult(p_end.getAddress()));
+    }
+  };
+  add(m.numLocals(), true);
+  add(m.numNonlocals(), false);
+  return { *std::move(ret)(), ret.domain() };
+}
+
+pair<Pointer, expr> Pointer::toLogical() const {
+  if (isLogical().isTrue())
+    return { *this, true };
+
+  DisjointExpr<Pointer> ret;
+  DisjointExpr<expr> leftover;
+
+  // Try to optimize the conversion
+  for (auto [e, cond] : DisjointExpr<expr>(p, 5)) {
+    Pointer p(m, e);
+    if (p.isLogical().isTrue()) {
+      ret.add(std::move(p), std::move(cond));
+      continue;
+    }
+
+    // (ptr2int p) + offset
+    // FIXME: this also matches arg + ((ptr2int p) - arg2)
+    auto blks = e.get_apps_of("blk_addr", "local_addr!");
+    // There's only one possible bid in this expression
+    if (blks.size() == 1) {
+      auto &fn = *blks.begin();
+      expr bid;
+      if (fn.fn_name().starts_with("local_addr!")) {
+        for (auto &[bid0, addr] : m.local_blk_addr) {
+          auto blks = addr.get_apps_of("blk_addr", "local_addr!");
+          assert(blks.size() == 1);
+          if (blks.begin()->eq(fn)) {
+            bid = Pointer::mkLongBid(bid0, true);
+            break;
+          }
+        }
+      } else {
+        // non-local block
+        assert(fn.fn_name() == "blk_addr");
+        bid = Pointer::mkLongBid(fn.getFnArg(0), false);
+      }
+      assert(bid.isValid());
+      Pointer base(m, bid, expr::mkUInt(0, bits_for_offset));
+      expr offset = (p.getAddress() - base.getAddress())
+                      .sextOrTrunc(bits_for_offset);
+      ret.add(Pointer(m, bid, offset), std::move(cond));
+    } else {
+      leftover.add(std::move(e), std::move(cond));
+    }
+  }
+
+  if (!leftover.empty()) {
+    auto [ptr, domain] = findLogicalPointer(*std::move(leftover)());
+    ret.add(std::move(ptr), leftover.domain() && domain);
+  }
+
+  return { mkIf(isLogical(), *this, *std::move(ret)()), ret.domain() };
+}
+
 Pointer
 Pointer::mkIf(const expr &cond, const Pointer &then, const Pointer &els) {
   assert(&then.m == &els.m);
@@ -681,8 +857,10 @@ Pointer::mkIf(const expr &cond, const Pointer &then, const Pointer &els) {
 }
 
 ostream& operator<<(ostream &os, const Pointer &p) {
+  auto logical = p.isLogical();
+
   if (p.isNull().isTrue())
-    return os << "null";
+    return os << (logical.isFalse() ? "0x0" : "null");
 
 #define P(field, fn)   \
   if (field.isConst()) \
@@ -690,16 +868,28 @@ ostream& operator<<(ostream &os, const Pointer &p) {
   else                 \
     os << field
 
-  os << "pointer(";
-  if (p.isLocal().isConst())
-    os << (p.isLocal().isTrue() ? "local" : "non-local");
-  else
-    os << "local=" << p.isLocal();
-  os << ", block_id=";
-  P(p.getShortBid(), printUnsigned);
+  os << (logical.isFalse() ? "phy-ptr(" : "pointer(");
 
-  os << ", offset=";
-  P(p.getOffset(), printSigned);
+  bool needs_comma = false;
+  if (!logical.isFalse()) {
+    if (p.isLocal().isConst())
+      os << (p.isLocal().isTrue() ? "local" : "non-local");
+    else
+      os << "local=" << p.isLocal();
+    os << ", block_id=";
+    P(p.getShortBid(), printUnsigned);
+
+    os << ", offset=";
+    P(p.getOffset(), printSigned);
+    needs_comma = true;
+  }
+  if (auto addr = p.getPhysicalAddress();
+      addr.isConst() || logical.isFalse()) {
+    if (needs_comma)
+      os << ", ";
+    os << "address=";
+    P(addr, printUnsigned);
+  }
 
   if (bits_for_ptrattrs && !p.getAttrs().isZero()) {
     os << ", attrs=";
diff --git a/ir/pointer.h b/ir/pointer.h
index 3e93f1ff4..c19961400 100644
--- a/ir/pointer.h
+++ b/ir/pointer.h
@@ -17,7 +17,8 @@ class Memory;
 class Pointer {
   const Memory &m;
 
-  // [bid, offset, attributes (1 bit for each)]
+  // [0, padding, bid, offset, attributes (1 bit for each)] -- logical pointer
+  // [1, padding, address, attributes] -- physical pointer
   // The top bit of bid is 1 if the block is local, 0 otherwise.
   // A local memory block is a memory block that is
   // allocated by an instruction during the current function call. This does
@@ -46,10 +47,18 @@ class Pointer {
   Pointer(const Memory &m, const smt::expr &bid, const smt::expr &offset,
           const ParamAttrs &attr = {});
 
+  static Pointer mkPhysical(const Memory &m, const smt::expr &addr);
+  static Pointer mkPhysical(const Memory &m, const smt::expr &addr,
+                            const smt::expr &attr);
+
   Pointer(const Pointer &other) noexcept = default;
   Pointer(Pointer &&other) noexcept = default;
   void operator=(Pointer &&rhs) noexcept { p = std::move(rhs.p); }
 
+  // returns (log-ptr, domain of inboundness)
+  std::pair<Pointer, smt::expr> findLogicalPointer(const smt::expr &addr) const;
+  std::pair<Pointer, smt::expr> toLogical() const;
+
   static smt::expr mkLongBid(const smt::expr &short_bid, bool local);
   static smt::expr mkUndef(State &s);
 
@@ -59,10 +68,19 @@ class Pointer {
   static unsigned zeroBitsShortOffset();
   static bool hasLocalBit();
 
+  smt::expr isLogical() const;
+
   smt::expr isLocal(bool simplify = true) const;
   smt::expr isConstGlobal() const;
   smt::expr isWritableGlobal() const;
 
+  // these assume the pointer is logical
+  smt::expr isLogLocal(bool simplify = true) const;
+  smt::expr getLogBid() const;
+  smt::expr getLogShortBid() const;
+  smt::expr getLogOffset() const;
+  smt::expr getLogAddress(bool simplify = true) const;
+
   smt::expr getBid() const;
   smt::expr getShortBid() const; // same as getBid but ignoring is_local bit
   smt::expr getOffset() const;
@@ -71,6 +89,7 @@ class Pointer {
   smt::expr getAttrs() const;
   smt::expr getBlockBaseAddress(bool simplify = true) const;
   smt::expr getAddress(bool simplify = true) const;
+  smt::expr getPhysicalAddress() const;
 
   smt::expr blockSize() const;
   smt::expr blockSizeOffsetT() const; // to compare with offsets
diff --git a/smt/exprs.cpp b/smt/exprs.cpp
index fb2cef1f4..2c0a4d48c 100644
--- a/smt/exprs.cpp
+++ b/smt/exprs.cpp
@@ -66,6 +66,11 @@ ostream &operator<<(ostream &os, const AndExpr &e) {
 }
 
 
+void OrExpr::add(const expr &e) {
+  if (!e.isFalse())
+    exprs.emplace(e);
+}
+
 void OrExpr::add(expr &&e) {
   if (!e.isFalse())
     exprs.insert(std::move(e));
diff --git a/smt/exprs.h b/smt/exprs.h
index 5ac924d00..546cd2dc3 100644
--- a/smt/exprs.h
+++ b/smt/exprs.h
@@ -42,6 +42,7 @@ class OrExpr {
   std::set<expr> exprs;
 
 public:
+  void add(const expr &e);
   void add(expr &&e);
   void add(const OrExpr &other);
   expr operator()() const;
@@ -120,6 +121,14 @@ class DisjointExpr {
 
   std::optional<T> operator()() && { return std::move(*this).mk({}); }
 
+  expr domain() const {
+    OrExpr ret;
+    for (auto &[val, domain] : vals) {
+      ret.add(domain);
+    }
+    return std::move(ret)();
+  }
+
   std::optional<T> lookup(const expr &domain) const {
     for (auto &[v, d] : vals) {
       if (d.eq(domain))
@@ -131,6 +140,7 @@ class DisjointExpr {
   auto begin() const { return vals.begin(); }
   auto end() const   { return vals.end(); }
   auto size() const  { return vals.size(); }
+  bool empty() const { return vals.empty() && !default_val; }
 };
 
 
diff --git a/tests/alive-tv/asm/gep_mem.srctgt.ll b/tests/alive-tv/asm/gep_mem.srctgt.ll
new file mode 100644
index 000000000..41cb3d5ff
--- /dev/null
+++ b/tests/alive-tv/asm/gep_mem.srctgt.ll
@@ -0,0 +1,16 @@
+; TEST-ARGS: -tgt-is-asm
+@G = external global ptr, align 8
+
+define void @src(ptr %0) {
+   %LGV = load ptr, ptr %0, align 8
+   %G1 = getelementptr i8, ptr %LGV, i64 8
+   store ptr %G1, ptr @G, align 8
+   ret void
+}
+
+define void @tgt(ptr %0) {
+   %a3_1 = load i64, ptr %0, align 8
+   %a6_1 = add i64 %a3_1, 8
+   store i64 %a6_1, ptr @G, align 8
+   ret void
+}
diff --git a/tests/alive-tv/int2ptr/gep_cmp.srctgt.ll b/tests/alive-tv/int2ptr/gep_cmp.srctgt.ll
new file mode 100644
index 000000000..c948f3327
--- /dev/null
+++ b/tests/alive-tv/int2ptr/gep_cmp.srctgt.ll
@@ -0,0 +1,11 @@
+define i1 @src(ptr %0) {
+   %2 = getelementptr i8, ptr %0, i64 1
+   %3 = icmp ult ptr %2, %0
+   ret i1 %3
+}
+
+define i1 @tgt(ptr %0) {
+   %ptr = inttoptr i64 -1 to ptr
+   %a4_5.not = icmp eq ptr %0, %ptr
+   ret i1 %a4_5.not
+}
diff --git a/tests/alive-tv/int2ptr/intro.srctgt.ll b/tests/alive-tv/int2ptr/intro.srctgt.ll
new file mode 100644
index 000000000..4af852f0a
--- /dev/null
+++ b/tests/alive-tv/int2ptr/intro.srctgt.ll
@@ -0,0 +1,13 @@
+define ptr @src(ptr %0, i64 %1) {
+   %3 = icmp eq i64 %1, 0
+   %4 = select i1 %3, ptr null, ptr %0
+   ret ptr %4
+}
+
+define ptr @tgt(ptr %0, i64 %1) {
+   %3 = ptrtoint ptr %0 to i64
+   %a2_5 = icmp eq i64 %1, 0
+   %a3_6 = select i1 %a2_5, i64 0, i64 %3
+   %4 = inttoptr i64 %a3_6 to ptr
+   ret ptr %4
+}
diff --git a/tests/alive-tv/int2ptr.srctgt.ll b/tests/alive-tv/int2ptr/removal.srctgt.ll
similarity index 100%
rename from tests/alive-tv/int2ptr.srctgt.ll
rename to tests/alive-tv/int2ptr/removal.srctgt.ll
diff --git a/tools/transform.cpp b/tools/transform.cpp
index 1d83283ca..4958c3e27 100644
--- a/tools/transform.cpp
+++ b/tools/transform.cpp
@@ -187,7 +187,8 @@ static bool error(Errors &errs, State &src_state, State &tgt_state,
         // this *may* be a pointer
         if (bw == Pointer::totalBits()) {
           Pointer p(src_state.returnMemory(), var);
-          reduce(p.getOffset());
+          if (try_reduce(p.isLogical()))
+            reduce(p.getOffset());
           reduce(p.getAddress());
         }
       }
@@ -1209,6 +1210,10 @@ static void calculateAndInitConstants(Transform &t) {
   bits_for_offset = min(bits_for_offset, config::max_offset_bits);
   bits_for_offset = min(bits_for_offset, bits_program_pointer);
 
+  // we may have an implicit ptr2int through memory. Ensure we have enough bits
+  if (has_ptr_load && does_int_mem_access && t.tgt.has(FnAttrs::Asm))
+    bits_for_offset = bits_program_pointer;
+
   // ASSUMPTION: programs can only allocate up to half of address space
   // so the first bit of size is always zero.
   // We need this assumption to support negative offsets.
@@ -1230,7 +1235,7 @@ static void calculateAndInitConstants(Transform &t) {
                              bits_ptr_address) + has_local_bit,
                          bits_program_pointer);
 
-  if (config::tgt_is_asm)
+  if (t.tgt.has(FnAttrs::Asm))
     bits_ptr_address = bits_program_pointer;
 
   bits_byte = 8 * (does_mem_access ?  (unsigned)min_access_size : 1);