diff --git a/ir/memory.cpp b/ir/memory.cpp
index 2318b0077..d687ee1de 100644
--- a/ir/memory.cpp
+++ b/ir/memory.cpp
@@ -2048,10 +2048,45 @@ expr Memory::ptr2int(const expr &ptr) const {
   return p.getAddress();
 }
 
-expr Memory::int2ptr(const expr &val) const {
+expr Memory::int2ptr(const expr &val0) const {
   assert(!memory_unused() && observesAddresses());
   if (state->getFn().getFnAttrs().has(FnAttrs::Asm)) {
     DisjointExpr<expr> ret(expr{});
+    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");
+      if (blks.empty()) {
+        expr subst = false;
+        if (cond.isNot(cond))
+          subst = true;
+        val = val.subst(cond, subst);
+        continue;
+      }
+      if (blks.size() == 1) {
+        expr bid = blks.begin()->getFnArg(0);
+        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();
+
+    val = val.simplify();
+
     expr valx = val.zextOrTrunc(bits_program_pointer);
 
     auto add = [&](unsigned limit, bool local) {
@@ -2068,9 +2103,9 @@ expr Memory::int2ptr(const expr &val) const {
   }
 
   expr null = Pointer::mkNullPointer(*this).release();
-  expr fn = expr::mkUF("int2ptr", { val }, null);
+  expr fn = expr::mkUF("int2ptr", { val0 }, null);
   state->doesApproximation("inttoptr", fn);
-  return expr::mkIf(val == 0, null, fn);
+  return expr::mkIf(val0 == 0, null, fn);
 }
 
 expr Memory::blockValRefined(const Memory &other, unsigned bid, bool local,
diff --git a/smt/expr.cpp b/smt/expr.cpp
index af292305a..7cecf2964 100644
--- a/smt/expr.cpp
+++ b/smt/expr.cpp
@@ -2240,6 +2240,29 @@ set<expr> expr::leafs(unsigned max) const {
   return ret;
 }
 
+set<expr> expr::get_apps_of(const char *fn_name) const {
+  C();
+  vector<expr> worklist = { *this };
+  unordered_set<Z3_ast> seen;
+  set<expr> ret;
+  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));
+    }
+
+    if (val.fn_name() == fn_name) {
+      ret.emplace(std::move(val));
+    }
+  } while (!worklist.empty());
+
+  return ret;
+}
+
 void expr::printUnsigned(ostream &os) const {
   os << numeral_string();
 }
diff --git a/smt/expr.h b/smt/expr.h
index 421d51688..5d9367074 100644
--- a/smt/expr.h
+++ b/smt/expr.h
@@ -360,6 +360,8 @@ class expr {
 
   std::set<expr> leafs(unsigned max = 64) const;
 
+  std::set<expr> get_apps_of(const char *fn_name) const;
+
   void printUnsigned(std::ostream &os) const;
   void printSigned(std::ostream &os) const;
   void printHexadecimal(std::ostream &os) const;