diff --git a/ir/memory.cpp b/ir/memory.cpp
index 0bdbacb36..bab7af461 100644
--- a/ir/memory.cpp
+++ b/ir/memory.cpp
@@ -2051,7 +2051,7 @@ expr Memory::ptr2int(const expr &ptr) const {
 expr Memory::int2ptr(const expr &val0) const {
   assert(!memory_unused() && observesAddresses());
   if (state->getFn().getFnAttrs().has(FnAttrs::Asm)) {
-    DisjointExpr<expr> ret(expr{});
+    DisjointExpr<expr> ret(Pointer::mkNullPointer(*this).release());
     expr val = val0;
     OrExpr domain;
     bool processed_all = true;
@@ -2062,7 +2062,7 @@ expr Memory::int2ptr(const expr &val0) const {
     // 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");
+      auto blks = e.get_apps_of("blk_addr", "local_addr!");
       if (blks.empty()) {
         expr subst = false;
         if (cond.isNot(cond))
@@ -2070,8 +2070,23 @@ expr Memory::int2ptr(const expr &val0) const {
         val = val.subst(cond, subst);
         continue;
       }
+      // There's only only possible bid in this expression
       if (blks.size() == 1) {
-        expr bid = blks.begin()->getFnArg(0);
+        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 {
+          bid = fn.getFnArg(0);
+        }
+        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);
diff --git a/smt/expr.cpp b/smt/expr.cpp
index 7cecf2964..9a5ae62a9 100644
--- a/smt/expr.cpp
+++ b/smt/expr.cpp
@@ -812,8 +812,8 @@ expr expr::add_no_soverflow(const expr &rhs) const {
 
   if (rhs.isConst()) {
     auto v = IntSMin(bits()) - rhs;
-    return
-      rhs.isNegative().isTrue() ? sge(v) : sle(v - expr::mkUInt(1, sort()));
+    return rhs.isNegative().isTrue() ? sge(v)
+                                     : sle(v - expr::mkUInt(1, rhs.sort()));
   }
   if (isConst())
     return rhs.add_no_soverflow(*this);
@@ -2240,7 +2240,7 @@ set<expr> expr::leafs(unsigned max) const {
   return ret;
 }
 
-set<expr> expr::get_apps_of(const char *fn_name) const {
+set<expr> expr::get_apps_of(const char *fn_name, const char *prefix) const {
   C();
   vector<expr> worklist = { *this };
   unordered_set<Z3_ast> seen;
@@ -2248,14 +2248,15 @@ set<expr> expr::get_apps_of(const char *fn_name) const {
   do {
     auto val = std::move(worklist.back());
     worklist.pop_back();
-    if (!seen.emplace(val()).second || !val.isApp())
-      continue;
 
     for (unsigned i = 0, e = val.getFnNumArgs(); i < e; ++i) {
-      worklist.emplace_back(val.getFnArg(i));
+      expr arg = val.getFnArg(i);
+      if (arg.isApp() && seen.emplace(arg()).second)
+        worklist.emplace_back(std::move(arg));
     }
 
-    if (val.fn_name() == fn_name) {
+    auto str = val.fn_name();
+    if (str == fn_name || str.starts_with(prefix)) {
       ret.emplace(std::move(val));
     }
   } while (!worklist.empty());
diff --git a/smt/expr.h b/smt/expr.h
index 5d9367074..2720e5195 100644
--- a/smt/expr.h
+++ b/smt/expr.h
@@ -360,7 +360,7 @@ class expr {
 
   std::set<expr> leafs(unsigned max = 64) const;
 
-  std::set<expr> get_apps_of(const char *fn_name) const;
+  std::set<expr> get_apps_of(const char *fn_name, const char *prefix) const;
 
   void printUnsigned(std::ostream &os) const;
   void printSigned(std::ostream &os) const;
diff --git a/tests/alive-tv/asm/malloc-in-tgt.srctgt.ll b/tests/alive-tv/asm/malloc-in-tgt.srctgt.ll
new file mode 100644
index 000000000..cdb0fbfd5
--- /dev/null
+++ b/tests/alive-tv/asm/malloc-in-tgt.srctgt.ll
@@ -0,0 +1,22 @@
+; TEST-ARGS: -tgt-is-asm
+; SKIP-IDENTITY
+
+define i32 @src() {
+  %1 = alloca i8, i32 0, align 1
+  store i8 0, ptr %1, align 1
+  ret i32 0
+}
+
+define i32 @tgt() {
+f:
+  %stack = tail call dereferenceable(64) ptr @myalloc(i32 64)
+  %0 = getelementptr inbounds i8, ptr %stack, i64 48
+  %1 = ptrtoint ptr %0 to i64
+  %a0_38 = add i64 %1, -16
+  %2 = inttoptr i64 %a0_38 to ptr
+  %3 = getelementptr i8, ptr %2, i64 15
+  store i8 0, ptr %3, align 1
+  ret i32 0
+}
+
+declare ptr @myalloc(i32) local_unnamed_addr allockind("alloc") allocsize(0)