diff --git a/lib/Core/Executor.cpp b/lib/Core/Executor.cpp
index 9b7235b6a3..2dee00e49c 100644
--- a/lib/Core/Executor.cpp
+++ b/lib/Core/Executor.cpp
@@ -5471,6 +5471,100 @@ void Executor::executeFree(ExecutionState &state, ref<Expr> address,
   }
 }
 
+ExecutionState *Executor::handleNullPointerException(ExecutionState &state,
+                                                     ref<Expr> base) {
+  StatePair branches =
+      forkInternal(state, Expr::createIsZero(base), BranchType::MemOp);
+  ExecutionState *bound = branches.first;
+  if (!bound) {
+    return branches.second;
+  }
+
+  // If there are no markers on `malloc` returning nullptr,
+  // then `confidence` depends on presence of `unbound` state.
+  if (!bound->outOfMemoryMarkers.empty()) {
+    // bound constraints already contain `Expr::createIsZero()`
+    std::vector<const Array *> markersArrays;
+    markersArrays.reserve(bound->outOfMemoryMarkers.size());
+    findSymbolicObjects(bound->outOfMemoryMarkers.begin(),
+                        bound->outOfMemoryMarkers.end(), markersArrays);
+
+    // Do some iterations (2-3) to figure out if error is confident.
+    ref<Expr> allExcludedVectorsOfMarkers = Expr::createTrue();
+
+    bool convinced = false;
+    for (int tpCheckIteration = 0; tpCheckIteration < 2; ++tpCheckIteration) {
+      ref<SolverResponse> isConfidentResponse;
+      if (!solver->getResponse(bound->constraints.cs(),
+                               allExcludedVectorsOfMarkers, isConfidentResponse,
+                               bound->queryMetaData)) {
+        terminateStateOnSolverError(*bound, "Query timeout");
+      }
+
+      if (isa<ValidResponse>(isConfidentResponse)) {
+        reportStateOnTargetError(*bound,
+                                 ReachWithError::MustBeNullPointerException);
+
+        terminateStateOnProgramError(
+            *bound,
+            new ErrorEvent(locationOf(*bound), StateTerminationType::Ptr,
+                           "memory error: null pointer exception"),
+            StateTerminationConfidenceCategory::CONFIDENT);
+        convinced = true;
+        break;
+      }
+
+      // Receive current values of markers
+      std::vector<SparseStorage<unsigned char>> boundSetSolution;
+      isConfidentResponse->tryGetInitialValuesFor(markersArrays,
+                                                  boundSetSolution);
+      Assignment nonConfidentResponseAssignment(markersArrays,
+                                                boundSetSolution);
+
+      // Exclude this combinations of markers
+
+      ref<Expr> conjExcludedVectorOfMarkers = Expr::createTrue();
+      for (ref<Expr> marker : bound->outOfMemoryMarkers) {
+        conjExcludedVectorOfMarkers = AndExpr::create(
+            conjExcludedVectorOfMarkers,
+            EqExpr::create(marker,
+                           nonConfidentResponseAssignment.evaluate(marker)));
+      }
+
+      allExcludedVectorsOfMarkers =
+          OrExpr::create(allExcludedVectorsOfMarkers,
+                         NotExpr::create(conjExcludedVectorOfMarkers));
+    }
+
+    if (!convinced) {
+      reportStateOnTargetError(*bound,
+                               ReachWithError::MayBeNullPointerException);
+
+      terminateStateOnProgramError(
+          *bound,
+          new ErrorEvent(locationOf(*bound), StateTerminationType::Ptr,
+                         "memory error: null pointer exception"),
+          StateTerminationConfidenceCategory::PROBABLY);
+    }
+
+  } else {
+    auto error = branches.second != nullptr
+                     ? ReachWithError::MayBeNullPointerException
+                     : ReachWithError::MustBeNullPointerException;
+    reportStateOnTargetError(*bound, error);
+
+    terminateStateOnProgramError(
+        *bound,
+        new ErrorEvent(locationOf(*bound), StateTerminationType::Ptr,
+                       "memory error: null pointer exception"),
+        branches.second != nullptr
+            ? StateTerminationConfidenceCategory::PROBABLY
+            : StateTerminationConfidenceCategory::CONFIDENT);
+  }
+
+  return branches.second;
+}
+
 bool Executor::resolveExact(ExecutionState &estate, ref<Expr> address,
                             KType *type, ExactResolutionList &results,
                             const std::string &name) {
@@ -5496,20 +5590,12 @@ bool Executor::resolveExact(ExecutionState &estate, ref<Expr> address,
       Simplificator::simplifyExpr(estate.constraints.cs(), base).simplified;
   uniqueBase = toUnique(estate, uniqueBase);
 
-  StatePair branches =
-      forkInternal(estate, Expr::createIsZero(base), BranchType::MemOp);
-  ExecutionState *bound = branches.first;
-  if (bound) {
-    auto error = isReadFromSymbolicArray(uniqueBase)
-                     ? ReachWithError::MayBeNullPointerException
-                     : ReachWithError::MustBeNullPointerException;
-    terminateStateOnTargetError(*bound, error);
-  }
-  if (!branches.second) {
-    address = Expr::createPointer(0);
+  ExecutionState *handledNPEState = handleNullPointerException(estate, base);
+  if (!handledNPEState) {
+    return false;
   }
 
-  ExecutionState &state = *branches.second;
+  ExecutionState &state = *handledNPEState;
 
   ResolutionList rl;
   bool mayBeOutOfBound = true;
@@ -6266,97 +6352,9 @@ void Executor::executeMemoryOperation(
 
   ref<Expr> uniqueBase = toUnique(estate, base);
 
-  StatePair branches =
-      forkInternal(estate, Expr::createIsZero(base), BranchType::MemOp);
-  ExecutionState *bound = branches.first;
-
-  if (bound) {
-    // If there are no markers on `malloc` returning nullptr,
-    // then `confidence` depends on presence of `unbound` state.
-    if (!bound->outOfMemoryMarkers.empty()) {
-      // bound constraints already contain `Expr::createIsZero()`
-      std::vector<const Array *> markersArrays;
-      markersArrays.reserve(bound->outOfMemoryMarkers.size());
-      findSymbolicObjects(bound->outOfMemoryMarkers.begin(),
-                          bound->outOfMemoryMarkers.end(), markersArrays);
-
-      // Do some iterations (2-3) to figure out if error is confident.
-      ref<Expr> allExcludedVectorsOfMarkers = Expr::createTrue();
-
-      bool convinced = false;
-      for (int tpCheckIteration = 0; tpCheckIteration < 2; ++tpCheckIteration) {
-        ref<SolverResponse> isConfidentResponse;
-        if (!solver->getResponse(bound->constraints.cs(),
-                                 allExcludedVectorsOfMarkers,
-                                 isConfidentResponse, bound->queryMetaData)) {
-          terminateStateOnSolverError(*bound, "Query timeout");
-        }
-
-        if (isa<ValidResponse>(isConfidentResponse)) {
-          reportStateOnTargetError(*bound,
-                                   ReachWithError::MustBeNullPointerException);
-
-          terminateStateOnProgramError(
-              *bound,
-              new ErrorEvent(locationOf(*bound), StateTerminationType::Ptr,
-                             "memory error: null pointer exception"),
-              StateTerminationConfidenceCategory::CONFIDENT);
-          convinced = true;
-          break;
-        }
-
-        // Receive current values of markers
-        std::vector<SparseStorage<unsigned char>> boundSetSolution;
-        isConfidentResponse->tryGetInitialValuesFor(markersArrays,
-                                                    boundSetSolution);
-        Assignment nonConfidentResponseAssignment(markersArrays,
-                                                  boundSetSolution);
-
-        // Exclude this combinations of markers
-
-        ref<Expr> conjExcludedVectorOfMarkers = Expr::createTrue();
-        for (ref<Expr> marker : bound->outOfMemoryMarkers) {
-          conjExcludedVectorOfMarkers = AndExpr::create(
-              conjExcludedVectorOfMarkers,
-              EqExpr::create(marker,
-                             nonConfidentResponseAssignment.evaluate(marker)));
-        }
-
-        allExcludedVectorsOfMarkers =
-            OrExpr::create(allExcludedVectorsOfMarkers,
-                           NotExpr::create(conjExcludedVectorOfMarkers));
-      }
-
-      if (!convinced) {
-        reportStateOnTargetError(*bound,
-                                 ReachWithError::MayBeNullPointerException);
-
-        terminateStateOnProgramError(
-            *bound,
-            new ErrorEvent(locationOf(*bound), StateTerminationType::Ptr,
-                           "memory error: null pointer exception"),
-            StateTerminationConfidenceCategory::PROBABLY);
-      }
-
-    } else {
-      auto error = branches.second != nullptr
-                       ? ReachWithError::MayBeNullPointerException
-                       : ReachWithError::MustBeNullPointerException;
-      reportStateOnTargetError(*bound, error);
-
-      terminateStateOnProgramError(
-          *bound,
-          new ErrorEvent(locationOf(*bound), StateTerminationType::Ptr,
-                         "memory error: null pointer exception"),
-          branches.second != nullptr
-              ? StateTerminationConfidenceCategory::PROBABLY
-              : StateTerminationConfidenceCategory::CONFIDENT);
-    }
-  }
-
-  if (!branches.second)
+  ExecutionState *state = handleNullPointerException(estate, base);
+  if (!state)
     return;
-  ExecutionState *state = branches.second;
 
   // fast path: single in-bounds resolution
   IDType idFastResult;
@@ -6542,7 +6540,7 @@ void Executor::executeMemoryOperation(
           maxNewWriteableOSSize =
               std::max(maxNewWriteableOSSize, wos->getSparseStorageEntries());
           if (wos->readOnly) {
-            branches =
+            StatePair branches =
                 forkInternal(*state, Expr::createIsZero(unboundConditions[i]),
                              BranchType::MemOp);
             assert(branches.first);
diff --git a/lib/Core/Executor.h b/lib/Core/Executor.h
index b6a1b01c0e..8780de8aef 100644
--- a/lib/Core/Executor.h
+++ b/lib/Core/Executor.h
@@ -413,6 +413,9 @@ class Executor : public Interpreter {
                     const std::vector<Assignment> &resolveConcretizations,
                     std::vector<ref<Expr>> &results);
 
+  ExecutionState *handleNullPointerException(ExecutionState &state,
+                                             ref<Expr> base);
+
   // do address resolution / object binding / out of bounds checking
   // and perform the operation
   void executeMemoryOperation(ExecutionState &state, bool isWrite,