diff --git a/ir/instr.cpp b/ir/instr.cpp
index 806666725..7d4841ac2 100644
--- a/ir/instr.cpp
+++ b/ir/instr.cpp
@@ -2682,9 +2682,24 @@ StateValue FnCall::toSMT(State &s) const {
   };
 
   if (attrs.has(AllocKind::Alloc) ||
-      attrs.has(AllocKind::Realloc) ||
-      attrs.has(FnAttrs::AllocSize)) {
-    auto [size, np_size] = attrs.computeAllocSize(s, args);
+      attrs.has(AllocKind::Realloc)) {
+
+    smt::expr size;
+    smt::expr np_size;
+    
+    if (!attrs.has(FnAttrs::AllocSize)) {
+      auto result = s.addFnCall(std::move(fnName_mangled).str(), std::move(inputs),
+                         std::move(ptr_inputs), getType(), std::move(ret_val),
+                         ret_arg_ty, std::move(ret_vals), attrs, indirect_hash);
+      auto retval =std::move(result.retval);
+      size = std::move(result.alloc_size.value());
+      np_size = expr(true);
+    } else {
+      auto result = attrs.computeAllocSize(s, args);
+      size = std::move(result.first);
+      np_size = std::move(result.second);
+    }
+
     expr nonnull = attrs.isNonNull() ? expr(true)
                                      : expr::mkBoolVar("malloc_never_fails");
     // FIXME: alloc-family below
@@ -2755,7 +2770,7 @@ StateValue FnCall::toSMT(State &s) const {
     return {};
   }
 
-  auto ret = s.addFnCall(std::move(fnName_mangled).str(), std::move(inputs),
+  auto [ret, alloc_size] = s.addFnCall(std::move(fnName_mangled).str(), std::move(inputs),
                          std::move(ptr_inputs), getType(), std::move(ret_val),
                          ret_arg_ty, std::move(ret_vals), attrs, indirect_hash);
 
diff --git a/ir/memory.cpp b/ir/memory.cpp
index 96b213baa..96d046cab 100644
--- a/ir/memory.cpp
+++ b/ir/memory.cpp
@@ -1717,6 +1717,7 @@ void Memory::syncWithSrc(const Memory &src) {
   next_nonlocal_bid = src.next_nonlocal_bid;
   ptr_alias = src.ptr_alias;
   // TODO: copy alias info for fn return ptrs from src?
+  
 }
 
 void Memory::markByVal(unsigned bid, bool is_const) {
diff --git a/ir/state.cpp b/ir/state.cpp
index 8f863a2cc..3015a72ce 100644
--- a/ir/state.cpp
+++ b/ir/state.cpp
@@ -1081,7 +1081,7 @@ expr State::FnCallOutput::refines(const FnCallOutput &rhs,
   return ret;
 }
 
-StateValue
+State::FnCallResult
 State::addFnCall(const string &name, vector<StateValue> &&inputs,
                  vector<PtrInput> &&ptr_inputs,
                  const Type &out_type, StateValue &&ret_arg,
@@ -1090,7 +1090,8 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
   bool noret   = attrs.has(FnAttrs::NoReturn);
   bool willret = attrs.has(FnAttrs::WillReturn);
   bool noundef = attrs.has(FnAttrs::NoUndef);
-  bool noalias = attrs.has(FnAttrs::NoAlias);
+  bool noalias = (attrs.has(FnAttrs::NoAlias)) || 
+              (attrs.has(AllocKind::Alloc) && !attrs.has(FnAttrs::AllocSize));
   bool is_indirect = name.starts_with("#indirect_call");
 
   expr fn_ptr_bid;
@@ -1278,8 +1279,17 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
     addUB(I->second.ub);
     addNoReturn(I->second.noreturns);
     retval = I->second.retval;
+
+    optional<expr> alloc_size;
+    if (noalias && out_type.isPtrType() && !I->second.ret_data.empty()) {
+      alloc_size = I->second.ret_data[0].size;
+    }
+    
     memory.setState(I->second.callstate, memaccess, I->first.args_ptr,
                     inaccessible_bid);
+
+
+    return { std::move(retval), std::move(alloc_size) };
   }
   else {
     // target: this fn call must match one from the source, otherwise it's UB
@@ -1336,15 +1346,23 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
       fn_call_pre &= pre;
       if (qvar.isValid())
         fn_call_qvars.emplace(std::move(qvar));
+
+      // Extract allocation size for noalias functions returning pointers
+      optional<expr> alloc_size;
+      if (noalias && out_type.isPtrType() && !d.ret_data.empty()) {
+        alloc_size = d.ret_data[0].size;
+      }
+
+      analysis.ranges_fn_calls.inc(name, memaccess);
+      return { std::move(retval), std::move(alloc_size) };
     } else {
       addUB(expr(false));
       retval = out_type.getDummyValue(false);
+
+      analysis.ranges_fn_calls.inc(name, memaccess);
+      return { std::move(retval), std::nullopt };
     }
   }
-
-  analysis.ranges_fn_calls.inc(name, memaccess);
-
-  return retval;
 }
 
 void State::doesApproximation(string &&name, optional<expr> e,
diff --git a/ir/state.h b/ir/state.h
index 1cfd6a906..7b0ddbdad 100644
--- a/ir/state.h
+++ b/ir/state.h
@@ -240,6 +240,14 @@ class State {
     smt::expr refines(const FnCallOutput &rhs, const Type &retval_ty) const;
     auto operator<=>(const FnCallOutput &rhs) const = default;
   };
+
+  struct FnCallResult {
+    StateValue retval;
+    std::optional<smt::expr> alloc_size;
+  };
+
+  // Add non-deterministic local_blk_size variable member and pending variable to access it
+
   std::map<std::string, std::map<FnCallInput, FnCallOutput>> fn_call_data;
   smt::expr fn_call_pre = true;
   std::set<smt::expr> fn_call_qvars;
@@ -308,7 +316,7 @@ class State {
   void addNoReturn(const smt::expr &cond);
   bool isViablePath() const { return domain.UB; }
 
-  StateValue
+  FnCallResult
     addFnCall(const std::string &name, std::vector<StateValue> &&inputs,
               std::vector<PtrInput> &&ptr_inputs,
               const Type &out_type,