diff --git a/include/tsar/Analysis/Memory/AssumptionInfo.h b/include/tsar/Analysis/Memory/AssumptionInfo.h
new file mode 100644
index 00000000..3e176e35
--- /dev/null
+++ b/include/tsar/Analysis/Memory/AssumptionInfo.h
@@ -0,0 +1,69 @@
+//===- AssumptionInfo.h ----- Assumption Information ------------*- C++ -*-===//
+//
+//                     Traits Static Analyzer (SAPFOR)
+//
+// Copyright 2022 DVM System Group
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+//
+//===----------------------------------------------------------------------===//
+//
+// This file provides assumption information for memory locations with variable
+// bounds.
+//
+//===----------------------------------------------------------------------===/
+
+#ifndef TSAR_ASSUMPTION_INFO_H
+#define TSAR_ASSUMPTION_INFO_H
+
+#include "tsar/Analysis/Memory/Passes.h"
+#include <llvm/ADT/DenseMap.h>
+#include <llvm/Pass.h>
+#include <bcl/utility.h>
+
+namespace llvm {
+class Value;
+}
+
+namespace tsar {
+  typedef llvm::Optional<int64_t> AssumptionBound;
+  struct AssumptionBounds {
+    AssumptionBound Lower = llvm::None;
+    AssumptionBound Upper = llvm::None;
+  };
+
+  typedef llvm::DenseMap<llvm::Value *, AssumptionBounds> AssumptionMap; 
+}
+
+namespace llvm {
+class AssumptionInfoPass : public FunctionPass, private bcl::Uncopyable {
+public:
+  static char ID;
+
+  AssumptionInfoPass() : FunctionPass(ID) {
+    initializeAssumptionInfoPassPass(*PassRegistry::getPassRegistry());
+  }
+
+  bool runOnFunction(Function &F) override;
+  void getAnalysisUsage(AnalysisUsage &AU) const override;
+  void releaseMemory() override { mAM.clear(); }
+
+  const tsar::AssumptionMap & getAssumptionMap() const {
+    return mAM;
+  }
+private:
+  tsar::AssumptionMap mAM; 
+};
+}
+
+#endif //TSAR_ASSUMPTION_INFO_H
diff --git a/include/tsar/Analysis/Memory/DefinedMemory.h b/include/tsar/Analysis/Memory/DefinedMemory.h
index 6b9cab0b..53e6d944 100644
--- a/include/tsar/Analysis/Memory/DefinedMemory.h
+++ b/include/tsar/Analysis/Memory/DefinedMemory.h
@@ -52,6 +52,7 @@
 #include <llvm/Pass.h>
 
 namespace llvm {
+class AssumptionCache;
 class DominatorTree;
 class Value;
 class Instruction;
@@ -92,6 +93,11 @@ class DefUseSet {
   /// Set of memory locations.
   typedef MemorySet<MemoryLocationRange> LocationSet;
 
+  /// Set of data flow nodes with which memory locations from the 
+  /// ExplicitAccesses set are associated.
+  typedef llvm::SmallDenseMap<const llvm::Value *,
+      llvm::SmallDenseSet<const DFNode *>> ExplicitNodeMap;
+
   /// Returns set of the must defined locations.
   const LocationSet & getDefs() const { return mDefs; }
 
@@ -209,6 +215,25 @@ class DefUseSet {
     return mUses.insert(Uses.begin(), Uses.end());
   }
 
+  /// Replaced collapsed memory locations with its expanded forms which are 
+  /// of kind `Default`.
+  void summarizeCollapsedLocations() {
+    LocationSet DestDefs, DestMayDefs, DestUses;
+    for (auto &Loc : mDefs) {
+      if (Loc.Kind == MemoryLocationRange::LocKind::Collapsed)
+        DestMayDefs.insert(Loc.expand());
+      else
+        DestDefs.insert(Loc);
+    }
+    for (auto &Loc : mMayDefs)
+      DestMayDefs.insert(Loc.expand());
+    for (auto &Loc : mUses)
+      DestUses.insert(Loc.expand());
+    mDefs = std::move(DestDefs);
+    mMayDefs = std::move(DestMayDefs);
+    mUses = std::move(DestUses);
+  }
+
   /// Returns locations accesses to which are performed explicitly.
   ///
   /// For example, if p = &x and to access x, *p is used, let us assume that
@@ -367,6 +392,42 @@ class DefUseSet {
         .second;
   }
 
+  /// Inserts a data flow node associated with a collapsable explicit access
+  /// ExplLoc. ColLoc is a collapsed memory location created from the ExplLoc. 
+  void addNodeOfCollapsableExplicitAccess(
+      const MemoryLocationRange &ExplLoc,
+      const MemoryLocationRange &ColLoc,
+      const DFNode *N) {
+    assert(ExplLoc.Ptr && "Location pointer must not be null!");
+    assert(ColLoc.Kind == MemoryLocationRange::LocKind::Collapsed &&
+        "Location must be of a `collapsed` kind!");
+    mCollapsableExplicitAccesses.try_emplace(ExplLoc.Ptr).first->second.insert(N);
+  }
+
+  /// Returns a map of collapsable explicit accesses with associated data flow
+  /// nodes.
+  const ExplicitNodeMap & getCollapsableExplicitAccesses() const {
+    return mCollapsableExplicitAccesses;
+  }
+
+  /// Specifies that there are a collapsable explicit access to all collapsable 
+  /// explicit accesses from a specified map.
+  void addCollapsableExplicitAccesses(const ExplicitNodeMap &ENM) {
+    for (auto Itr = ENM.begin(); Itr != ENM.end(); ++Itr) {
+      auto &NodeList = Itr->second;
+      mCollapsableExplicitAccesses.try_emplace(Itr->first).
+          first->second.insert(NodeList.begin(), NodeList.end());
+    }
+  }
+
+  /// Returns a pointer to a set of data flow nodes associated with the memory 
+  /// location Loc if it is collabsable. Returns `nullptr` otherwise.
+  const llvm::SmallDenseSet<const DFNode *> *
+  getNodesOfCollapsableExplicitAccess(const MemoryLocationRange &Loc) const {
+    auto Itr = mCollapsableExplicitAccesses.find(Loc.Ptr);
+    return Itr == mCollapsableExplicitAccesses.end() ? nullptr : &Itr->second;
+  }
+
 private:
   LocationSet mDefs;
   LocationSet mMayDefs;
@@ -377,6 +438,7 @@ class DefUseSet {
   InstructionSet mExplicitUnknowns;
   InstructionSet mAddressUnknowns;
   TransitiveMap mAddressTransitives;
+  ExplicitNodeMap mCollapsableExplicitAccesses;
 };
 
 /// This presents information whether a location has definition after a node
@@ -430,29 +492,32 @@ class ReachDFFwk : private bcl::Uncopyable {
   ReachDFFwk(AliasTree &AT, llvm::TargetLibraryInfo &TLI,
       const DFRegionInfo &DFI, const llvm::DominatorTree &DT,
       const DelinearizeInfo &DI, llvm::ScalarEvolution &SE,
-      const llvm::DataLayout &DL, const GlobalOptions &GO,
-      DefinedMemoryInfo &DefInfo) :
+      const llvm::DataLayout &DL, const AssumptionMap &AM,
+      const GlobalOptions &GO, DefinedMemoryInfo &DefInfo) :
     mAliasTree(&AT), mTLI(&TLI), mRegionInfo(&DFI),
-    mDT(&DT), mDI(&DI), mSE(&SE), mDL(&DL), mGO(&GO), mDefInfo(&DefInfo) {}
+    mDT(&DT), mDI(&DI), mSE(&SE), mDL(&DL), mAM(&AM), mGO(&GO),
+    mDefInfo(&DefInfo) {}
 
   /// Creates data-flow framework.
   ReachDFFwk(AliasTree &AT, llvm::TargetLibraryInfo &TLI,
       const DFRegionInfo &DFI, const llvm::DominatorTree &DT,
       const DelinearizeInfo &DI, llvm::ScalarEvolution &SE,
-      const llvm::DataLayout &DL, const GlobalOptions &GO,
-      DefinedMemoryInfo &DefInfo, InterprocDefUseInfo &InterprocDUInfo) :
+      const llvm::DataLayout &DL, const AssumptionMap &AM,
+      const GlobalOptions &GO, DefinedMemoryInfo &DefInfo,
+      InterprocDefUseInfo &InterprocDUInfo) :
     mAliasTree(&AT), mTLI(&TLI), mRegionInfo(&DFI), mDT(&DT),
-    mDI(&DI), mSE(&SE), mDL(&DL), mGO(&GO), mDefInfo(&DefInfo),
+    mDI(&DI), mSE(&SE), mDL(&DL), mAM(&AM), mGO(&GO), mDefInfo(&DefInfo),
     mInterprocDUInfo(&InterprocDUInfo) {}
 
   /// Creates data-flow framework.
   ReachDFFwk(AliasTree &AT, llvm::TargetLibraryInfo &TLI,
       const llvm::DominatorTree &DT, const DelinearizeInfo &DI,
       llvm::ScalarEvolution &SE, const llvm::DataLayout &DL,
-      const GlobalOptions &GO, DefinedMemoryInfo &DefInfo,
-      InterprocDefUseInfo &InterprocDUInfo) :
+      const AssumptionMap &AM, const GlobalOptions &GO,
+      DefinedMemoryInfo &DefInfo, InterprocDefUseInfo &InterprocDUInfo) :
     mAliasTree(&AT), mTLI(&TLI), mDT(&DT), mDI(&DI), mSE(&SE), mDL(&DL),
-    mGO(&GO), mDefInfo(&DefInfo), mInterprocDUInfo(&InterprocDUInfo) {}
+    mGO(&GO), mAM(&AM), mDefInfo(&DefInfo),
+    mInterprocDUInfo(&InterprocDUInfo) {}
 
   /// Return results of interprocedural analysis or nullptr.
   InterprocDefUseInfo * getInterprocDefUseInfo() noexcept {
@@ -491,6 +556,11 @@ class ReachDFFwk : private bcl::Uncopyable {
   /// Returns data layout.
   const llvm::DataLayout & getDataLayout() const noexcept { return *mDL; }
 
+  /// Returns assumption map.
+  const AssumptionMap * getAssumptionMap() const noexcept {
+    return mAM;
+  }
+
   /// Returns global options.
   const GlobalOptions & getGlobalOptions() const noexcept { return *mGO; }
 
@@ -507,6 +577,7 @@ class ReachDFFwk : private bcl::Uncopyable {
   const DelinearizeInfo *mDI;
   llvm::ScalarEvolution *mSE;
   const llvm::DataLayout *mDL;
+  const AssumptionMap *mAM;
   const GlobalOptions *mGO;
 };
 
diff --git a/include/tsar/Analysis/Memory/MemoryLocationRange.h b/include/tsar/Analysis/Memory/MemoryLocationRange.h
index ae86613f..a7c5f0ef 100644
--- a/include/tsar/Analysis/Memory/MemoryLocationRange.h
+++ b/include/tsar/Analysis/Memory/MemoryLocationRange.h
@@ -25,10 +25,16 @@
 #ifndef TSAR_MEMORY_LOCATION_RANGE_H
 #define TSAR_MEMORY_LOCATION_RANGE_H
 
+#include "tsar/Analysis/Memory/AssumptionInfo.h"
 #include <llvm/ADT/APInt.h>
 #include <llvm/ADT/BitmaskEnum.h>
 #include <llvm/Analysis/MemoryLocation.h>
 
+namespace llvm {
+class ScalarEvolution;
+class SCEV;
+}
+
 namespace tsar {
 
 using LocationSize = llvm::LocationSize;
@@ -42,24 +48,37 @@ LLVM_ENABLE_BITMASK_ENUMS_IN_NAMESPACE();
 /// LowerBound is always 0.
 struct MemoryLocationRange {
   enum : uint64_t { UnknownSize = llvm::MemoryLocation::UnknownSize };
+  // There are several kinds of memory locations:
+  // * Default - the kind of memory locations corresponding to scalar variables
+  // or array memory locations can potentially be collapsed later.
+  // * NonCollapsable - the kind of memory locations that are not scalar, for
+  // which it has already been determined that collapse cannot be performed.
+  // * Collapsed - the kind of collapsed memory locations.
+  // * Hint - the kind of memory locations artificially added for correct
+  // private variables analysis.
+  // * Auxiliary - the kind of memory locations that intersect with some other
+  // memory location and are added to MemorySet as auxiliary, in order to take
+  // into account the fact that the same memory is being accessed.
   enum LocKind : uint8_t {
     Default = 0,
     NonCollapsable = 1u << 0,
     Collapsed = 1u << 1,
     Hint = 1u << 2,
-    LLVM_MARK_AS_BITMASK_ENUM(Hint)
+    Auxiliary = 1u << 3,
+    LLVM_MARK_AS_BITMASK_ENUM(Auxiliary)
   };
 
   struct Dimension {
-    uint64_t Start;
-    uint64_t Step;
-    uint64_t TripCount;
+    const llvm::SCEV *Start;
+    const llvm::SCEV *End;
+    const llvm::SCEV *Step;
     uint64_t DimSize;
-    Dimension() : Start(0), Step(0), TripCount(0), DimSize(0) {}
+    Dimension() : Start(nullptr), End(nullptr), Step(nullptr), DimSize(0) {}
     inline bool operator==(const Dimension &Other) const {
-      return Start == Other.Start && Step == Other.Step &&
-             TripCount == Other.TripCount && DimSize == Other.DimSize;
+      return Start == Other.Start && End == Other.End && Step == Other.Step &&
+             DimSize == Other.DimSize;
     }
+    void print(llvm::raw_ostream &OS, bool IsDebug = false) const;
   };
 
   const llvm::Value * Ptr;
@@ -68,6 +87,8 @@ struct MemoryLocationRange {
   llvm::SmallVector<Dimension, 0> DimList;
   llvm::AAMDNodes AATags;
   LocKind Kind;
+  llvm::ScalarEvolution *SE;
+  const AssumptionMap *AM;
 
   /// Return a location with information about the memory reference by the given
   /// instruction.
@@ -135,23 +156,26 @@ struct MemoryLocationRange {
                                LocationSize UpperBound = UnknownSize,
                                const llvm::AAMDNodes &AATags = llvm::AAMDNodes())
       : Ptr(Ptr), LowerBound(LowerBound), UpperBound(UpperBound),
-        AATags(AATags), Kind(LocKind::Default) {}
+        AATags(AATags), SE(nullptr), AM(nullptr), Kind(LocKind::Default) {}
 
   explicit MemoryLocationRange(const llvm::Value *Ptr,
                                LocationSize LowerBound,
                                LocationSize UpperBound,
                                LocKind Kind,
+                               llvm::ScalarEvolution *SE,
+                               AssumptionMap *AM,
                                const llvm::AAMDNodes &AATags = llvm::AAMDNodes())
-      : Ptr(Ptr), LowerBound(LowerBound), UpperBound(UpperBound),
-        AATags(AATags), Kind(Kind) {}
+      : Ptr(Ptr), LowerBound(LowerBound), UpperBound(UpperBound), Kind(Kind),
+        SE(SE), AM(AM), AATags(AATags) {}
 
   MemoryLocationRange(const llvm::MemoryLocation &Loc)
       : Ptr(Loc.Ptr), LowerBound(0), UpperBound(Loc.Size), AATags(Loc.AATags),
-        Kind(LocKind::Default) {}
+        Kind(LocKind::Default), SE(nullptr), AM(nullptr) {}
 
   MemoryLocationRange(const MemoryLocationRange &Loc)
       : Ptr(Loc.Ptr), LowerBound(Loc.LowerBound), UpperBound(Loc.UpperBound),
-        AATags(Loc.AATags), DimList(Loc.DimList), Kind(Loc.Kind) {}
+        AATags(Loc.AATags), DimList(Loc.DimList), Kind(Loc.Kind), SE(Loc.SE),
+        AM(Loc.AM) {}
 
   MemoryLocationRange &operator=(const llvm::MemoryLocation &Loc) {
     Ptr = Loc.Ptr;
@@ -159,13 +183,16 @@ struct MemoryLocationRange {
     UpperBound = Loc.Size;
     AATags = Loc.AATags;
     Kind = Default;
+    SE = nullptr;
+    AM = nullptr;
     return *this;
   }
 
   bool operator==(const MemoryLocationRange &Other) const {
     return Ptr == Other.Ptr && AATags == Other.AATags &&
       LowerBound == Other.LowerBound && UpperBound == Other.UpperBound &&
-      DimList == Other.DimList && Kind == Other.Kind;
+      DimList == Other.DimList && SE == Other.SE && AM == Other.AM &&
+      Kind == Other.Kind;
   }
 
   std::string getKindAsString() const {
@@ -183,8 +210,26 @@ struct MemoryLocationRange {
       append("Collapsed", KindStr);
     if (Kind & Hint)
       append("Hint", KindStr);
+    if (Kind & Auxiliary)
+      append("Auxiliary", KindStr);
     return KindStr;
   }
+
+  /// If the location is associated with an array, i.e. it has a non-empty list
+  /// of dimensions, convert it to an ordinary location with an empty list of
+  /// dimensions and return it. The new location covers the entire memory of 
+  /// the array, even though the dimensions are not completely used. 
+  MemoryLocationRange expand() const {
+    if (DimList.empty())
+      return *this;
+    assert(UpperBound.hasValue() && "UpperBound must have a value!");
+    auto FullSize = UpperBound.getValue();;
+    for (std::size_t I = 0; I < DimList.size(); ++I)
+      FullSize *= DimList[I].DimSize;
+    if (FullSize == 0)
+      return MemoryLocationRange(Ptr, 0, UnknownSize, AATags);
+    return MemoryLocationRange(Ptr, 0, LocationSize(FullSize), AATags);
+  }
 };
 
 /// \brief Finds an intersection between memory locations LHS and RHS.
@@ -204,8 +249,10 @@ struct MemoryLocationRange {
 /// exact differences will not be saved.
 /// \return The result of intersection. If it is None, intersection is empty.
 /// If it is a location, but `Ptr` of the returned location is `nullptr`, then
-/// the intersection may exist but can't be calculated. Otherwise, the
-/// returned location is an exact intersection.
+/// the intersection may exist but can't be calculated (note that you will get
+/// the same result if the intersection is exact but LC or RC is not `nullptr`
+/// and we can't find the exact differences). Otherwise, the returned location 
+/// is an exact intersection. 
 llvm::Optional<MemoryLocationRange> intersect(
     MemoryLocationRange LHS,
     MemoryLocationRange RHS,
diff --git a/include/tsar/Analysis/Memory/MemorySetInfo.h b/include/tsar/Analysis/Memory/MemorySetInfo.h
index 2b92ba0a..3ffc5ad4 100644
--- a/include/tsar/Analysis/Memory/MemorySetInfo.h
+++ b/include/tsar/Analysis/Memory/MemorySetInfo.h
@@ -26,6 +26,8 @@
 #define TSAR_MEMORY_SET_INFO_H
 
 #include "tsar/Analysis/Memory/MemoryLocationRange.h"
+#include "tsar/Support/SCEVUtils.h"
+#include <llvm/Analysis/ScalarEvolutionExpressions.h>
 
 namespace tsar {
 /// Provide traits for objects stored in a MemorySet.
@@ -230,22 +232,54 @@ template<> struct MemorySetInfo<MemoryLocationRange> {
         sizecmp(getLowerBound(LHS), getUpperBound(RHS)) <= 0;
     }
     std::size_t JoinableDimCount = 0;
+    auto SE = LHS.SE;
+    assert(SE && "ScalarEvolution must be specified!");
     for (std::size_t I = 0; I < LHS.DimList.size(); ++I) {
       auto &Left = LHS.DimList[I];
       auto &Right = RHS.DimList[I];
-      assert(Left.TripCount > 0 && Right.TripCount > 0 &&
-          "Trip count of dimension must be positive!");
       if (Left == Right)
         continue;
-      auto LeftEnd = Left.Start + Left.Step * (Left.TripCount - 1);
-      auto RightEnd = Right.Start + Right.Step * (Right.TripCount - 1);
-      if (Left.Step != Right.Step ||
-          (Left.Start >= Right.Start &&
-              (Left.Start - Right.Start) % Left.Step != 0) ||
-          (Right.Start >= Left.Start &&
-              (Right.Start - Left.Start) % Left.Step != 0) ||
-          (LeftEnd < Right.Start && (Right.Start - LeftEnd) != Left.Step) ||
-          (RightEnd < Left.Start && (Left.Start - RightEnd) != Left.Step))
+      assert(llvm::isa<llvm::SCEVConstant>(Left.Step) &&
+             llvm::isa<llvm::SCEVConstant>(Right.Step) &&
+             "Dimension step must be constant!");
+      if (!llvm::isa<llvm::SCEVConstant>(Left.Start) ||
+          !llvm::isa<llvm::SCEVConstant>(Left.End) ||
+          !llvm::isa<llvm::SCEVConstant>(Right.Start) ||
+          !llvm::isa<llvm::SCEVConstant>(Right.End)) {
+        auto CmpLSRE = compareSCEVs(Left.Start, Right.End, SE);
+        auto CmpRSLE = compareSCEVs(Right.Start, Left.End, SE);
+        if (Left.Step == Right.Step &&
+            llvm::isa<llvm::SCEVConstant>(Left.Step) &&
+            llvm::cast<llvm::SCEVConstant>(Left.Step)->
+                getAPInt().getSExtValue() == 1 &&
+            CmpLSRE && (*CmpLSRE == 0 || *CmpLSRE == 1) ||
+            CmpRSLE && (*CmpRSLE == 0 || *CmpRSLE == 1)) {
+          ++JoinableDimCount;
+          continue;
+        } 
+        return false;
+      }
+      auto LeftStart = llvm::cast<llvm::SCEVConstant>(Left.Start)->
+                       getValue()->getZExtValue();
+      auto LeftEnd = llvm::cast<llvm::SCEVConstant>(Left.End)->
+                     getValue()->getZExtValue();
+      auto LeftStep = llvm::cast<llvm::SCEVConstant>(Left.Step)->
+                      getValue()->getZExtValue();
+      auto RightStart = llvm::cast<llvm::SCEVConstant>(Right.Start)->
+                        getValue()->getZExtValue();
+      auto RightEnd = llvm::cast<llvm::SCEVConstant>(Right.End)->
+                        getValue()->getZExtValue();
+      auto RightStep = llvm::cast<llvm::SCEVConstant>(Right.Step)->
+                       getValue()->getZExtValue();
+      assert(LeftStart <= LeftEnd && RightStart <= RightEnd &&
+          "Start of dimension must be less or equal than End.");
+      if (LeftStep != RightStep ||
+          (LeftStart >= RightStart &&
+              (LeftStart - RightStart) % LeftStep != 0) ||
+          (RightStart >= LeftStart &&
+              (RightStart - LeftStart) % LeftStep != 0) ||
+          (LeftEnd < RightStart && (RightStart - LeftEnd) != LeftStep) ||
+          (RightEnd < LeftStart && (LeftStart - RightEnd) != LeftStep))
         return false;
       ++JoinableDimCount;
     }
@@ -268,18 +302,37 @@ template<> struct MemorySetInfo<MemoryLocationRange> {
         IsChanged = true;
       }
     } else {
+      auto SE = What.SE;
+      assert(SE && "ScalarEvolution must be specified!");
       for (size_t I = 0; I < To.DimList.size(); I++) {
         auto &DimTo = To.DimList[I];
         auto &DimFrom = What.DimList[I];
-        if (DimFrom.Start < DimTo.Start) {
-          DimTo.TripCount += (DimTo.Start - DimFrom.Start) / DimFrom.Step;
+        if (!llvm::isa<llvm::SCEVConstant>(DimTo.Start) ||
+            !llvm::isa<llvm::SCEVConstant>(DimTo.End) ||
+            !llvm::isa<llvm::SCEVConstant>(DimFrom.Start) ||
+            !llvm::isa<llvm::SCEVConstant>(DimFrom.End)) {
+          auto CmpTSFE = compareSCEVs(DimTo.Start, DimFrom.End, SE);
+          auto CmpFSTE = compareSCEVs(DimFrom.Start, DimTo.End, SE);
+          if (CmpTSFE && (*CmpTSFE == 0 || *CmpTSFE == 1)) {
+            DimTo.Start = DimFrom.Start;
+            IsChanged = true;
+          }
+          if (CmpFSTE && (*CmpFSTE == 0 || *CmpFSTE == 1)) {
+            DimTo.End = DimFrom.End;
+            IsChanged = true;
+          }
+          continue;
+        }
+        auto DiffStart = compareSCEVs(DimTo.Start, DimFrom.Start, SE);
+        assert(DiffStart && "Difference must be constant!");
+        if (*DiffStart > 0) {
           DimTo.Start = DimFrom.Start;
           IsChanged = true;
         }
-        auto ToEnd = DimTo.Start + DimTo.Step * (DimTo.TripCount - 1);
-        auto FromEnd = DimFrom.Start + DimFrom.Step * (DimFrom.TripCount - 1);
-        if (FromEnd > ToEnd) {
-          DimTo.TripCount += (FromEnd - ToEnd) / DimFrom.Step;
+        auto DiffEnd = compareSCEVs(DimFrom.End, DimTo.End, SE);
+        assert(DiffEnd && "Difference must be constant!");
+        if (*DiffEnd > 0) {
+          DimTo.End = DimFrom.End;
           IsChanged = true;
         }
       }
diff --git a/include/tsar/Analysis/Memory/Passes.h b/include/tsar/Analysis/Memory/Passes.h
index 1ed2e0d1..063d2831 100644
--- a/include/tsar/Analysis/Memory/Passes.h
+++ b/include/tsar/Analysis/Memory/Passes.h
@@ -234,5 +234,9 @@ ModulePass * createGlobalsAccessCollector();
 // Initialize a pass to access list of explicit accesses to global
 // values in a function.
 void initializeGlobalsAccessWrapperPass(PassRegistry &Registry);
+
+FunctionPass *createAssumptionInfoPass();
+
+void initializeAssumptionInfoPassPass(PassRegistry& Registry);
 }
 #endif//TSAR_MEMORY_ANALYSIS_PASSES_H
diff --git a/include/tsar/Support/SCEVUtils.h b/include/tsar/Support/SCEVUtils.h
index a8c5f4df..ba079bc5 100644
--- a/include/tsar/Support/SCEVUtils.h
+++ b/include/tsar/Support/SCEVUtils.h
@@ -31,6 +31,7 @@
 namespace llvm {
 class ScalarEvolution;
 class SCEV;
+class SCEVAddRecExpr;
 }
 
 namespace tsar {
@@ -74,5 +75,35 @@ const llvm::SCEV* findGCD(llvm::ArrayRef<const llvm::SCEV *> Expressions,
 ///
 /// This function implements Sieve of Atkin with cache.
 std::vector<std::size_t> countPrimeNumbers(std::size_t Bound);
+
+/// If LHS and RHS have the same sequence of type casts, add them and cast 
+/// the result back to the original type.
+const llvm::SCEV *addSCEVAndCast(const llvm::SCEV *LHS,
+                                 const llvm::SCEV *RHS,
+                                 llvm::ScalarEvolution *SE);
+
+/// Add 1 to the expression S.
+const llvm::SCEV *addOneToSCEV(const llvm::SCEV *S, llvm::ScalarEvolution *SE);
+
+/// Subtract 1 from the expression S.
+const llvm::SCEV *subtractOneFromSCEV(const llvm::SCEV *S,
+                                      llvm::ScalarEvolution *SE);
+
+/// If LHS and RHS have the same sequence of type casts, subtract them and cast 
+/// the result back to the original type.
+const llvm::SCEV *subtractSCEVAndCast(const llvm::SCEV *LHS,
+                                      const llvm::SCEV *RHS,
+                                      llvm::ScalarEvolution *SE);
+
+/// Returns the distance between LHS and RHS if it can be calculated.
+llvm::Optional<int64_t> compareSCEVs(const llvm::SCEV *LHS,
+                                     const llvm::SCEV *RHS,
+                                     llvm::ScalarEvolution *SE);
+
+/// Return the value of this chain of recurrences at the specified
+/// iteration number.
+const llvm::SCEV *evaluateAtIteration(const llvm::SCEVAddRecExpr *ARE,
+                                      const llvm::SCEV *It,
+                                      llvm::ScalarEvolution *SE);
 }
 #endif//TSAR_SCEV_UTILS_H
diff --git a/include/tsar/Transform/IR/Passes.h b/include/tsar/Transform/IR/Passes.h
index e59e39c6..ee9db2aa 100644
--- a/include/tsar/Transform/IR/Passes.h
+++ b/include/tsar/Transform/IR/Passes.h
@@ -106,5 +106,13 @@ void initializePointerScalarizerPassPass(PassRegistry &Registry);
 
 /// Create a pass which attempts to promote pointer values to registers.
 FunctionPass *createPointerScalarizerPass();
+
+/// Initialize a pass that replaces the always true conditional branch
+/// instructions with an unconditional branch instruction.
+void initializeRedundantEdgeEliminationPassPass(PassRegistry &Registry);
+
+/// Create a pass that replaces the always true conditional branch
+/// instructions with an unconditional branch instruction.
+FunctionPass *createRedundantEdgeEliminationPass();
 }
 #endif//TSAR_IR_TRANSFORM_PASSES_H
diff --git a/lib/Analysis/Memory/AssumptionInfo.cpp b/lib/Analysis/Memory/AssumptionInfo.cpp
new file mode 100644
index 00000000..727ff46b
--- /dev/null
+++ b/lib/Analysis/Memory/AssumptionInfo.cpp
@@ -0,0 +1,153 @@
+//===- AssumptionInfo.cpp --- Assumption Information ------------*- C++ -*-===//
+//
+//                     Traits Static Analyzer (SAPFOR)
+//
+// Copyright 2022 DVM System Group
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+//
+//===----------------------------------------------------------------------===//
+//
+// This file provides assumption information for memory locations with variable
+// bounds.
+//
+//===----------------------------------------------------------------------===/
+
+#include "tsar/Analysis/Memory/AssumptionInfo.h"
+#include "tsar/Core/Query.h"
+#include <llvm/Analysis/AssumptionCache.h>
+#include <llvm/Analysis/ScalarEvolution.h>
+#include <llvm/Analysis/ScalarEvolutionExpressions.h>
+#include <llvm/InitializePasses.h>
+
+using namespace llvm;
+using namespace tsar;
+
+#undef DEBUG_TYPE
+#define DEBUG_TYPE "assumption-info"
+
+char AssumptionInfoPass::ID = 0;
+INITIALIZE_PASS_IN_GROUP_BEGIN(AssumptionInfoPass, "assumption-info",
+  "Assumption information extractor", false, true,
+  DefaultQueryManager::PrintPassGroup::getPassRegistry())
+INITIALIZE_PASS_DEPENDENCY(AssumptionCacheTracker)
+INITIALIZE_PASS_IN_GROUP_END(AssumptionInfoPass, "assumption-info",
+  "Assumption information extractor", false, true,
+  DefaultQueryManager::PrintPassGroup::getPassRegistry())
+
+namespace {
+/// Fills AssumptionMap AM with information extracted from AssumptionCache AC.
+/// AssumptionMap maps llvm::Value* to AssumptionBounds - a pair of two optional
+/// integers: Lower and Upper. AC stores expressions collected from arguments of
+/// the intrinsic `__builtin_assume'. Consider the following example:
+///
+/// __builtin_assume(x > 0);
+/// __builtin_assume(x <= 100);
+///
+/// For the llvm::Value *V corresponding to variable X, the following
+/// AssumptionBounds will be set: Lower = 1, Upper = 100. In essence,
+/// AssumptionBounds is a segment that symbolizes the set of values ​​that X
+/// can take. If Lower or Upper are not set, it is considered that the
+/// corresponding segment boundary becomes equal to infinity. If several values
+/// are defined for the lower boundary of the segment, the maximum is selected
+/// from them. For the upper bound, the minimum is similarly selected.
+void initializeAssumptions(AssumptionMap &AM, AssumptionCache &AC) {
+  auto UpdateBound = [](ConstantInt *C, Value *V, CmpInst::Predicate Pred,
+                        AssumptionBounds &Bounds) {
+    auto CV = C->getSExtValue();
+    switch (Pred)
+    {
+    case CmpInst::Predicate::ICMP_UGE:
+    case CmpInst::Predicate::ICMP_SGE:
+      Bounds.Upper = Bounds.Upper ? std::min(CV, *Bounds.Upper) : CV;
+      break;
+    case CmpInst::Predicate::ICMP_UGT:
+    case CmpInst::Predicate::ICMP_SGT:
+      Bounds.Upper = Bounds.Upper ? std::min(CV - 1, *Bounds.Upper) :
+                                             CV - 1;
+      break;
+    case CmpInst::Predicate::ICMP_ULE:
+    case CmpInst::Predicate::ICMP_SLE:
+      Bounds.Lower = Bounds.Lower ? std::max(CV, *Bounds.Lower) : CV;
+      break;
+    case CmpInst::Predicate::ICMP_ULT:
+    case CmpInst::Predicate::ICMP_SLT:
+      Bounds.Lower = Bounds.Lower ? std::max(CV + 1, *Bounds.Lower) :
+                                             CV + 1;
+      break;
+    default:
+      llvm_unreachable("Predicate must be relational!");
+    }
+  };
+  for (auto &AssumeVH : AC.assumptions()) {
+    if (!AssumeVH)
+      continue;
+    if (auto *I = dyn_cast<CallInst>(AssumeVH.Assume)) {
+      auto *CI = dyn_cast<CmpInst>(I->getArgOperand(0));
+      if (CI && CI->isIntPredicate() && CI->isRelational()) {
+        assert(CI->getNumOperands() == 2 &&
+            "Number of operands for CmpInst must be 2!");
+        auto *Op0 = CI->getOperand(0);
+        auto *Op1 = CI->getOperand(1);
+        auto *C0 = dyn_cast<ConstantInt>(Op0);
+        auto *C1 = dyn_cast<ConstantInt>(Op1);
+        if (C0 && !C1) {
+          auto &Bounds = AM.insert(
+              std::make_pair(Op1, AssumptionBounds())).
+              first->second;
+          UpdateBound(C0, Op1, CI->getPredicate(), Bounds);
+        } else if (!C0 && C1) {
+          auto &Bounds = AM.insert(
+              std::make_pair(Op0, AssumptionBounds())).
+              first->second;
+          UpdateBound(C1, Op0, CI->getSwappedPredicate(), Bounds);
+        }
+      }
+    }
+  }
+  LLVM_DEBUG(
+    dbgs() << "[ASSUME] Bounds: ";
+    for (auto &Pair : AM) {
+      dbgs() << "<";
+      Pair.first->print(dbgs(), true);
+      dbgs() << ", [" << Pair.second.Lower << ", " << Pair.second.Upper << "]> ";
+    }
+    dbgs() << "\n";
+  );
+}
+
+#ifdef LLVM_DEBUG
+void dumpAssumptions(llvm::AssumptionCache &AC, llvm::Value *For=nullptr) {
+  dbgs() << "[ASSUME] AssumptionCache: ";
+  auto AL = For ? AC.assumptionsFor(For) : AC.assumptions();
+  for (auto &AssumeVH : AL) {
+    if (!AssumeVH)
+      continue;
+    AssumeVH.Assume->dump();
+  }
+}
+#endif
+}
+
+bool AssumptionInfoPass::runOnFunction(Function &F) {
+  releaseMemory();
+  auto &AC = getAnalysis<AssumptionCacheTracker>().getAssumptionCache(F);
+  LLVM_DEBUG(dumpAssumptions(AC));
+  initializeAssumptions(mAM, AC);
+  return false;
+}
+
+void AssumptionInfoPass::getAnalysisUsage(AnalysisUsage &AU) const {
+  AU.addRequired<AssumptionCacheTracker>();
+  AU.setPreservesAll();
+}
diff --git a/lib/Analysis/Memory/CMakeLists.txt b/lib/Analysis/Memory/CMakeLists.txt
index 9361a9b4..8cf946d2 100644
--- a/lib/Analysis/Memory/CMakeLists.txt
+++ b/lib/Analysis/Memory/CMakeLists.txt
@@ -6,7 +6,7 @@ set(ANALYSIS_SOURCES Passes.cpp DependenceAnalysis.cpp PrivateAnalysis.cpp
   Delinearization.cpp ServerUtils.cpp ClonedDIMemoryMatcher.cpp
   GlobalLiveMemory.cpp GlobalDefinedMemory.cpp DIClientServerInfo.cpp
   DIMemoryAnalysisServer.cpp DIArrayAccess.cpp AllocasModRef.cpp
-  MemoryLocationRange.cpp GlobalsAccess.cpp)
+  MemoryLocationRange.cpp GlobalsAccess.cpp AssumptionInfo.cpp)
 
 if(MSVC_IDE)
   file(GLOB_RECURSE ANALYSIS_HEADERS RELATIVE ${CMAKE_CURRENT_SOURCE_DIR}
diff --git a/lib/Analysis/Memory/DefinedMemory.cpp b/lib/Analysis/Memory/DefinedMemory.cpp
index 510c352e..44222665 100644
--- a/lib/Analysis/Memory/DefinedMemory.cpp
+++ b/lib/Analysis/Memory/DefinedMemory.cpp
@@ -22,6 +22,7 @@
 //
 //===----------------------------------------------------------------------===//
 
+#include "tsar/Analysis/Memory/AssumptionInfo.h"
 #include "tsar/Analysis/Memory/DefinedMemory.h"
 #include "tsar/Analysis/DFRegionInfo.h"
 #include "tsar/Analysis/Memory/Delinearization.h"
@@ -46,6 +47,7 @@
 #include <llvm/IR/Function.h>
 #include <llvm/IR/Instructions.h>
 #include <llvm/IR/InstIterator.h>
+#include <llvm/IR/Operator.h>
 #include <llvm/Support/Debug.h>
 #include <functional>
 
@@ -66,6 +68,7 @@ INITIALIZE_PASS_BEGIN(DefinedMemoryPass, "def-mem",
   INITIALIZE_PASS_DEPENDENCY(DelinearizationPass)
   INITIALIZE_PASS_DEPENDENCY(ScalarEvolutionWrapperPass)
   INITIALIZE_PASS_DEPENDENCY(GlobalOptionsImmutableWrapper)
+  INITIALIZE_PASS_DEPENDENCY(AssumptionInfoPass)
 INITIALIZE_PASS_END(DefinedMemoryPass, "def-mem",
   "Defined Memory Region Analysis", false, true)
 
@@ -80,12 +83,13 @@ bool llvm::DefinedMemoryPass::runOnFunction(Function & F) {
   auto &DL = F.getParent()->getDataLayout();
   auto &GO = getAnalysis<GlobalOptionsImmutableWrapper>().getOptions();
   auto &GDM = getAnalysis<GlobalDefinedMemoryWrapper>();
+  auto &AM = getAnalysis<AssumptionInfoPass>().getAssumptionMap();
   if (GDM) {
-    ReachDFFwk ReachDefFwk(AliasTree, TLI, RegionInfo, DT, DI, SE, DL, GO,
+    ReachDFFwk ReachDefFwk(AliasTree, TLI, RegionInfo, DT, DI, SE, DL, AM, GO,
                            mDefInfo, *GDM);
     solveDataFlowUpward(&ReachDefFwk, DFF);
   } else {
-    ReachDFFwk ReachDefFwk(AliasTree, TLI, RegionInfo, DT, DI, SE, DL, GO,
+    ReachDFFwk ReachDefFwk(AliasTree, TLI, RegionInfo, DT, DI, SE, DL, AM, GO,
                            mDefInfo);
     solveDataFlowUpward(&ReachDefFwk, DFF);
   }
@@ -101,6 +105,7 @@ void DefinedMemoryPass::getAnalysisUsage(AnalysisUsage & AU) const {
   AU.addRequired<DelinearizationPass>();
   AU.addRequired<ScalarEvolutionWrapperPass>();
   AU.addRequired<GlobalOptionsImmutableWrapper>();
+  AU.addRequired<AssumptionInfoPass>();
   AU.setPreservesAll();
 }
 
@@ -242,27 +247,37 @@ class AddUnknownAccessFunctor :
 /// single array access within the basic block, this is used in
 /// `DataFlowTraits<ReachDFFwk*>::initialize()`.
 ///
+/// If `N == nullptr`, this means that we want to check some explicitly 
+/// accessed location to be collapsed later and we may ignore restrictions
+/// associated with a region matching.
+///
 /// Return a pair consisting of an aggregated memory location and boolean value.
 /// If returned location is of kind `Collapsed` and does not belong to the
 /// loop nest associated with region `R`, this value will be set to `false`,
 /// `true` otherwise.
 std::pair<MemoryLocationRange, bool> aggregate(
-    DFRegion *R, const MemoryLocationRange &Loc, const ReachDFFwk *Fwk) {
+    const DFRegion *R, const DFNode *N, const MemoryLocationRange &Loc,
+    const ReachDFFwk *Fwk) {
   typedef MemoryLocationRange::Dimension Dimension;
   typedef MemoryLocationRange::LocKind LocKind;
+  typedef ICmpInst::Predicate Predicate;
   assert(Fwk && "Data-flow framework must not be null");
   assert(!(Loc.Kind & LocKind::Collapsed) || Loc.DimList.size() > 0 &&
       "Collapsed array location must not be empty!");
-  // We will try to aggregate location if it is of kind `Default` only.
-  if (Loc.Kind != LocKind::Default)
+  // We will try to aggregate location if it is of kind `Default` or 
+  // `Auxiliary Default` only.
+  if ((Loc.Kind & ~LocKind::Auxiliary) != LocKind::Default)
     return std::make_pair(Loc, true);
   MemoryLocationRange ResLoc(Loc);
+  auto *SE = Fwk->getScalarEvolution();
+  assert(SE && "ScalarEvolution must be specified!");
+  ResLoc.SE = SE;
+  ResLoc.AM = Fwk->getAssumptionMap();
   auto LocInfo = Fwk->getDelinearizeInfo()->findRange(Loc.Ptr);
   auto ArrayPtr = LocInfo.first;
   if (!ArrayPtr || !ArrayPtr->isDelinearized() || !LocInfo.second->isValid()) {
     LLVM_DEBUG(dbgs() << "[AGGREGATE] Failed to delinearize location.\n");
-    ResLoc.Kind = LocKind::Default;
-    return std::make_pair(ResLoc, true);
+    return std::make_pair(Loc, true);
   }
   LLVM_DEBUG(dbgs() << "[AGGREGATE] Array info: " << *ArrayPtr->getBase() <<
       ", IsAddress: " << ArrayPtr->isAddressOfVariable() << ".\n");
@@ -277,29 +292,76 @@ std::pair<MemoryLocationRange, bool> aggregate(
   auto ArraySizeInfo = arraySize(ArrayType);
   if (ArraySizeInfo == std::make_tuple(0, 1, ArrayType) &&
       ArrayPtr->getNumberOfDims() != 1) {
-    LLVM_DEBUG(dbgs() << "[AGGREGATE] Failed to get array size.\n");
     ResLoc.Kind = LocKind::NonCollapsable;
     return std::make_pair(ResLoc, true);
   }
   auto ElemType = std::get<2>(ArraySizeInfo);
   LLVM_DEBUG(dbgs() << "[AGGREGATE] Array element type:  " <<
       *ElemType << ".\n");
+  auto Int64Ty = Type::getInt64Ty(SE->getContext());
+  auto ElemSize = Fwk->getDataLayout().getTypeStoreSize(ElemType).
+      getFixedSize();
+  int64_t Offset;
+  auto *BasePtr = GetPointerBaseWithConstantOffset(
+      Loc.Ptr, Offset, Fwk->getDataLayout());
+  auto *GV{dyn_cast<GlobalValue>(getUnderlyingObject(Loc.Ptr, 0))};
   if (Fwk->getDataLayout().getTypeStoreSize(ElemType).isScalable() ||
       LocInfo.second->Subscripts.size() != ArrayPtr->getNumberOfDims() ||
       !Loc.LowerBound.hasValue() || !Loc.UpperBound.hasValue() ||
       Loc.LowerBound.getValue() != 0 ||
-      Loc.UpperBound.getValue() != Fwk->getDataLayout().
-                                   getTypeStoreSize(ElemType).getFixedSize()) {
+      Loc.UpperBound.getValue() != ElemSize) {
+    // Consider the following example:
+    //
+    // int A[13];
+    // void f() {
+    //   for (...) {
+    //     A[0] = ...; // S
+    //     ...
+    //   }
+    // }
+    //
+    // Statement S produces such non-collapsable memory location: <A[0], 0, 52>.
+    // If there are collapsed memory locations of A for the loop, we won't be
+    // able to take into account this non-collapsable location correctly. So
+    // we should collapse such location manually.
+    //
+    // TODO (yukki.lapenko@gmail.com): consider multidimensional arrays
+    if (ArrayPtr->getNumberOfDims() == 1 &&
+        Loc.LowerBound.hasValue() &&
+        Loc.LowerBound.getValue() % ElemSize == 0 &&
+        Loc.UpperBound.hasValue() &&
+        Loc.UpperBound.getValue() % ElemSize == 0) {
+      if (BasePtr == GV && Offset == 0) {
+        ResLoc.Ptr = BasePtr;
+        ResLoc.LowerBound = 0;
+        ResLoc.UpperBound = ElemSize;
+        Dimension DimInfo;
+        DimInfo.Start = SE->getConstant(
+            Int64Ty, Loc.LowerBound.getValue() / ElemSize);
+        DimInfo.End = SE->getConstant(Int64Ty,
+            Loc.UpperBound.getValue() / ElemSize - 1);
+        DimInfo.Step = SE->getConstant(Int64Ty, 1);
+        auto ResLocInfo = Fwk->getDelinearizeInfo()->findRange(BasePtr);
+        auto ResArrayPtr = ResLocInfo.first;
+        DimInfo.DimSize = 0;
+        if (ResArrayPtr && ResArrayPtr->isDelinearized() &&
+            ResLocInfo.second->isValid()) {
+          if (auto *C = dyn_cast<SCEVConstant>(ResArrayPtr->getDimSize(0)))
+            DimInfo.DimSize = C->getAPInt().getZExtValue();
+        }
+        ResLoc.DimList.clear();
+        ResLoc.DimList.push_back(DimInfo);
+        ResLoc.Kind = LocKind::Collapsed | Loc.Kind & LocKind::Auxiliary;
+        return std::make_pair(ResLoc, true);
+      }
+    }
     ResLoc.Kind = LocKind::NonCollapsable;
     return std::make_pair(ResLoc, true);
   }
   ResLoc.Ptr = ArrayPtr->getBase();
   ResLoc.LowerBound = 0;
-  ResLoc.UpperBound = Fwk->getDataLayout().getTypeStoreSize(ElemType).
-      getFixedSize();
+  ResLoc.UpperBound = ElemSize;
   ResLoc.Kind = LocKind::Collapsed;
-  auto *SE = Fwk->getScalarEvolution();
-  assert(SE && "ScalarEvolution must be specified!");
   std::size_t DimensionN = 0;
   std::size_t LoopMatchCount = 0, ConstMatchCount = 0;
   for (auto *S : LocInfo.second->Subscripts) {
@@ -327,53 +389,171 @@ std::pair<MemoryLocationRange, bool> aggregate(
       if (C->getAPInt().isNegative())
         break;
       ++ConstMatchCount;
-      DimInfo.Start = C->getAPInt().getSExtValue();
-      DimInfo.TripCount = 1;
-      DimInfo.Step = 1;
+      DimInfo.Start = DimInfo.End = SE->getConstant(C->getAPInt());
+      DimInfo.Step = SE->getOne(C->getType());
       ResLoc.DimList.push_back(DimInfo);
       ResLoc.Kind = LocKind::Collapsed;
     } else if (auto C = dyn_cast<SCEVAddRecExpr>(SCEV)) {
-      if (!R) {
+      if (!R && N) {
         LLVM_DEBUG(dbgs() << "[AGGREGATE] Region == nullptr.\n");
         ResLoc.Kind = LocKind::Default;
         break;
       }
-      if (auto *DFL = dyn_cast<DFLoop>(R)) {
-        assert(DFL->getLoop() && C->getLoop() &&
-            "Loops for the DFLoop and AddRecExpr must be specified!");
-        if (DFL->getLoop()->contains(C->getLoop()))
-          ++LoopMatchCount;
+      if (N) {
+        if (auto *DFL = dyn_cast<DFLoop>(R)) {
+          assert(DFL->getLoop() && C->getLoop() &&
+              "Loops for the DFLoop and AddRecExpr must be specified!");
+          if (DFL->getLoop()->contains(C->getLoop()))
+            ++LoopMatchCount;
+        }
       }
       auto *StepSCEV = C->getStepRecurrence(*SE);
       if (!isa<SCEVConstant>(StepSCEV)) {
         LLVM_DEBUG(dbgs() << "[AGGREGATE] Non-constant step.\n");
         break;
       }
-      auto TripCount = SE->getSmallConstantTripCount(C->getLoop());
-      if (TripCount <= 1) {
-        LLVM_DEBUG(dbgs() << "[AGGREGATE] Unknown or non-constant "
-                             "trip count.\n");
+      auto AddRecStep = cast<SCEVConstant>(StepSCEV)->getAPInt().getSExtValue();
+      if (!C->getLoop()->getExitingBlock() || !C->getLoop()->getLoopLatch()) {
+        LLVM_DEBUG(dbgs() << "[AGGREGATE] Multiple exiting and latch blocks "
+                              "are prohibited.\n");
         break;
       }
-      int64_t SignedRangeMin = SE->getSignedRangeMin(SCEV).getSExtValue();
-      if (SignedRangeMin < 0) {
-        LLVM_DEBUG(dbgs() << "[AGGREGATE] Range bounds must be "
-                              "non-negative.\n");
-        break;
+      unsigned int TripCount = 0;
+      if (C->getLoop()->getLoopLatch() == C->getLoop()->getExitingBlock()) {
+        LLVM_DEBUG(dbgs() << "[AGGREGATE] Node kind: Latch and Exiting.\n"); 
+        TripCount = SE->getSmallConstantTripCount(C->getLoop());
+      } else {
+        LLVM_DEBUG(dbgs() << "[AGGREGATE] Node kind: Latch or Exiting.\n");
+        if (N) {
+          auto *DFB = dyn_cast<DFBlock>(N);
+          if (DFB && DFB->getBlock() == C->getLoop()->getExitingBlock()) {
+            TripCount = SE->getSmallConstantTripCount(C->getLoop());
+          } else if ((DFB && DFB->getBlock() == C->getLoop()->getLoopLatch()) ||
+                     C->getLoop()->getHeader() == C->getLoop()->getExitingBlock()){
+            if (auto BTC = dyn_cast<SCEVConstant>(
+                SE->getBackedgeTakenCount(C->getLoop())))
+              TripCount = BTC->getAPInt().getZExtValue();
+          } else {
+            break;
+          }
+        } else {
+          // This case means that we want to check some explicitly accessed
+          // location to be collapsed later. For this reason we only need to
+          // know that the number of iterations is greater than 0, the exact
+          // trip count doesn't matter.
+          TripCount = 42;
+        }
       }
-      DimInfo.Start = SignedRangeMin;
-      DimInfo.TripCount = TripCount - 1;
-      DimInfo.Step = std::abs(cast<SCEVConstant>(StepSCEV)->
-                              getAPInt().getSExtValue());
-      if (DimInfo.Start + DimInfo.Step * (DimInfo.TripCount - 1) >=
-          DimInfo.DimSize && DimensionN != 0) {
-        LLVM_DEBUG(dbgs() << "[AGGREGATE] Array index out of bounds.");
+      if (TripCount > 0) {
+        LLVM_DEBUG(dbgs() << "[AGGREGATE] Aggregate a constant range.\n");
+        int64_t SignedRangeMin = SE->getSignedRangeMin(SCEV).getSExtValue();
+        if (SignedRangeMin < 0) {
+          LLVM_DEBUG(dbgs() << "[AGGREGATE] Range bounds must be "
+                                "non-negative.\n");
+          break;
+        }
+        DimInfo.Start = SE->getConstant(SCEV->getType(), SignedRangeMin);
+        DimInfo.End = SE->getConstant(SCEV->getType(),
+            SignedRangeMin + std::abs(AddRecStep) * (TripCount - 1));
+      } else {
+        if (std::abs(AddRecStep) != 1)
+          break;
+        auto Bounds = C->getLoop()->getBounds(*SE);
+        if (!Bounds) {
+          LLVM_DEBUG(dbgs() << "[AGGREGATE] Failed to get loop bounds.\n");
+          break;
+        }
+        auto *InitValue = &Bounds->getInitialIVValue();
+        auto *FinalValue = &Bounds->getFinalIVValue();
+        if (!SE->isSCEVable(InitValue->getType()) ||
+            !SE->isSCEVable(FinalValue->getType())) {
+          LLVM_DEBUG(dbgs() << "[AGGREGATE] Loop bound is not SCEVable.\n");
+          break;
+        }
+        if (!InitValue->getType()->isIntegerTy() ||
+            !FinalValue->getType()->isIntegerTy()) {
+          LLVM_DEBUG(dbgs() << "[AGGREGATE] Non-integer loop bound.\n");
+          break;
+        }
+        auto Predicate = Bounds->getCanonicalPredicate();
+        if (!ICmpInst::isRelational(Predicate)) {
+          LLVM_DEBUG(dbgs() << "[AGGREGATE] Bad predicate.\n");
+          break;
+        }
+        if (Bounds->getDirection() == Loop::LoopBounds::Direction::Unknown) {
+          LLVM_DEBUG(dbgs() << "[AGGREGATE] Unknown direction.\n");
+          break;
+        }
+        auto LoopStep = cast<SCEVConstant>(
+            SE->getSCEV(Bounds->getStepValue()))->getAPInt().getSExtValue();
+        auto InitSCEV = SE->getSCEV(InitValue);
+        auto FinalSCEV = SE->getSCEV(FinalValue);
+        if (Bounds->getDirection() == Loop::LoopBounds::Direction::Increasing &&
+           (ICmpInst::isGT(Predicate) || ICmpInst::isGE(Predicate)) ||
+            Bounds->getDirection() == Loop::LoopBounds::Direction::Decreasing &&
+           (ICmpInst::isLT(Predicate) || ICmpInst::isLE(Predicate))) {
+          LLVM_DEBUG(dbgs() << "[AGGREGATE] Unpredictable predicate.\n");
+          break;
+        }
+        if (Bounds->getDirection() == Loop::LoopBounds::Direction::Increasing) {
+          if (ICmpInst::isLT(Predicate))
+            FinalSCEV = subtractSCEVAndCast(FinalSCEV,
+                                            SE->getOne(FinalSCEV->getType()),
+                                            SE);
+        } else {
+          if (ICmpInst::isGT(Predicate))
+            FinalSCEV = addSCEVAndCast(SE->getOne(FinalSCEV->getType()),
+                                       FinalSCEV, SE);
+        }
+        LLVM_DEBUG(dbgs() << "[AGGREGATE] AddRecType: "; C->getType()->dump());
+        auto ZeroItr = evaluateAtIteration(C, SE->getZero(C->getType()), SE);
+        auto IdxExprStep = AddRecStep / LoopStep;
+        LLVM_DEBUG(dbgs() << "[AGGREGATE] LoopStep: " << LoopStep <<
+            ", IdxExprStep: " << IdxExprStep << "\n");
+        if (LoopStep > 0 && IdxExprStep > 0) {
+          DimInfo.Start = ZeroItr;
+          DimInfo.End = evaluateAtIteration(C,
+              subtractSCEVAndCast(FinalSCEV, InitSCEV, SE), SE);
+        } else if (LoopStep > 0 && IdxExprStep < 0) {
+          DimInfo.Start = evaluateAtIteration(C,
+              subtractSCEVAndCast(FinalSCEV, InitSCEV, SE), SE);
+          DimInfo.End = ZeroItr;
+        } else if (LoopStep < 0 && IdxExprStep > 0) {
+          DimInfo.Start = evaluateAtIteration(C,
+              subtractSCEVAndCast(InitSCEV, FinalSCEV, SE), SE);
+          DimInfo.End = ZeroItr;
+        } else {
+          DimInfo.Start = ZeroItr;
+          DimInfo.End = evaluateAtIteration(C,
+              subtractSCEVAndCast(InitSCEV, FinalSCEV, SE), SE);
+        }
+        auto CmpStartEnd = compareSCEVs(DimInfo.Start, DimInfo.End, SE);
+        if (CmpStartEnd && *CmpStartEnd > 0) {
+          LLVM_DEBUG(dbgs() << "[AGGREGATE] Incorrect bounds.\n");
+          break;
+        }
+      }
+      DimInfo.Step = SE->getConstant(C->getStepRecurrence(*SE)->getType(),
+                                     std::abs(AddRecStep));
+      assert(DimInfo.Start && DimInfo.End && DimInfo.Step &&
+          "Dimension bounds and step must be specified!");
+      if (isa<SCEVConstant>(DimInfo.End) &&
+          cast<SCEVConstant>(DimInfo.End)->getAPInt().
+            getSExtValue() >= DimInfo.DimSize && DimensionN != 0 && N != nullptr) {
+        auto End = cast<SCEVConstant>(DimInfo.End)->getAPInt().
+            getSExtValue();
+        LLVM_DEBUG(dbgs() << "[AGGREGATE] Array index out of bounds. End = " <<
+            End << ", DimSize = " << DimInfo.DimSize << "\n");
         break;
       }
       ResLoc.DimList.push_back(DimInfo);
       ResLoc.Kind = LocKind::Collapsed;
     } else {
-      break;
+      DimInfo.Start = DimInfo.End = SCEV;
+      DimInfo.Step = SE->getOne(Int64Ty);
+      ResLoc.DimList.push_back(DimInfo);
+      ResLoc.Kind = LocKind::Collapsed;
+      ++ConstMatchCount;
     }
     ++DimensionN;
   }
@@ -387,7 +567,7 @@ std::pair<MemoryLocationRange, bool> aggregate(
     return std::make_pair(NewLoc, true);
   }
   bool IsOwn = true;
-  if (isa_and_nonnull<DFLoop>(R)) {
+  if (isa_and_nonnull<DFLoop>(R) && N) {
     if (LoopMatchCount == 0 && ConstMatchCount != ArrayPtr->getNumberOfDims()) {
       IsOwn = false;
     } else if (LoopMatchCount > 0 &&
@@ -395,6 +575,9 @@ std::pair<MemoryLocationRange, bool> aggregate(
       return std::make_pair(Loc, true);
     }
   }
+  // For collapsable locations like <A[0], 0, 4>
+  if (BasePtr == GV && Offset == 0)
+    ResLoc.Ptr = BasePtr;
   assert(ResLoc.Kind == LocKind::Collapsed &&
       "Array location must be of the `collapsed` kind!");
   LLVM_DEBUG(
@@ -402,6 +585,7 @@ std::pair<MemoryLocationRange, bool> aggregate(
     printLocationSource(dbgs(), ResLoc, &Fwk->getDomTree(), true);
     dbgs() << "\n";
   );
+  ResLoc.Kind |= Loc.Kind & LocKind::Auxiliary;
   return std::make_pair(ResLoc, IsOwn);
 }
 
@@ -415,8 +599,9 @@ class AddKnownAccessFunctor :
 public:
   AddKnownAccessFunctor(AAResults &AA, const DataLayout &DL,
       const DFRegionInfo &DFI, const DominatorTree &DT, const Instruction &Inst,
-      const MemoryLocation &Loc, DefUseSet &DU, ReachDFFwk *DFF) :
-    Base(AA, DL, DFI, DT, Inst, DU),  mLoc(Loc), DFF(DFF) {}
+      const MemoryLocation &Loc, const EstimateMemory *EM, DefUseSet &DU,
+      ReachDFFwk *DFF, DFNode *N) :
+    Base(AA, DL, DFI, DT, Inst, DU), mLoc(Loc), mEM(EM), mDFF(DFF), mDFN(N) {}
 
   void addEstimate(AliasEstimateNode &N) {
     for (auto &EM : N) {
@@ -432,7 +617,10 @@ class AddKnownAccessFunctor :
           continue;
         auto AR = aliasRelation(this->mAA, this->mDL, mLoc, ALoc);
         if (AR.template is_any<trait::CoverAlias, trait::CoincideAlias>()) {
-          addMust(ALoc);
+          MemoryLocationRange Loc(ALoc);
+          if (mEM->isDescendantOf(EM) && mEM != &EM)
+            Loc.Kind |= MemoryLocationRange::LocKind::Auxiliary;
+          addMust(Loc);
         } else if (AR.template is<trait::ContainedAlias>()) {
           int64_t OffsetLoc, OffsetALoc;
           auto BaseLoc{
@@ -459,11 +647,16 @@ class AddKnownAccessFunctor :
           } else {
             Range = MemoryLocationRange{ALoc.Ptr, 0, mLoc.Size , ALoc.AATags};
           }
+          if (mEM->isDescendantOf(EM) && mEM != &EM)
+            Range.Kind |= MemoryLocationRange::LocKind::Auxiliary;
           if (this->mDU.hasDef(Range))
             continue;
           addMust(Range);
         } else if (!AR.template is<trait::NoAlias>()) {
-          addMay(ALoc);
+          MemoryLocationRange Loc(ALoc);
+          if (mEM->isDescendantOf(EM) && mEM != &EM)
+            Loc.Kind |= MemoryLocationRange::LocKind::Auxiliary;
+          addMay(Loc);
         }
       }
     }
@@ -471,27 +664,32 @@ class AddKnownAccessFunctor :
 
 private:
   void addMust(const MemoryLocationRange &Loc) {
-    static_cast<ImpTy *>(this)->addMust(aggregate(nullptr, Loc, DFF).first);
+    static_cast<ImpTy *>(this)->addMust(aggregate(
+        nullptr, mDFN, Loc, mDFF).first);
     static_cast<ImpTy *>(this)->addMust(Loc);
   }
 
   void addMay(const MemoryLocationRange &Loc) {
-    static_cast<ImpTy *>(this)->addMay(aggregate(nullptr, Loc, DFF).first);
+    static_cast<ImpTy *>(this)->addMay(aggregate(
+        nullptr, mDFN, Loc, mDFF).first);
     static_cast<ImpTy *>(this)->addMay(Loc);
   }
 
   const MemoryLocation &mLoc;
-  ReachDFFwk *DFF;
+  const EstimateMemory *mEM;
+  ReachDFFwk *mDFF;
+  DFNode *mDFN;
 };
 
 /// This macro determine functors according to a specified memory access modes.
-#define ADD_ACCESS_FUNCTOR(NAME, BASE, MEM, MAY, MUST, DFF) \
+#define ADD_ACCESS_FUNCTOR(NAME, BASE, MEM, MAY, MUST, DFF, N) \
 class NAME : public BASE<NAME> { \
 public: \
   NAME(AAResults &AA, const DataLayout &DL, const DFRegionInfo &DFI, \
       const DominatorTree &DT, const Instruction &Inst, \
-      MEM &Loc, DefUseSet &DU, ReachDFFwk *DFF) : \
-    BASE<NAME>(AA, DL, DFI, DT, Inst, Loc, DU, DFF) {} \
+      MEM &Loc, const EstimateMemory *EM, DefUseSet &DU, ReachDFFwk *DFF, \
+      DFNode *N) : \
+    BASE<NAME>(AA, DL, DFI, DT, Inst, Loc, EM, DU, DFF, N) {} \
 private: \
   friend BASE<NAME>; \
   void addMust(const MemoryLocationRange &Loc) { MUST; } \
@@ -499,17 +697,18 @@ private: \
 };
 
 ADD_ACCESS_FUNCTOR(AddDefFunctor, AddKnownAccessFunctor,
-  const MemoryLocation, mDU.addMayDef(Loc), mDU.addDef(Loc), DFF)
+  const MemoryLocation, mDU.addMayDef(Loc), mDU.addDef(Loc), DFF, N)
 ADD_ACCESS_FUNCTOR(AddMayDefFunctor, AddKnownAccessFunctor,
-  const MemoryLocation, mDU.addMayDef(Loc), mDU.addMayDef(Loc), DFF)
+  const MemoryLocation, mDU.addMayDef(Loc), mDU.addMayDef(Loc), DFF, N)
 ADD_ACCESS_FUNCTOR(AddUseFunctor, AddKnownAccessFunctor,
-  const MemoryLocation, mDU.addUse(Loc), mDU.addUse(Loc), DFF)
+  const MemoryLocation, mDU.addUse(Loc), mDU.addUse(Loc), DFF, N)
 ADD_ACCESS_FUNCTOR(AddDefUseFunctor, AddKnownAccessFunctor,
   const MemoryLocation,
-  mDU.addMayDef(Loc); mDU.addUse(Loc), mDU.addDef(Loc); mDU.addUse(Loc), DFF)
+  mDU.addMayDef(Loc); mDU.addUse(Loc), mDU.addDef(Loc); mDU.addUse(Loc), DFF, N)
 ADD_ACCESS_FUNCTOR(AddMayDefUseFunctor, AddKnownAccessFunctor,
   const MemoryLocation,
-  mDU.addMayDef(Loc); mDU.addUse(Loc), mDU.addMayDef(Loc); mDU.addUse(Loc), DFF)
+  mDU.addMayDef(Loc); mDU.addUse(Loc), mDU.addMayDef(Loc); mDU.addUse(Loc), DFF,
+      N)
 
 #ifndef NDEBUG
 void intializeDefUseSetLog(
@@ -605,8 +804,19 @@ void DataFlowTraits<ReachDFFwk*>::initialize(
       if (isMemoryMarkerIntrinsic(II->getIntrinsicID()) ||
           isDbgInfoIntrinsic(II->getIntrinsicID()))
         continue;
-    if (I.getType() && I.getType()->isPointerTy())
-      DU->addAddressAccess(&I);
+    if (I.getType() && I.getType()->isPointerTy()) {
+      if (isa<GEPOperator>(I)) {
+        auto IsOnlyGEPUsers{true};
+        for_each_user_insts(I,
+                            [&IsOnlyGEPUsers](auto *U) {
+                              IsOnlyGEPUsers &= isa<GEPOperator>(U);
+                            });
+        if (!IsOnlyGEPUsers)
+          DU->addAddressAccess(&I);
+      } else {
+        DU->addAddressAccess(&I);
+      }
+    }
     auto isAddressAccess = [&F](const Value *V) {
       if (const ConstantPointerNull *CPN = dyn_cast<ConstantPointerNull>(V)) {
         if (!NullPointerIsDefined(F, CPN->getType()->getAddressSpace()))
@@ -621,6 +831,13 @@ void DataFlowTraits<ReachDFFwk*>::initialize(
       } else if (auto *GV{dyn_cast<GlobalValue>(V)};
                  GV && GV->hasGlobalUnnamedAddr()) {
         return false;
+      } else if (isa<GEPOperator>(V)) {
+        auto IsOnlyGEPUsers{true};
+        for_each_user_insts(const_cast<Value &>(*V),
+                            [&IsOnlyGEPUsers](auto *U) {
+                              IsOnlyGEPUsers &= isa<GEPOperator>(U);
+                            });
+        return !IsOnlyGEPUsers;
       }
       return true;
     };
@@ -681,34 +898,39 @@ void DataFlowTraits<ReachDFFwk*>::initialize(
     auto &DFI = DFF->getRegionInfo();
     auto &AA = AT.getAliasAnalysis();
     auto add = [&AT, &AA, &DL, &DFI, &DT, &DU,
-                DFF](AliasNode *AN, const Instruction &I,
+                DFF, N](AliasNode *AN, EstimateMemory *EM, const Instruction &I,
                      const MemoryLocation &Loc, AccessInfo W, AccessInfo R) {
       switch (W) {
       case AccessInfo::No:
         if (R != AccessInfo::No)
           for_each_alias(&AT, AN,
-                         AddUseFunctor(AA, DL, DFI, DT, I, Loc, *DU, DFF));
+                         AddUseFunctor(AA, DL, DFI, DT, I, Loc, EM, *DU, DFF,
+                         N));
         break;
       case AccessInfo::May:
         if (R != AccessInfo::No)
           for_each_alias(
-              &AT, AN, AddMayDefUseFunctor(AA, DL, DFI, DT, I, Loc, *DU, DFF));
+              &AT, AN, AddMayDefUseFunctor(AA, DL, DFI, DT, I, Loc, EM, *DU,
+                                           DFF, N));
         else
           for_each_alias(&AT, AN,
-                         AddMayDefFunctor(AA, DL, DFI, DT, I, Loc, *DU, DFF));
+                         AddMayDefFunctor(AA, DL, DFI, DT, I, Loc, EM, *DU,
+                                          DFF, N));
         break;
       case AccessInfo::Must:
         if (R != AccessInfo::No)
           for_each_alias(&AT, AN,
-                         AddDefUseFunctor(AA, DL, DFI, DT, I, Loc, *DU, DFF));
+                         AddDefUseFunctor(AA, DL, DFI, DT, I, Loc, EM, *DU,
+                                          DFF, N));
         else
           for_each_alias(&AT, AN,
-                         AddDefFunctor(AA, DL, DFI, DT, I, Loc, *DU, DFF));
+                         AddDefFunctor(AA, DL, DFI, DT, I, Loc, EM, *DU, DFF,
+                                       N));
         break;
       }
     };
     for_each_memory(I, TLI,
-      [&AA, &DL, &AT, InterDUInfo, &DU, &add](Instruction &I,
+      [&AA, &DL, &AT, InterDUInfo, &DU, &add, &N, &DFF](Instruction &I,
           MemoryLocation &&Loc, unsigned Idx, AccessInfo R, AccessInfo W) {
         auto *EM = AT.find(Loc);
         // EM may be smaller than Loc if it is known that access out of the
@@ -725,8 +947,13 @@ void DataFlowTraits<ReachDFFwk*>::initialize(
         for (auto *APtr : *EM) {
           MemoryLocation ALoc(APtr, EM->getSize(), EM->getAAInfo());
           auto AR = aliasRelation(AA, DL, Loc, ALoc);
-          if (AR.template is<trait::CoincideAlias>())
+          if (AR.template is<trait::CoincideAlias>()) {
             DU->addExplicitAccess(ALoc);
+            auto ColLoc = aggregate(nullptr, nullptr, ALoc, DFF).first;
+            if (ColLoc.Kind == MemoryLocationRange::LocKind::Collapsed) {
+              DU->addNodeOfCollapsableExplicitAccess(ALoc, ColLoc, N);
+            }
+          }
         }
         auto AN = EM->getAliasNode(AT);
         assert(AN && "Alias node must not be null!");
@@ -763,7 +990,7 @@ void DataFlowTraits<ReachDFFwk*>::initialize(
                 W = R = AccessInfo::May; break;
             }
         }
-        add(AN, I, Loc, W, R);
+        add(AN, EM, I, Loc, W, R);
       },
       [&DL, &DFI, &DT, &AT, &DU, InterDUInfo, &add](Instruction &I, AccessInfo,
           AccessInfo) {
@@ -801,7 +1028,7 @@ void DataFlowTraits<ReachDFFwk*>::initialize(
                       W = AccessInfo::May;
                     if (InterDUItr->get<DefUseSet>()->hasUse(Loc))
                       R = AccessInfo::Must;
-                    add(EM->getAliasNode(AT), I, Loc, W, R);
+                    add(EM->getAliasNode(AT), EM, I, Loc, W, R);
                   }
                 if (!HasUnknownAccess)
                   return;
@@ -919,9 +1146,45 @@ void ReachDFFwk::collapse(DFRegion *R) {
                              const MemoryLocationRange &Loc) {
     dbgs() << Msg;
     printLocationSource(dbgs(), Loc, &getDomTree());
-    dbgs() << " (" << Loc.getKindAsString() << ")\n";
+    dbgs() << " (" << Loc.getKindAsString() << ")";
+    int64_t Offset = -1;
+    dbgs() << " | Base Ptr: " << GetPointerBaseWithConstantOffset(
+      Loc.Ptr, Offset, getDataLayout()) << ", Offset: " << Offset << "\n";
   };
   #endif
+  auto MaySkipAuxiliaryLocation = [this](const MemoryLocationRange &Loc,
+                                         const LocationSet &LS) -> bool {
+    bool AreAllCollapsedOrAuxiliary = true;
+    bool HasCollapsed = false;
+    auto *GV{dyn_cast<GlobalValue>(getUnderlyingObject(Loc.Ptr, 0))};
+    for (auto &OtherLoc : LS) {
+      if (&Loc == &OtherLoc)
+        continue;
+      auto *OtherGV{dyn_cast<GlobalValue>(
+          getUnderlyingObject(OtherLoc.Ptr, 0))};
+      if (GV == OtherGV) {
+        if ((OtherLoc.Kind & MemoryLocationRange::LocKind::Collapsed) &&
+            !(OtherLoc.Kind & MemoryLocationRange::LocKind::Auxiliary))
+          HasCollapsed = true;
+        if (!(OtherLoc.Kind & MemoryLocationRange::LocKind::Auxiliary) &&
+            !(OtherLoc.Kind & MemoryLocationRange::LocKind::Collapsed)) {
+          AreAllCollapsedOrAuxiliary = false;
+          break;
+        }
+      }
+    }
+    if (AreAllCollapsedOrAuxiliary && HasCollapsed)
+      return true;
+    return false;
+  };
+  auto IsNonCollapsableWithConstIndex = [this](const GlobalValue *GV,
+                                               const MemoryLocationRange &Loc) {
+    int64_t Offset;
+    auto *BasePtr = GetPointerBaseWithConstantOffset(
+        Loc.Ptr, Offset, getDataLayout());
+    return Loc.Kind == MemoryLocationRange::LocKind::NonCollapsable &&
+           BasePtr == GV;
+  };
   for (DFNode *N : R->getNodes()) {
     auto DefItr = getDefInfo().find(N);
     assert(DefItr != getDefInfo().end() &&
@@ -945,18 +1208,70 @@ void ReachDFFwk::collapse(DFRegion *R) {
           continue;
       }
       LLVM_DEBUG(printLocInfo("[COLLAPSE] Collapse Use location: ", Loc));
-      distribute(aggregate(R, Loc, this), Loc, OwnUses, OtherUses);
+      distribute(aggregate(R, N, Loc, this), Loc, OwnUses, OtherUses);
     }
-    OwnUses.clarify(OtherUses);
+    LocationSet NewUses;
     for (auto &Loc : OwnUses) {
       SmallVector<MemoryLocationRange, 4> UseDiff;
       if (MustReachIn.subtractFrom(Loc, UseDiff)) {
         for (auto &L : UseDiff) {
           LLVM_DEBUG(printLocInfo("[COLLAPSE] Add Use location: ", L));
-          DefUse->addUse(L);
+          NewUses.insert(L);
         }
       } else {
         LLVM_DEBUG(printLocInfo("[COLLAPSE] Add entire Use location: ", Loc));
+        NewUses.insert(Loc);
+      }
+    }
+    for (auto &Loc : NewUses) {
+      // Check if the location is strictly default, not collapsable.
+      auto *GV{dyn_cast<GlobalValue>(
+          getUnderlyingObject(Loc.Ptr, 0))};
+      bool SkipExcessUse = false;
+      LLVM_DEBUG(
+        dbgs() << "Check location: ";
+        printLocationSource(dbgs(), Loc, &getDomTree());
+        dbgs() << " | " << Loc.Ptr << "\n";
+        dbgs() << "Underlying object: " << GV << "\n";
+        dbgs() << "IsExplicit:" << DU->getExplicitAccesses().overlap(Loc) << "\n";
+      );
+      if ((Loc.Kind == MemoryLocationRange::LocKind::Default ||
+           Loc.Kind == MemoryLocationRange::LocKind::Auxiliary) &&
+           GV == Loc.Ptr && !DU->getExplicitAccesses().overlap(Loc)) {
+        uint64_t SameUnderlyingObjCount = 0;
+        bool AreAllCollapsed = true;
+        for (auto &OtherLoc : NewUses) {
+          auto *OtherGV{dyn_cast<GlobalValue>(
+            getUnderlyingObject(OtherLoc.Ptr, 0))};
+          if (GV == OtherGV) {
+            SameUnderlyingObjCount++;
+            if (Loc.Ptr != OtherLoc.Ptr) {
+              AreAllCollapsed = false;
+              break;
+            }
+          }
+        }
+        if (AreAllCollapsed && SameUnderlyingObjCount > 1)
+          SkipExcessUse = true;
+      } else if (Loc.Kind & MemoryLocationRange::LocKind::Auxiliary) {
+        SkipExcessUse = MaySkipAuxiliaryLocation(Loc, NewUses);
+      } else if (IsNonCollapsableWithConstIndex(GV, Loc)) {
+        auto MaySkipNonCollapsable = true;
+        for (auto &OtherLoc : NewUses) {
+          auto *OtherGV{dyn_cast<GlobalValue>(
+            getUnderlyingObject(OtherLoc.Ptr, 0))};
+          if (GV == OtherGV) {
+            if (!(OtherLoc.Kind & MemoryLocationRange::LocKind::Auxiliary) &&
+                !(OtherLoc.Kind & MemoryLocationRange::LocKind::Collapsed) &&
+                !IsNonCollapsableWithConstIndex(OtherGV, OtherLoc)) {
+              MaySkipNonCollapsable = false;
+              break;
+            }
+          }
+        }
+        SkipExcessUse = MaySkipNonCollapsable;
+      }
+      if (!SkipExcessUse) {
         DefUse->addUse(Loc);
       }
     }
@@ -1011,12 +1326,12 @@ void ReachDFFwk::collapse(DFRegion *R) {
           for (auto &L : Locs) {
             LLVM_DEBUG(printLocInfo(
                 "[COLLAPSE] Add location from a latch node: ", L));
-            distribute(aggregate(R, L, this), Loc, OwnDefs, OtherDefs);
+            distribute(aggregate(R, N, L, this), Loc, OwnDefs, OtherDefs);
           }
         } else {
           LLVM_DEBUG(printLocInfo(
               "[COLLAPSE] Collapse MayDef location of a latch node: ", Loc));
-          distribute(aggregate(R, Loc, this), Loc, OwnMayDefs, OtherMayDefs);
+          distribute(aggregate(R, N, Loc, this), Loc, OwnMayDefs, OtherMayDefs);
         }
       }
       LLVM_DEBUG(dbgs() << "[COLLAPSE] Check ExitingDefs.\n");
@@ -1025,25 +1340,30 @@ void ReachDFFwk::collapse(DFRegion *R) {
       if (!Locs.empty()) {
         for (auto &L : Locs) {
           LLVM_DEBUG(printLocInfo("[COLLAPSE] Collapse Def location: ", L));
-          distribute(aggregate(R, L, this), Loc, OwnDefs, OtherDefs);
+          distribute(aggregate(R, N, L, this), Loc, OwnDefs, OtherDefs);
         }
       } else {
         LLVM_DEBUG(printLocInfo("[COLLAPSE] Collapse MayDef location: ", Loc));
-        distribute(aggregate(R, Loc, this), Loc, OwnMayDefs, OtherMayDefs);
+        distribute(aggregate(R, N, Loc, this), Loc, OwnMayDefs, OtherMayDefs);
       }
     }
     OwnDefs.clarify(OtherDefs);
-    DefUse->addDefs(OwnDefs);
+    for (auto &Loc : OwnDefs) {
+      if (!(Loc.Kind & MemoryLocationRange::LocKind::Auxiliary) ||
+          !MaySkipAuxiliaryLocation(Loc, OwnDefs))
+        DefUse->addDef(Loc);
+    }
     for (auto &Loc : DU->getMayDefs()) {
       if (Loc.Kind & MemoryLocationRange::LocKind::Hint)
         continue;
       LLVM_DEBUG(printLocInfo("[COLLAPSE] Collapse MayDef location: ", Loc));
-      distribute(aggregate(R, Loc, this), Loc, OwnMayDefs, OtherMayDefs);
+      distribute(aggregate(R, N, Loc, this), Loc, OwnMayDefs, OtherMayDefs);
     }
     OwnMayDefs.clarify(OtherMayDefs);
     DefUse->addMayDefs(OwnMayDefs);
     DefUse->addExplicitAccesses(DU->getExplicitAccesses());
     DefUse->addExplicitUnknowns(DU->getExplicitUnknowns());
+    DefUse->addCollapsableExplicitAccesses(DU->getCollapsableExplicitAccesses());
     for (auto Loc : DU->getAddressAccesses())
       DefUse->addAddressAccess(Loc);
     for (auto &&[Loc, Insts] : DU->getAddressTransitives())
@@ -1069,36 +1389,44 @@ void ReachDFFwk::collapse(DFRegion *R) {
             EM = EM->getTopLevelParent();
     }
     LLVM_DEBUG(printLocInfo("[COLLAPSE] Collapse Explicit Access: ", Loc));
-    MemoryLocationRange ExpLoc = aggregate(R, Loc, this).first;
-    MemoryLocationRange NewLoc(Loc);
-    NewLoc.Kind |= MemoryLocationRange::LocKind::Hint;
-    // We use top-level parent (EM) if it is available to update def-use set.
-    // In the following example  `for (int I = 98; I >= 0; --I)  A[I] = A[I + 1];`
-    // `A[I]` does not alias `A[I+1]` because these are two different elements
-    // of array if a value of `I` is specified. In this case `A[I]` is not presented
-    // in  the `Use` set, so analysis recognizes `A` as privitizable. To overcome
-    // this issue we conservatively update def-use set according to accesses
-    // to the whole array `A`.
-    if (!DefUse->hasDef(Loc) &&
-        (ExpLoc.Kind == MemoryLocationRange::LocKind::Collapsed &&
-         DefUse->hasDef(ExpLoc)))
-      DefUse->addDef(NewLoc);
-    if (!DefUse->hasMayDef(Loc) &&
-        ((ExpLoc.Kind == MemoryLocationRange::LocKind::Collapsed &&
-          DefUse->hasMayDef(ExpLoc)) ||
-         (EM && any_of(*EM, [EM, &DefUse](auto *Ptr) {
-            return DefUse->hasMayDef(
-                MemoryLocation{Ptr, EM->getSize(), EM->getAAInfo()});
-          }))))
-      DefUse->addMayDef(NewLoc);
-    if (!DefUse->hasUse(Loc) &&
-        ((ExpLoc.Kind == MemoryLocationRange::LocKind::Collapsed &&
-          DefUse->hasUse(ExpLoc)) ||
-         (EM && any_of(*EM, [EM, &DefUse](auto *Ptr) {
-            return DefUse->hasUse(
-                MemoryLocation{Ptr, EM->getSize(), EM->getAAInfo()});
-          }))))
-      DefUse->addUse(NewLoc);
+    auto *DFNS = DefUse->getNodesOfCollapsableExplicitAccess(Loc);
+    llvm::SmallVector<const DFNode *, 4> Nodes; 
+    if (DFNS)
+      Nodes.append(DFNS->begin(), DFNS->end());
+    if (Nodes.empty())
+      Nodes.push_back(nullptr);
+    for (auto *N : Nodes) {
+      MemoryLocationRange ExpLoc = aggregate(R, N, Loc, this).first;
+      MemoryLocationRange NewLoc(Loc);
+      NewLoc.Kind |= MemoryLocationRange::LocKind::Hint;
+      // We use top-level parent (EM) if it is available to update def-use set.
+      // In the following example  `for (int I = 98; I >= 0; --I)  A[I] = A[I + 1];`
+      // `A[I]` does not alias `A[I+1]` because these are two different elements
+      // of array if a value of `I` is specified. In this case `A[I]` is not presented
+      // in  the `Use` set, so analysis recognizes `A` as privitizable. To overcome
+      // this issue we conservatively update def-use set according to accesses
+      // to the whole array `A`.
+      if (!DefUse->hasDef(Loc) &&
+          (ExpLoc.Kind == MemoryLocationRange::LocKind::Collapsed &&
+          DefUse->hasDef(ExpLoc)))
+        DefUse->addDef(NewLoc);
+      if (!DefUse->hasMayDef(Loc) &&
+          ((ExpLoc.Kind == MemoryLocationRange::LocKind::Collapsed &&
+            DefUse->hasMayDef(ExpLoc)) ||
+          (EM && any_of(*EM, [EM, &DefUse](auto *Ptr) {
+              return DefUse->hasMayDef(
+                  MemoryLocation{Ptr, EM->getSize(), EM->getAAInfo()});
+            }))))
+        DefUse->addMayDef(NewLoc);
+      if (!DefUse->hasUse(Loc) &&
+          ((ExpLoc.Kind == MemoryLocationRange::LocKind::Collapsed &&
+            DefUse->hasUse(ExpLoc)) ||
+          (EM && any_of(*EM, [EM, &DefUse](auto *Ptr) {
+              return DefUse->hasUse(
+                  MemoryLocation{Ptr, EM->getSize(), EM->getAAInfo()});
+            }))))
+        DefUse->addUse(NewLoc);
+    }
   }
   LLVM_DEBUG(intializeDefUseSetLog(*R, *DefUse, getDomTree()));
 }
diff --git a/lib/Analysis/Memory/Delinearization.cpp b/lib/Analysis/Memory/Delinearization.cpp
index 43fb129a..1da4271e 100644
--- a/lib/Analysis/Memory/Delinearization.cpp
+++ b/lib/Analysis/Memory/Delinearization.cpp
@@ -177,7 +177,9 @@ void delinearizationLog(const DelinearizeInfo &Info, ScalarEvolution &SE,
     }
     OS << "  accesses:\n";
     for (auto &Range : *ArrayInfo) {
-      OS << "    address: ";
+      OS << "    "
+         << "[" << (Range.isValid() ? "valid" : "invalid") << "] "
+         << "address: ";
       Range.Ptr->print(OS, true);
       OS << "\n";
       for (auto *S : Range.Subscripts) {
@@ -222,9 +224,9 @@ void DelinearizationPass::cleanSubscripts(Array &ArrayInfo) {
                     << (ArrayInfo.isAddressOfVariable() ? "address of " : "")
                     << "base " << ArrayInfo.getBase()->getName() << "\n");
   auto addExtraConstZero =
-      [this, &ArrayInfo](const Array::Range &Range, unsigned ExtraZeroCount,
-                         const llvm::Type *DereferenceTy, unsigned Idx,
-                         SmallVectorImpl<const SCEV *> &NewSubscripts) -> bool {
+      [this](const Array::Range &Range, const llvm::Type *DereferenceTy,
+             unsigned Idx,
+             SmallVectorImpl<const SCEV *> &NewSubscripts) -> bool {
     auto *ATy{dyn_cast<ArrayType>(DereferenceTy)};
     if (!ATy)
       return false;
@@ -234,18 +236,11 @@ void DelinearizationPass::cleanSubscripts(Array &ArrayInfo) {
       if (ATy->getElementType() == Range.Types[Idx]) {
         NewSubscripts.push_back(Range.Subscripts[Idx]);
         ++Idx;
-      } else if (ExtraZeroCount > 0) {
-        --ExtraZeroCount;
-        NewSubscripts.push_back(mSE->getZero(mIndexTy));
       } else {
-        return false;
+        NewSubscripts.push_back(mSE->getZero(mIndexTy));
       }
     }
-    if (!ATy)
-      return Idx == IdxE;
-    for (unsigned I = 0; I < ExtraZeroCount; ++I)
-      NewSubscripts.push_back(mSE->getZero(mIndexTy));
-    return true;
+    return Idx == IdxE;
   };
   auto LastConstDim = ArrayInfo.getNumberOfDims();
   for (LastConstDim; LastConstDim > 0; --LastConstDim)
@@ -255,30 +250,31 @@ void DelinearizationPass::cleanSubscripts(Array &ArrayInfo) {
     for (auto &Range : ArrayInfo) {
       LLVM_DEBUG(dbgs() << "[DELINEARIZE]: process access ";
                  Range.Ptr->print(dbgs()); dbgs() << "\n");
-      if (auto ExtraZeroCount{
-          Range.is(Array::Range::NeedExtraZero)
-              ? ArrayInfo.getNumberOfDims() - Range.Subscripts.size()
-                                  : 0};
-          ExtraZeroCount > 0) {
-        SmallVector<const SCEV *, 4> NewSubscripts;
-        auto *BaseType{ArrayInfo.getBase()->getType()};
-        if (auto *GV{dyn_cast<GlobalValue>(ArrayInfo.getBase())})
-          BaseType = GV->getValueType();
-        else if (auto *AI{dyn_cast<AllocaInst>(ArrayInfo.getBase())})
-          BaseType = AI->getAllocatedType();
-        if (!addExtraConstZero(Range, ExtraZeroCount, BaseType, 0,
-                               NewSubscripts)) {
-          LLVM_DEBUG(dbgs() << "[DELINEARIZE]: unable to delinearize access to "
-                               "constant dimensions\n");
-          continue;
-        }
-        std::swap(Range.Subscripts, NewSubscripts);
-        LLVM_DEBUG(dbgs() << "[DELINEARIZE]: add " << ExtraZeroCount
-                          << " extra zero subscripts\n");
+      SmallVector<const SCEV *, 4> NewSubscripts;
+      auto *BaseType{ArrayInfo.getBase()->getType()};
+      if (auto *GV{dyn_cast<GlobalValue>(ArrayInfo.getBase())})
+        BaseType = GV->getValueType();
+      else if (auto *AI{dyn_cast<AllocaInst>(ArrayInfo.getBase())})
+        BaseType = AI->getAllocatedType();
+      if (!addExtraConstZero(Range, BaseType, 0, NewSubscripts) ||
+          NewSubscripts.size() > ArrayInfo.getNumberOfDims()) {
+        LLVM_DEBUG(dbgs() << "[DELINEARIZE]: unable to delinearize access to "
+                             "constant dimensions\n");
+        continue;
       }
+      if (Range.is(Array::Range::NeedExtraZero))
+        for (unsigned I = NewSubscripts.size(),
+                      EI = ArrayInfo.getNumberOfDims();
+             I < EI; ++I)
+          NewSubscripts.push_back(mSE->getZero(mIndexTy));
+      LLVM_DEBUG(if (Range.Subscripts.size() < NewSubscripts.size())
+        dbgs()  << "[DELINEARIZE]: add "
+                << NewSubscripts.size() - Range.Subscripts.size()
+                << " extra zero subscripts\n");
+      std::swap(Range.Subscripts, NewSubscripts);
+      Range.setProperty(Array::Range::IsDelinearized);
       assert(Range.Subscripts.size() <= ArrayInfo.getNumberOfDims() &&
              "Unable to delinearize element access!");
-      Range.setProperty(Array::Range::IsDelinearized);
     }
     return;
   }
@@ -295,10 +291,11 @@ void DelinearizationPass::cleanSubscripts(Array &ArrayInfo) {
     // So, we try to add extra zero subscripts.
     auto ExtraZeroCount = Range.is(Array::Range::NeedExtraZero) ?
       ArrayInfo.getNumberOfDims() - Range.Subscripts.size() : 0;
-    std::size_t DimIdx = 0, SubscriptIdx = 0;
-    std::size_t DimIdxE = std::min(LastConstDim - 1, Range.Subscripts.size());
+    unsigned DimIdx = 0, SubscriptIdx = 0;
+    unsigned NumberOfKnownSubscripts = Range.Subscripts.size();
     SmallVector<const SCEV *, 4> NewSubscripts;
-    for (;  DimIdx < DimIdxE; ++DimIdx) {
+    for (; DimIdx < LastConstDim - 1 && DimIdx < NumberOfKnownSubscripts;
+         ++DimIdx) {
       auto *Subscript = Range.Subscripts[SubscriptIdx++];
       LLVM_DEBUG(dbgs() << "[DELINEARIZE]: subscript " << DimIdx << ": "
                         << *Subscript << "\n");
@@ -326,34 +323,51 @@ void DelinearizationPass::cleanSubscripts(Array &ArrayInfo) {
       NewSubscripts.push_back(Subscript);
       LLVM_DEBUG(dbgs() << "[DELINEARIZE]: set to " << *Subscript << "\n");
     }
-    if (DimIdx < DimIdxE)
+    if (DimIdx < LastConstDim - 1 && DimIdx < NumberOfKnownSubscripts)
       continue;
-    if (ExtraZeroCount > 0) {
-      LLVM_DEBUG(dbgs() << "[DELINEARIZE]: add " << ExtraZeroCount
-                        << " extra zero subscripts after " << SubscriptIdx
-                        << "\n");
-      if (Range.Subscripts.size() > SubscriptIdx) {
-        NewSubscripts.push_back(Range.Subscripts[SubscriptIdx]);
-        if (!addExtraConstZero(Range, ExtraZeroCount, Range.Types[SubscriptIdx],
-                               SubscriptIdx + 1, NewSubscripts)) {
-          if (SubscriptIdx == 0 ||
-              !(NewSubscripts.pop_back(),
-                addExtraConstZero(Range, ExtraZeroCount,
-                                  Range.Types[SubscriptIdx - 1], SubscriptIdx,
-                                  NewSubscripts))) {
-            LLVM_DEBUG(dbgs() << "[DELINEARIZE]: unable to delinearize\n");
-            continue;
-          }
+    if (LastConstDim == ArrayInfo.getNumberOfDims()) {
+      if (NumberOfKnownSubscripts > SubscriptIdx) {
+        NewSubscripts.push_back(Range.Subscripts[SubscriptIdx++]);
+        if (SubscriptIdx != NumberOfKnownSubscripts) {
+          LLVM_DEBUG(dbgs() << "[DELINEARIZE]: unable to delinearize, too many "
+                               "subscripts left\n");
+          continue;
         }
-      } else {
-        for (std::size_t I = 0; I < ExtraZeroCount; ++I)
-          NewSubscripts.push_back(mSE->getZero(mIndexTy));
+        assert(NewSubscripts.size() == ArrayInfo.getNumberOfDims() &&
+               ExtraZeroCount == 0 && "Invariant broken!");
       }
-    } else {
-      // Add subscripts for constant dimensions.
-      for (auto EI = Range.Subscripts.size(); SubscriptIdx < EI; ++SubscriptIdx)
-        NewSubscripts.push_back(Range.Subscripts[SubscriptIdx]);
+    } else if (NumberOfKnownSubscripts > SubscriptIdx) {
+      unsigned StashSize = NewSubscripts.size();
+      NewSubscripts.push_back(Range.Subscripts[SubscriptIdx]);
+      if (!addExtraConstZero(Range, Range.Types[SubscriptIdx],
+                             SubscriptIdx + 1, NewSubscripts) ||
+         NewSubscripts.size() > ArrayInfo.getNumberOfDims()) {
+        if (SubscriptIdx == 0 ||
+            !(NewSubscripts.resize(StashSize),
+              NewSubscripts.push_back(mSE->getZero(mIndexTy)),
+              addExtraConstZero(Range, Range.Types[SubscriptIdx - 1],
+                                SubscriptIdx, NewSubscripts)) ||
+            NewSubscripts.size() > ArrayInfo.getNumberOfDims()) {
+          LLVM_DEBUG(dbgs() << "[DELINEARIZE]: unable to delinearize\n");
+          continue;
+        }
+      }
+      LLVM_DEBUG(
+        if (NumberOfKnownSubscripts - SubscriptIdx + StashSize <
+            NewSubscripts.size())
+          dbgs() << "[DELINEARIZE]: add "
+                 << NewSubscripts.size() -
+                        (NumberOfKnownSubscripts - SubscriptIdx + StashSize)
+                 << " extra zero subscripts after " << SubscriptIdx << "\n");
+      ExtraZeroCount = std::min(
+          ArrayInfo.getNumberOfDims() - NewSubscripts.size(), ExtraZeroCount);
     }
+    LLVM_DEBUG(
+      if (ExtraZeroCount > 0)
+        dbgs() << "[DELINEARIZE]: add " << ExtraZeroCount
+               << " extra zero subscripts to finalize range delinearization\n");
+    for (std::size_t I = 0; I < ExtraZeroCount; ++I)
+      NewSubscripts.push_back(mSE->getZero(mIndexTy));
     std::swap(Range.Subscripts, NewSubscripts);
     assert(Range.Subscripts.size() <= ArrayInfo.getNumberOfDims() &&
       "Unable to delinearize element access!");
@@ -588,100 +602,106 @@ void DelinearizationPass::findArrayDimensionsFromDbgInfo(Array &ArrayInfo) {
 
 void DelinearizationPass::collectArrays(Function &F) {
   DenseSet<const Value *> Visited;
-  for (auto &I : instructions(F)) {
-    auto processMemory = [this, &Visited](Instruction &I, MemoryLocation Loc,
-        unsigned,  AccessInfo, AccessInfo) {
-      if (auto II = dyn_cast<IntrinsicInst>(&I)) {
-        if (isMemoryMarkerIntrinsic(II->getIntrinsicID()) ||
-            isDbgInfoIntrinsic(II->getIntrinsicID()))
-          return;
-      }
-      if (!Visited.insert(Loc.Ptr).second)
+  DenseSet<const Instruction *> Deferred;
+  auto processMemory = [this, &Visited](const Instruction &I,
+      MemoryLocation Loc, unsigned,  AccessInfo, AccessInfo) {
+    if (auto II = dyn_cast<IntrinsicInst>(&I)) {
+      if (isMemoryMarkerIntrinsic(II->getIntrinsicID()) ||
+          isDbgInfoIntrinsic(II->getIntrinsicID()))
         return;
-      LLVM_DEBUG(dbgs() << "[DELINEARIZE]: process instruction ";
-        I.print(dbgs()); dbgs() << "\n");
-      auto &DL = I.getModule()->getDataLayout();
-      auto *BasePtr = const_cast<Value *>(Loc.Ptr);
-      auto *DataPtr = BasePtr;
-      bool IsAddressOfVariable;
-      std::tie(BasePtr, DataPtr, IsAddressOfVariable) =
-        GetUnderlyingArray(BasePtr, DL);
-      LLVM_DEBUG(
-        dbgs() << "[DELINEARIZE]: strip to "
-               << (IsAddressOfVariable ? "address of " : "")
-               << "base " << *BasePtr << "\n");
-      auto ArrayPtr = mDelinearizeInfo.findArray(BasePtr, IsAddressOfVariable);
-      if (!ArrayPtr) {
-        ArrayPtr = *mDelinearizeInfo.getArrays().insert(
-          new Array(BasePtr, IsAddressOfVariable)).first;
-        findArrayDimensionsFromDbgInfo(*ArrayPtr);
-      }
-      auto NumberOfDims = ArrayPtr->getNumberOfDims();
-      SmallVector<GEPOperator *, 4> GEPs;
-      auto RangePtr = Loc.Ptr;
-      auto *GEP = dyn_cast<GEPOperator>(const_cast<Value *>(RangePtr));
-      while (!GEP) {
-        if (Operator::getOpcode(RangePtr) == Instruction::BitCast ||
-            Operator::getOpcode(RangePtr) == Instruction::AddrSpaceCast)
-          RangePtr = cast<Operator>(RangePtr)->getOperand(0);
-        else
-          break;
-        GEP = dyn_cast<GEPOperator>(const_cast<Value *>(RangePtr));
-      }
-      while (GEP) {
-        GEPs.push_back(GEP);
-        GEP = dyn_cast<GEPOperator>(GEP->getPointerOperand());
+    }
+    if (!Visited.insert(Loc.Ptr).second)
+      return;
+    LLVM_DEBUG(dbgs() << "[DELINEARIZE]: process instruction ";
+      I.print(dbgs()); dbgs() << "\n");
+    auto &DL = I.getModule()->getDataLayout();
+    auto *BasePtr = const_cast<Value *>(Loc.Ptr);
+    auto *DataPtr = BasePtr;
+    bool IsAddressOfVariable;
+    std::tie(BasePtr, DataPtr, IsAddressOfVariable) =
+      GetUnderlyingArray(BasePtr, DL);
+    LLVM_DEBUG(
+      dbgs() << "[DELINEARIZE]: strip to "
+             << (IsAddressOfVariable ? "address of " : "")
+             << "base " << *BasePtr << "\n");
+    auto ArrayPtr = mDelinearizeInfo.findArray(BasePtr, IsAddressOfVariable);
+    if (!ArrayPtr) {
+      ArrayPtr = *mDelinearizeInfo.getArrays().insert(
+        new Array(BasePtr, IsAddressOfVariable)).first;
+      findArrayDimensionsFromDbgInfo(*ArrayPtr);
+    }
+    auto NumberOfDims = ArrayPtr->getNumberOfDims();
+    SmallVector<GEPOperator *, 4> GEPs;
+    auto RangePtr = Loc.Ptr;
+    auto *GEP = dyn_cast<GEPOperator>(const_cast<Value *>(RangePtr));
+    while (!GEP) {
+      if (Operator::getOpcode(RangePtr) == Instruction::BitCast ||
+          Operator::getOpcode(RangePtr) == Instruction::AddrSpaceCast)
+        RangePtr = cast<Operator>(RangePtr)->getOperand(0);
+      else
+        break;
+      GEP = dyn_cast<GEPOperator>(const_cast<Value *>(RangePtr));
+    }
+    while (GEP) {
+      GEPs.push_back(GEP);
+      GEP = dyn_cast<GEPOperator>(GEP->getPointerOperand());
+    }
+    auto &Range = ArrayPtr->addRange(const_cast<Value *>(Loc.Ptr));
+    if (!isa<GEPOperator>(RangePtr) &&
+        !(RangePtr == BasePtr && !IsAddressOfVariable) &&
+        !(RangePtr == DataPtr && IsAddressOfVariable))
+      Range.setProperty(Array::Range::NoGEP);
+    SmallVector<std::tuple<Value *, Type *>, 4> SubscriptValues;
+    bool UseAllSubscripts = extractSubscriptsFromGEPs(
+      GEPs.begin(), GEPs.end(), NumberOfDims, SubscriptValues);
+    if (!UseAllSubscripts)
+      Range.setProperty(Array::Range::IgnoreGEP);
+    // In some cases zero subscript is dropping out by optimization passes.
+    // So, we try to add extra zero subscripts later. We add subscripts for
+    // instructions which access a single element, for example, in case of
+    // a call it is possible to pass a whole array as a parameter
+    // (without GEPs).
+    if (isa<LoadInst>(I) || isa<StoreInst>(I) ||
+        isa<AtomicRMWInst>(I) || isa<AtomicCmpXchgInst>(I)) {
+      Range.setProperty(Array::Range::IsElement);
+      if (SubscriptValues.size() < NumberOfDims) {
+        ArrayPtr->setRangeRef();
+        Range.setProperty(Array::Range::NeedExtraZero);
       }
-      auto &Range = ArrayPtr->addRange(const_cast<Value *>(Loc.Ptr));
-      if (!isa<GEPOperator>(RangePtr) &&
-          !(RangePtr == BasePtr && !IsAddressOfVariable) &&
-          !(RangePtr == DataPtr && IsAddressOfVariable))
-        Range.setProperty(Array::Range::NoGEP);
-      SmallVector<std::tuple<Value *, Type *>, 4> SubscriptValues;
-      bool UseAllSubscripts = extractSubscriptsFromGEPs(
-        GEPs.begin(), GEPs.end(), NumberOfDims, SubscriptValues);
-      if (!UseAllSubscripts)
-        Range.setProperty(Array::Range::IgnoreGEP);
-      // In some cases zero subscript is dropping out by optimization passes.
-      // So, we try to add extra zero subscripts later. We add subscripts for
-      // instructions which access a single element, for example, in case of
-      // a call it is possible to pass a whole array as a parameter
-      // (without GEPs).
-      if (isa<LoadInst>(I) || isa<StoreInst>(I) ||
-          isa<AtomicRMWInst>(I) || isa<AtomicCmpXchgInst>(I)) {
-        Range.setProperty(Array::Range::IsElement);
-        if (SubscriptValues.size() < NumberOfDims) {
-          ArrayPtr->setRangeRef();
-          Range.setProperty(Array::Range::NeedExtraZero);
-        }
+    }
+    if (!SubscriptValues.empty()) {
+      ArrayPtr->setRangeRef();
+      for (auto &&[V, T] : SubscriptValues) {
+        Range.Subscripts.push_back(mSE->getSCEV(V));
+        Range.Types.push_back(T);
       }
-      if (!SubscriptValues.empty()) {
-        ArrayPtr->setRangeRef();
-        for (auto &&[V, T] : SubscriptValues) {
-          Range.Subscripts.push_back(mSE->getSCEV(V));
-          Range.Types.push_back(T);
-        }
+    }
+    LLVM_DEBUG(
+      dbgs() << "[DELINEARIZE]: number of dimensions "
+             << NumberOfDims << "\n";
+      dbgs() << "[DELINEARIZE]: number of subscripts "
+             << Range.Subscripts.size() << "\n";
+      if (Range.is(Array::Range::NeedExtraZero))
+        dbgs() << "[DELINEARIZE]: need extra zero subscripts\n";
+      if (Range.is(Array::Range::IgnoreGEP))
+        dbgs() << "[DELINEARIZE]: ignore some beginning GEPs\n";
+      if (Range.is(Array::Range::NoGEP))
+        dbgs() << "[DELINEARIZE]: no GEPs found\n";
+      dbgs() << "[DELINEARIZE]: subscripts: \n";
+      for (auto *Subscript : Range.Subscripts) {
+        dbgs() << "  "; Subscript->print(dbgs()); dbgs() <<"\n";
       }
-      LLVM_DEBUG(
-        dbgs() << "[DELINEARIZE]: number of dimensions "
-               << NumberOfDims << "\n";
-        dbgs() << "[DELINEARIZE]: number of subscripts "
-               << Range.Subscripts.size() << "\n";
-        if (Range.is(Array::Range::NeedExtraZero))
-          dbgs() << "[DELINEARIZE]: need extra zero subscripts\n";
-        if (Range.is(Array::Range::IgnoreGEP))
-          dbgs() << "[DELINEARIZE]: ignore some beginning GEPs\n";
-        if (Range.is(Array::Range::NoGEP))
-          dbgs() << "[DELINEARIZE]: no GEPs found\n";
-        dbgs() << "[DELINEARIZE]: subscripts: \n";
-        for (auto *Subscript : Range.Subscripts) {
-          dbgs() << "  "; Subscript->print(dbgs()); dbgs() <<"\n";
-        }
-      );
-    };
+    );
+  };
+  for (auto &I : instructions(F)) {
     for_each_memory(I, *mTLI, processMemory,
       [](Instruction &, AccessInfo, AccessInfo) {});
+    if (isa<GetElementPtrInst>(I))
+      Deferred.insert(&I);
   }
+  for (auto *I : Deferred)
+    processMemory(*I, MemoryLocation(I, LocationSize::beforeOrAfterPointer()),
+                  0, AccessInfo::No, AccessInfo::No);
   // Now, we remove all object which is not arrays.
   for (auto Itr = mDelinearizeInfo.getArrays().begin(),
        ItrE = mDelinearizeInfo.getArrays().end(); Itr != ItrE;) {
diff --git a/lib/Analysis/Memory/EstimateMemory.cpp b/lib/Analysis/Memory/EstimateMemory.cpp
index 657b325a..de6e33fe 100644
--- a/lib/Analysis/Memory/EstimateMemory.cpp
+++ b/lib/Analysis/Memory/EstimateMemory.cpp
@@ -1115,6 +1115,14 @@ bool EstimateMemoryPass::runOnFunction(Function &F) {
         return;
     if (AccessedMemory.count(V))
       return;
+  if (auto *GEP{dyn_cast<GEPOperator>(V)}) {
+    auto IsOnlyGEPUsers{true};
+    for_each_user_insts(const_cast<Value &>(*V), [&IsOnlyGEPUsers](auto *U) {
+      IsOnlyGEPUsers &= isa<GEPOperator>(U);
+    });
+    if (IsOnlyGEPUsers)
+      return;
+  }    
     auto PointeeTy{getPointerElementType(*V)};
     addLocation(MemoryLocation(
         V, PointeeTy && PointeeTy->isSized()
diff --git a/lib/Analysis/Memory/GlobalDefinedMemory.cpp b/lib/Analysis/Memory/GlobalDefinedMemory.cpp
index d8a57679..66da2b70 100644
--- a/lib/Analysis/Memory/GlobalDefinedMemory.cpp
+++ b/lib/Analysis/Memory/GlobalDefinedMemory.cpp
@@ -22,6 +22,7 @@
 //===----------------------------------------------------------------------===//
 
 #include "tsar/Analysis/Attributes.h"
+#include "tsar/Analysis/Memory/AssumptionInfo.h"
 #include "tsar/Analysis/Memory/DefinedMemory.h"
 #include "tsar/Analysis/Memory/Delinearization.h"
 #include "tsar/Analysis/Memory/EstimateMemory.h"
@@ -96,7 +97,8 @@ using GlobalDefinedMemoryProvider = FunctionPassProvider<
   EstimateMemoryPass,
   DominatorTreeWrapperPass,
   DelinearizationPass,
-  ScalarEvolutionWrapperPass>;
+  ScalarEvolutionWrapperPass,
+  AssumptionInfoPass>;
 }
 
 INITIALIZE_PROVIDER_BEGIN(GlobalDefinedMemoryProvider,
@@ -108,6 +110,7 @@ INITIALIZE_PASS_DEPENDENCY(DominatorTreeWrapperPass)
 INITIALIZE_PASS_DEPENDENCY(ScalarEvolutionWrapperPass)
 INITIALIZE_PASS_DEPENDENCY(DelinearizationPass)
 INITIALIZE_PASS_DEPENDENCY(GlobalsAccessWrapper)
+INITIALIZE_PASS_DEPENDENCY(AssumptionInfoPass)
 INITIALIZE_PROVIDER_END(GlobalDefinedMemoryProvider, "global-def-mem-provider",
                         "Global Defined Memory Analysis (Provider)")
 
@@ -190,13 +193,15 @@ bool GlobalDefinedMemory::runOnModule(Module &SCC) {
     auto *DFF = cast<DFFunction>(RegInfo.getTopLevelRegion());
     auto &DI = Provider.get<DelinearizationPass>().getDelinearizeInfo();
     auto &SE = Provider.get<ScalarEvolutionWrapperPass>().getSE();
+    auto &AM = Provider.get<AssumptionInfoPass>().getAssumptionMap();
     DefinedMemoryInfo DefInfo;
-    ReachDFFwk ReachDefFwk(AT, TLI, RegInfo, DT, DI, SE, DL, GO, DefInfo,
+    ReachDFFwk ReachDefFwk(AT, TLI, RegInfo, DT, DI, SE, DL, AM, GO, DefInfo,
                            *Wrapper);
     solveDataFlowUpward(&ReachDefFwk, DFF);
     auto DefUseSetItr = ReachDefFwk.getDefInfo().find(DFF);
     assert(DefUseSetItr != ReachDefFwk.getDefInfo().end() &&
            "Def-use set must exist for a function!");
+    DefUseSetItr->get<DefUseSet>()->summarizeCollapsedLocations();
     Wrapper->try_emplace(F, std::move(DefUseSetItr->get<DefUseSet>()));
     LLVM_DEBUG(dbgs() << "[GLOBAL DEFINED MEMORY]: leave " << F->getName()
                       << "\n";);
diff --git a/lib/Analysis/Memory/GlobalLiveMemory.cpp b/lib/Analysis/Memory/GlobalLiveMemory.cpp
index 793c0a54..9011e16a 100644
--- a/lib/Analysis/Memory/GlobalLiveMemory.cpp
+++ b/lib/Analysis/Memory/GlobalLiveMemory.cpp
@@ -319,6 +319,18 @@ bool GlobalLiveMemory::runOnModule(Module &M) {
     LS->setOut(MayLives);
     LiveDFFwk LiveFwk(IntraLiveInfo, DefInfo, DT);
     solveDataFlowDownward(&LiveFwk, TopRegion);
+    auto ExpandCollapsed = [](LiveSet &LS) {
+      typedef MemorySet<MemoryLocationRange> LocationSet;
+      LocationSet DestIn, DestOut;
+      auto expand = [](const LocationSet &From, LocationSet &To) {
+        for (auto Loc : From)
+          To.insert(Loc.expand());
+      };
+      expand(LS.getIn(), DestIn);
+      expand(LS.getOut(), DestOut);
+      LS.setIn(std::move(DestIn));
+      LS.setOut(std::move(DestOut));
+    };
     auto &TLI = getAnalysis<TargetLibraryInfoWrapperPass>().getTLI(*F);
     for (auto &CallRecord : *CGN) {
       Function *Callee = CallRecord.second->getFunction();
@@ -345,7 +357,9 @@ bool GlobalLiveMemory::runOnModule(Module &M) {
             CallLiveOut.insert(MemoryLocationRange(Arg, 0, Loc.Size));
           },
           [](Instruction &, AccessInfo, AccessInfo) {});
+      ExpandCollapsed(*CallLS.get());
     }
+    ExpandCollapsed(*IntraLiveInfo[TopRegion].get());
     Wrapper->try_emplace(F, std::move(IntraLiveInfo[TopRegion]));
   }
   LLVM_DEBUG(visitedFunctionsLog(LiveSetForCalls));
diff --git a/lib/Analysis/Memory/LiveMemory.cpp b/lib/Analysis/Memory/LiveMemory.cpp
index a937f032..0e8bba8d 100644
--- a/lib/Analysis/Memory/LiveMemory.cpp
+++ b/lib/Analysis/Memory/LiveMemory.cpp
@@ -155,10 +155,10 @@ bool DataFlowTraits<LiveDFFwk*>::transferFunction(
   }
   dbgs() << "IN:\n";
   for (auto &Loc : newIn)
-    (printLocationSource(dbgs(), Loc.Ptr, DFF->getDomTree()), dbgs() << "\n");
+    (printLocationSource(dbgs(), Loc, DFF->getDomTree(), true), dbgs() << "\n");
   dbgs() << "OUT:\n";
   for (auto &Loc : LS->getOut())
-    (printLocationSource(dbgs(), Loc.Ptr, DFF->getDomTree()), dbgs() << "\n");
+    (printLocationSource(dbgs(), Loc, DFF->getDomTree(), true), dbgs() << "\n");
   dbgs() << "[END LIVE]\n";
   );
   if (LS->getIn() != newIn) {
diff --git a/lib/Analysis/Memory/MemoryLocationRange.cpp b/lib/Analysis/Memory/MemoryLocationRange.cpp
index 2ffa74f3..26132319 100644
--- a/lib/Analysis/Memory/MemoryLocationRange.cpp
+++ b/lib/Analysis/Memory/MemoryLocationRange.cpp
@@ -26,19 +26,23 @@
 #ifndef NDEBUG
 #include "tsar/Unparse/Utils.h"
 #endif
+#include "tsar/Support/SCEVUtils.h"
 #include <bcl/Equation.h>
+#include <llvm/Analysis/ScalarEvolution.h>
+#include <llvm/Analysis/ScalarEvolutionExpressions.h>
 #include <llvm/Support/Debug.h>
 
 using namespace tsar;
+using namespace llvm;
 
 #undef DEBUG_TYPE
-#define DEBUG_TYPE "def-mem"
+#define DEBUG_TYPE "inter-mem"
 
 namespace {
 typedef int64_t ColumnT;
 typedef int64_t ValueT;
 typedef MemoryLocationRange::Dimension Dimension;
-
+typedef std::pair<llvm::Optional<MemoryLocationRange>, bool> IntersectionResult;
 struct ColumnInfo {
   std::array<char, 3> Variables = {'X', 'Y', 'T'};
 
@@ -48,37 +52,106 @@ struct ColumnInfo {
   char name(ColumnT Column) const { return Variables[Column]; }
 };
 
+enum DimPairKind {
+  BothVariable,
+  OneStartOtherEndConst,
+  BothStartConst,
+  BothEndConst,
+  OneConstOtherSemiconst,
+  OneVariableOtherSemiconst,
+  BothConst,
+  OneConstOtherVariable,
+  Unknown
+};
+
+#ifndef NDEBUG
+std::string getKindAsString(DimPairKind Kind) {
+  switch (Kind)
+  {
+  case BothVariable:
+    return "BothVariable";
+  case OneStartOtherEndConst:
+    return "OneStartOtherEndConst";
+  case BothStartConst:
+    return "BothStartConst";
+  case BothEndConst:
+    return "BothEndConst";
+  case OneConstOtherSemiconst:
+    return "OneConstOtherSemiconst";
+  case OneVariableOtherSemiconst:
+    return "OneVariableOtherSemiconst";
+  case BothConst:
+    return "BothConst"; 
+  case OneConstOtherVariable:
+    return "OneConstOtherVariable";
+  default:
+    return "Unknown";
+  }
+}
+#endif
+
 /// Finds difference between dimensions D and I where I is a subset of D
 /// and adds results to Res. Return `false` if Threshold is exceeded, `true`
 /// otherwise.
 bool difference(const Dimension &D, const Dimension &I,
-                llvm::SmallVectorImpl<Dimension> &Res, std::size_t Threshold) {
-  if (D.Start < I.Start) {
+                llvm::SmallVectorImpl<Dimension> &Res,
+                llvm::ScalarEvolution *SE, std::size_t Threshold) {
+  assert(SE && "ScalarEvolution must be specified!");
+  assert(isa<SCEVConstant>(D.Step) && isa<SCEVConstant>(I.Step) &&
+         "Dimension step must be constant.");
+  assert(isa<SCEVConstant>(D.Start) && isa<SCEVConstant>(I.Start) &&
+         "Dimension start must be constant.");
+  if (*compareSCEVs(D.Start, I.Start, SE) < 0) {
     auto &Left = Res.emplace_back();
     Left.Step = D.Step;
     Left.Start = D.Start;
-    Left.TripCount = (I.Start - D.Start) / D.Step;
+    Left.End = subtractSCEVAndCast(I.Start, D.Step, SE);
+    assert(isa<SCEVConstant>(Left.Start) && isa<SCEVConstant>(Left.End) &&
+           "Dimension bounds must be constant.");
     Left.DimSize = D.DimSize;
   }
-  auto DEnd = D.Start + D.Step * (D.TripCount - 1);
-  auto IEnd = I.Start + I.Step * (I.TripCount - 1);
-  if (DEnd > IEnd) {
+  assert(isa<SCEVConstant>(D.End) && isa<SCEVConstant>(I.End) &&
+         "Dimension end must be constant.");
+  if (*compareSCEVs(D.End, I.End, SE) > 0) {
     auto &Right = Res.emplace_back();
     Right.Step = D.Step;
-    Right.Start = IEnd + D.Step;
-    Right.TripCount = (DEnd - IEnd) / D.Step;
+    Right.Start = addSCEVAndCast(I.End, D.Step, SE);
+    Right.End = D.End;
+    assert(isa<SCEVConstant>(Right.Start) && isa<SCEVConstant>(Right.End) &&
+           "Dimension start must be constant.");
     Right.DimSize = D.DimSize;
   }
-  if (I.TripCount > 1) {
+  if (*compareSCEVs(I.End, I.Start, SE) > 0) {
     // I.Step % D.Step is always 0 because I is a subset of D.
-    auto RepeatNumber = I.Step / D.Step - 1;
-    if (RepeatNumber > Threshold)
+    auto Quotient = divide(*SE, I.Step, D.Step).Quotient;
+    assert(isa<SCEVConstant>(Quotient) && "Quotient must be constant!");
+    // I.Step / D.Step - 1
+    auto RepeatNumber = subtractSCEVAndCast(
+        Quotient, SE->getOne(Quotient->getType()), SE);
+    auto RepeatNumberConst = dyn_cast<SCEVConstant>(RepeatNumber);
+    assert(RepeatNumberConst && "Repeat Number must be constant.");
+    if (RepeatNumberConst->getValue()->getZExtValue() > Threshold)
       return false;
-    for (auto J = 0; J < RepeatNumber; ++J) {
+    // I.TripCount = (I.End - I.Start) / Step + 1
+    // CenterTripCount = I.TripCount - 1 = (I.End - I.Start) / Step
+    auto CenterTripCountMinusOne = subtractSCEVAndCast(divide(*SE,
+        subtractSCEVAndCast(I.End, I.Start, SE), I.Step).Quotient,
+        SE->getOne(I.Step->getType()), SE);
+    assert(isa<SCEVConstant>(CenterTripCountMinusOne) &&
+           "Trip count must be constant!");
+    for (auto J = 0; J < RepeatNumberConst->getValue()->getZExtValue(); ++J) {
       auto &Center = Res.emplace_back();
-      Center.Start = I.Start + D.Step * (J + 1);
+      // Center.Start = I.Start + D.Step * (J + 1);
+      Center.Start = addSCEVAndCast(I.Start, SE->getMulExpr(
+          D.Step, SE->getConstant(I.Start->getType(), J + 1)), SE);
       Center.Step = I.Step;
-      Center.TripCount = I.TripCount - 1;
+      // Center.End = Center.Start + (Center.TripCount - 1) * Center.Step
+      Center.End = addSCEVAndCast(
+          Center.Start, SE->getMulExpr(CenterTripCountMinusOne, Center.Step), SE);
+      assert(isa<SCEVConstant>(Center.Start) && isa<SCEVConstant>(Center.End) &&
+             "Dimension bounds must be constant!");
+      assert(isa<SCEVConstant>(Center.Step) &&
+             "Dimension step must be constant!");
       Center.DimSize = D.DimSize;
     }
   }
@@ -152,26 +225,37 @@ void delinearize(const MemoryLocationRange &From, MemoryLocationRange &What) {
   }
   llvm::SmallVector<Dimension, 4> DimList(DimN);
   bool HasPartialCoverage = false;
+  assert(From.SE && "ScalarEvolution must be specified!");
+  auto SE = From.SE;
   for (int64_t I = DimN - 1; I >= 0; --I) {
     auto &CurrDim = DimList[I];
-    CurrDim.Step = 1;
-    CurrDim.DimSize = From.DimList[I].DimSize;
+    auto &FromDim = From.DimList[I];
+    CurrDim.Step = SE->getOne(FromDim.Step->getType());
+    CurrDim.DimSize = FromDim.DimSize;
     if (HasPartialCoverage) {
       if (LowerIdx[I] != UpperIdx[I])
         return;
-      CurrDim.Start = LowerIdx[I];
-      CurrDim.TripCount = 1;
+      CurrDim.Start = SE->getConstant(FromDim.Start->getType(), LowerIdx[I]);
+      CurrDim.End = CurrDim.Start;
+      assert(dyn_cast<SCEVConstant>(CurrDim.Start) &&
+             dyn_cast<SCEVConstant>(CurrDim.End) &&
+             "Dimension bounds must be constant!");
     } else {
-      CurrDim.Start = LowerIdx[I];
-      CurrDim.TripCount = UpperIdx[I] - LowerIdx[I] + 1;
-      if (LowerIdx[I] != 0 || UpperIdx[I] + 1 != From.DimList[I].DimSize)
+      CurrDim.Start = SE->getConstant(FromDim.Start->getType(), LowerIdx[I]);
+      CurrDim.End = SE->getConstant(FromDim.End->getType(), UpperIdx[I]);
+      assert(dyn_cast<SCEVConstant>(CurrDim.Start) &&
+             dyn_cast<SCEVConstant>(CurrDim.End) &&
+             "Dimension bounds must be constant!");
+      if (LowerIdx[I] != 0 || UpperIdx[I] + 1 != FromDim.DimSize)
         HasPartialCoverage = true;
     }
   }
   What.LowerBound = 0;
   What.UpperBound = ElemSize;
   What.DimList = std::move(DimList);
-  What.Kind = LocKind::Collapsed | (What.Kind & LocKind::Hint);
+  What.Kind = LocKind::Collapsed | (What.Kind & LocKind::Hint) | (What.Kind & LocKind::Auxiliary);
+  What.SE = SE;
+  What.AM = From.AM;
 }
 
 llvm::Optional<MemoryLocationRange> intersectScalar(
@@ -197,6 +281,7 @@ llvm::Optional<MemoryLocationRange> intersectScalar(
   if (LHS.UpperBound.getValue() > RHS.LowerBound.getValue() &&
       LHS.LowerBound.getValue() < RHS.UpperBound.getValue()) {
     MemoryLocationRange Int(LHS);
+    Int.Kind = LocKind::Default;
     Int.LowerBound = std::max(LHS.LowerBound.getValue(),
                               RHS.LowerBound.getValue());
     Int.UpperBound = std::min(LHS.UpperBound.getValue(),
@@ -217,6 +302,1073 @@ llvm::Optional<MemoryLocationRange> intersectScalar(
   }
   return llvm::None;
 }
+
+DimPairKind getDimPairKind(const Dimension &LHS, const Dimension &RHS) {
+  LLVM_DEBUG(
+    dbgs() << "[INTERSECT] Check the pair:\n";
+    LHS.print(dbgs() << "\t"); dbgs() << "\n";
+    RHS.print(dbgs() << "\t"); dbgs() << "\n";
+  );
+  auto LStartConst = isa<SCEVConstant>(LHS.Start);
+  auto LEndConst = isa<SCEVConstant>(LHS.End);
+  auto RStartConst = isa<SCEVConstant>(RHS.Start);
+  auto REndConst = isa<SCEVConstant>(RHS.End);
+  if (!LStartConst && !LEndConst && !RStartConst && !REndConst)
+    return DimPairKind::BothVariable;
+  if ((LStartConst && LEndConst && !RStartConst && !REndConst) ||
+      (!LStartConst && !LEndConst && RStartConst && REndConst))
+    return DimPairKind::OneConstOtherVariable;
+  if ((LStartConst && !LEndConst && !RStartConst && REndConst) ||
+     (RStartConst && !REndConst && !LStartConst && LEndConst))
+    return DimPairKind::OneStartOtherEndConst;
+  if (LStartConst && RStartConst && !LEndConst && !REndConst)
+    return DimPairKind::BothStartConst;
+  if (!LStartConst && !RStartConst && LEndConst && REndConst)
+    return DimPairKind::BothEndConst;
+  if ((LStartConst && LEndConst && (RStartConst ^ REndConst)) ||
+      (RStartConst && REndConst && (LStartConst ^ LEndConst)))
+    return DimPairKind::OneConstOtherSemiconst;
+  if ((!LStartConst && !LEndConst && (RStartConst ^ REndConst)) ||
+      (!RStartConst && !REndConst && (LStartConst ^ LEndConst)))
+    return DimPairKind::OneVariableOtherSemiconst;
+  if (LStartConst && LEndConst && RStartConst && REndConst)
+    return DimPairKind::BothConst;
+  return DimPairKind::Unknown;
+}
+
+struct IntersectVarInfo {
+  IntersectionResult UnknownIntersection;
+  IntersectionResult EmptyIntersection;
+  IntersectionResult TrueIntersection;
+  llvm::Optional<int64_t> CmpStart;
+  llvm::Optional<int64_t> CmpEnd;
+  llvm::Optional<int64_t> CmpLeftEndRightStart;
+  llvm::Optional<int64_t> CmpLeftStartRightEnd;
+  bool IsValidStep;
+};
+
+/// We can compare the bounds of the segments only if they can be represented
+/// as f(V) = V + C, where V is a variable expression and C is an integer
+/// constant. For the expression S representing one bound of the segment
+/// this function returns a pair consisting of an llvm::Value* of V and an
+/// integer value of C. If S does not have the form f(V), this function
+/// returns llvm::None.
+llvm::Optional<std::pair<Value *, int64_t>>
+parseBoundExpression(const llvm::SCEV *S) {
+  auto GetInnerSCEV = [](const SCEV *S) -> const SCEV* {
+    while (auto Cast{dyn_cast<SCEVCastExpr>(S)})
+      S = Cast->getOperand();
+    return S;
+  };
+  if (!isa<SCEVNAryExpr>(S)) {
+    if (isa<SCEVSignExtendExpr>(S) || isa<SCEVZeroExtendExpr>(S)) {
+      return parseBoundExpression(GetInnerSCEV(S));
+    }
+    if (auto *Unknown = dyn_cast<SCEVUnknown>(S))
+      return std::make_pair(Unknown->getValue(), int64_t(0));
+  }
+  auto *NAry = dyn_cast<SCEVNAryExpr>(S);
+  if (!NAry || NAry->getSCEVType() != llvm::SCEVTypes::scAddExpr ||
+      NAry->getNumOperands() != 2)
+    return llvm::None;
+  auto *S1 = NAry->getOperand(0);
+  auto *S2 = NAry->getOperand(1);
+  if (isa<SCEVSignExtendExpr>(S1) || isa<SCEVZeroExtendExpr>(S1))
+    S1 = GetInnerSCEV(S1);
+  if (isa<SCEVSignExtendExpr>(S2) || isa<SCEVZeroExtendExpr>(S2))
+    S2 = GetInnerSCEV(S2);
+  auto T1 = static_cast<SCEVTypes>(S1->getSCEVType());
+  auto T2 = static_cast<SCEVTypes>(S2->getSCEVType());
+  int64_t Constant = 0;
+  Value *Variable = nullptr;
+  if (T1 == SCEVTypes::scConstant && T2 == SCEVTypes::scUnknown) {
+    Constant = cast<SCEVConstant>(S1)->getAPInt().getSExtValue();
+    Variable = cast<SCEVUnknown>(S2)->getValue();
+  } else if (T2 == SCEVTypes::scConstant && T1 == SCEVTypes::scUnknown) {
+    Constant = cast<SCEVConstant>(S2)->getAPInt().getSExtValue();
+    Variable = cast<SCEVUnknown>(S1)->getValue();
+  } else {
+    return llvm::None;
+  }
+  assert(Variable && "Value must not be nullptr!");
+  return std::make_pair(Variable, Constant);
+}
+
+void shiftBounds(AssumptionBounds &AB, int64_t Offset) {
+  if (AB.Lower)
+    AB.Lower = *AB.Lower + Offset;
+  if (AB.Upper)
+    AB.Upper = *AB.Upper + Offset;
+}
+
+inline std::function<Dimension& (llvm::SmallVectorImpl<MemoryLocationRange> *)>
+getGrowFunction(const MemoryLocationRange &LeftRange, std::size_t DimIdx) {
+  assert(DimIdx < LeftRange.DimList.size() &&
+      "DimIdx must match the size of LeftRange.DimList!");
+  auto Lambda = [&LeftRange, DimIdx](
+    llvm::SmallVectorImpl<MemoryLocationRange> *C) -> Dimension & {
+    return C->emplace_back(LeftRange).DimList[DimIdx];
+  };
+  return Lambda;
+}
+
+IntersectionResult processBothVariable(const MemoryLocationRange &LeftRange,
+    std::size_t DimIdx, const Dimension &Right, const IntersectVarInfo &Info,
+    Dimension &Intersection, llvm::SmallVectorImpl<MemoryLocationRange> *LC,
+    llvm::SmallVectorImpl<MemoryLocationRange> *RC) {
+  auto Grow = getGrowFunction(LeftRange, DimIdx);
+  auto &Left = LeftRange.DimList[DimIdx];
+  auto SE = LeftRange.SE;
+  auto &CmpStart = Info.CmpStart;
+  auto &CmpEnd = Info.CmpEnd;
+  auto &CmpLSRE = Info.CmpLeftStartRightEnd;
+  auto &CmpLERS = Info.CmpLeftEndRightStart;
+  if (CmpLERS && *CmpLERS < 0 || CmpLSRE && *CmpLSRE > 0)
+    return Info.EmptyIntersection;
+  if (!CmpStart || !CmpEnd || !Info.IsValidStep)
+    return Info.UnknownIntersection;
+  if (CmpLERS && CmpLSRE && *CmpLERS >= 0 && *CmpLSRE <= 0) {
+    // The left dimension overlaps the right.
+    Intersection.Start = (*CmpStart) > 0 ? Left.Start : Right.Start;
+    Intersection.End = (*CmpEnd) < 0 ? Left.End : Right.End;
+    if (LC) {
+      if (*CmpStart < 0) {
+        auto &Dim = Grow(LC);
+        Dim.Start = Left.Start;
+        Dim.End = subtractOneFromSCEV(Right.Start, SE);
+      }
+      if (*CmpEnd > 0) {
+        auto &Dim = Grow(LC);
+        Dim.Start = addOneToSCEV(Right.End, SE);
+        Dim.End = Left.End;
+      }
+    }
+    if (RC) {
+      if (*CmpStart > 0) {
+        auto &Dim = Grow(RC);
+        Dim.Start = Right.Start;
+        Dim.End = subtractOneFromSCEV(Left.Start, SE);
+      }
+      if (*CmpEnd < 0) {
+        auto &Dim = Grow(RC);
+        Dim.Start = addOneToSCEV(Left.End, SE);
+        Dim.End = Right.End;
+      }
+    }
+  } else
+    return Info.UnknownIntersection;
+  return Info.TrueIntersection;
+}
+
+IntersectionResult processOneStartOtherEndConst(
+    const MemoryLocationRange &LeftRange, std::size_t DimIdx,
+    const Dimension &Right, Dimension &Intersection,
+    llvm::SmallVectorImpl<MemoryLocationRange> *LC,
+    llvm::SmallVectorImpl<MemoryLocationRange> *RC, IntersectVarInfo &Info) {
+  auto Grow = getGrowFunction(LeftRange, DimIdx);
+  auto &Left = LeftRange.DimList[DimIdx];
+  assert((isa<SCEVConstant>(Left.Start) && !isa<SCEVConstant>(Left.End) &&
+         !isa<SCEVConstant>(Right.Start) && isa<SCEVConstant>(Right.End)) ||
+         (isa<SCEVConstant>(Right.Start) && !isa<SCEVConstant>(Right.End) &&
+         !isa<SCEVConstant>(Left.Start) && isa<SCEVConstant>(Left.End)));
+  auto SE = LeftRange.SE;
+  auto *AM = LeftRange.AM;
+  // Let the First dimension be a dimension whose Start is constant and End
+  // is variable. We will denote the segments as follows:
+  // First = [m, N], Second = [P, q], where lowercase letters mean constants,
+  // and capital letters mean variables.
+  auto *First { &Left }, *Second { &Right };
+  auto *FC { LC }, *SC { RC };
+  auto &Cmpmq { Info.CmpLeftStartRightEnd },
+       &CmpNP { Info.CmpLeftEndRightStart };
+  if (!isa<SCEVConstant>(Left.Start)) {
+    std::swap(First, Second);
+    std::swap(FC, SC);
+    std::swap(Cmpmq, CmpNP);
+  }
+  assert(Cmpmq && "Constant bounds must be comparable!");
+  if (*Cmpmq > 0)
+    return Info.EmptyIntersection;
+  if (!CmpNP)
+    return Info.UnknownIntersection;
+  if (*CmpNP < 0)
+    return Info.EmptyIntersection;
+  if (!Info.IsValidStep)
+    return Info.UnknownIntersection;
+  // N >= P
+  auto *M = First->Start, *N = First->End;
+  auto *P = Second->Start, *Q = Second->End;
+  auto BN = parseBoundExpression(N);
+  auto BP = parseBoundExpression(P);
+  if (!BP || !BN || !AM)
+    return Info.UnknownIntersection;
+  auto BPItr = AM->find(BP->first);
+  auto BNItr = AM->find(BN->first);
+  if (BPItr == AM->end() || BNItr == AM->end())
+    return Info.UnknownIntersection;
+  auto BoundsP = BPItr->second;
+  auto BoundsN = BNItr->second;
+  shiftBounds(BoundsP, BP->second);
+  shiftBounds(BoundsN, BN->second);
+  auto MInt = cast<SCEVConstant>(M)->getAPInt().getSExtValue();
+  auto QInt = cast<SCEVConstant>(Q)->getAPInt().getSExtValue();
+  if (!BoundsN.Lower || !BoundsN.Upper || !BoundsP.Lower || !BoundsP.Upper)
+    return Info.UnknownIntersection;
+  if (MInt < *BoundsP.Lower) {
+    if (QInt > *BoundsN.Upper) {
+      Intersection.Start = P;
+      Intersection.End = N;
+      if (FC) {
+        // [m, P-1]
+        auto &Dim = Grow(FC);
+        Dim.Start = M;
+        Dim.End = subtractOneFromSCEV(P, SE);
+      }
+      if (SC) {
+        // [N+1, q]
+        auto &Dim = Grow(SC);
+        Dim.Start = addOneToSCEV(N, SE);
+        Dim.End = Q;
+      }
+    } else if (QInt < *BoundsN.Lower) {
+      Intersection = *Second;
+      if (FC) {
+        // [m, P-1], [q+1, N]
+        auto &Dim1 = Grow(FC);
+        Dim1.Start = M;
+        Dim1.End = subtractOneFromSCEV(P, SE);
+        auto &Dim2 = Grow(FC);
+        Dim2.Start = addOneToSCEV(Q, SE);
+        Dim2.End = N;
+      }
+    } else {
+      return Info.UnknownIntersection;
+    }
+  } else if (MInt <= *BoundsP.Lower && *BoundsN.Lower >= QInt) {
+    if (FC || SC)
+      return Info.UnknownIntersection;
+    Intersection = *Second;
+  } else if (MInt > *BoundsP.Upper) {
+    if (QInt < BoundsN.Lower) {
+      Intersection.Start = M;
+      Intersection.End = Q;
+      if (FC) {
+        // [P, m-1]
+        auto &Dim = Grow(FC);
+        Dim.Start = P;
+        Dim.End = subtractOneFromSCEV(M, SE);
+      }
+      if (SC) {
+        // [q+1, N]
+        auto &Dim = Grow(SC);
+        Dim.Start = addOneToSCEV(Q, SE);
+        Dim.End = N;
+      }
+    } else if (QInt > BoundsN.Upper) {
+      Intersection = *First;
+      if (SC) {
+        // [P, m-1], [N+1, q]
+        auto &Dim1 = Grow(SC);
+        Dim1.Start = P;
+        Dim1.End = subtractOneFromSCEV(M, SE);
+        auto &Dim2 = Grow(SC);
+        Dim2.Start = subtractOneFromSCEV(N, SE);
+        Dim2.End = Q;
+      }
+    } else {
+      return Info.UnknownIntersection;
+    }
+  } else if (MInt >= *BoundsP.Upper && BoundsN.Upper <= QInt) {
+    if (FC || SC)
+      return Info.UnknownIntersection;
+    Intersection = *First;
+  } else {
+    return Info.UnknownIntersection;
+  }
+  return Info.TrueIntersection;
+}
+
+IntersectionResult processBothStartConst(const MemoryLocationRange &LeftRange,
+    std::size_t DimIdx, const Dimension &Right, Dimension &Intersection,
+    llvm::SmallVectorImpl<MemoryLocationRange> *LC,
+    llvm::SmallVectorImpl<MemoryLocationRange> *RC, IntersectVarInfo &Info) {
+  auto Grow = getGrowFunction(LeftRange, DimIdx);
+  auto &Left = LeftRange.DimList[DimIdx];
+  assert(isa<SCEVConstant>(Left.Start) && !isa<SCEVConstant>(Left.End) &&
+         isa<SCEVConstant>(Right.Start) && !isa<SCEVConstant>(Right.End));
+  auto SE = LeftRange.SE;
+  auto *AM = LeftRange.AM;
+  // Let the First dimension be a dimension whose Start is less than the Start
+  // of the Second dimension. We will denote the segments as follows:
+  // First = [m, N], Second = [p, Q], where lowercase letters mean constants,
+  // and capital letters mean variables.
+  auto *First { &Left }, *Second { &Right };
+  auto *FC { LC }, *SC { RC };
+  auto CmpNQ { Info.CmpEnd };
+  if (cast<SCEVConstant>(Left.Start)->getAPInt().getSExtValue() >
+      cast<SCEVConstant>(Right.Start)->getAPInt().getSExtValue()) {
+    std::swap(First, Second);
+    std::swap(FC, SC);
+    if (CmpNQ)
+      *CmpNQ = -(*CmpNQ);
+  }
+  auto *M = First->Start, *N = First->End;
+  auto *P = Second->Start, *Q = Second->End;
+  auto MInt = cast<SCEVConstant>(M)->getAPInt().getSExtValue();
+  auto PInt = cast<SCEVConstant>(P)->getAPInt().getSExtValue();
+  if (!CmpNQ)
+    return Info.UnknownIntersection;
+  if (MInt == PInt) {
+    // [m, min(N, Q)]
+    Intersection.Start = M;
+    Intersection.End = *CmpNQ > 0 ? Q : N;
+    if (FC && *CmpNQ > 0) {
+      // [Q+1, N]
+      auto &Dim = Grow(FC);
+      Dim.Start = addOneToSCEV(Q, SE);
+      Dim.End = N;
+    }
+    if (SC && *CmpNQ < 0) {
+      // [N+1, Q]
+      auto &Dim = Grow(SC);
+      Dim.Start = addOneToSCEV(N, SE);
+      Dim.End = Q;
+    }
+  } else {
+    if (N == Q) {
+      // [max(m, p), N]
+      Intersection.Start = MInt > PInt ? M : P;
+      Intersection.End = N;
+      if (FC && MInt < PInt) {
+        // [m, p-1]
+        auto &Dim = Grow(FC);
+        Dim.Start = M;
+        Dim.End = subtractOneFromSCEV(P, SE);
+      }
+      if (SC && MInt > PInt)
+        llvm_unreachable("M must be less than or equal to P!");
+    } else {
+      auto BN = parseBoundExpression(N);
+      auto BQ = parseBoundExpression(Q);
+      if (!BN || !BQ || !AM)
+        return Info.UnknownIntersection;
+      auto BNItr = AM->find(BN->first);
+      auto BQItr = AM->find(BQ->first);
+      if (BNItr == AM->end() || BQItr == AM->end())
+        return Info.UnknownIntersection;
+      auto BoundsN = BNItr->second;
+      auto BoundsQ = BQItr->second;
+      shiftBounds(BoundsN, BN->second);
+      shiftBounds(BoundsQ, BN->second);
+      if (BoundsN.Upper && PInt > *BoundsN.Upper) {
+        return Info.EmptyIntersection;
+      } else if (BoundsN.Lower && PInt <= *BoundsN.Lower) {
+        // [max(m, p), min(N, Q)]
+        Intersection.Start = MInt > PInt ? M : P;
+        Intersection.End = *CmpNQ < 0 ? N : Q;
+        if (FC && MInt < PInt) {
+          // [m, p-1]
+          auto &Dim = Grow(FC);
+          Dim.Start = M;
+          Dim.End = subtractOneFromSCEV(P, SE);
+        }
+        if (SC && *CmpNQ < 0) {
+          // [N+1, Q]
+          auto &Dim = Grow(SC);
+          Dim.Start = addOneToSCEV(N, SE);
+          Dim.End = Q;
+        }
+      } else {
+        return Info.UnknownIntersection;
+      }
+    }
+  }
+  return Info.TrueIntersection;
+}
+
+IntersectionResult processBothEndConst(const MemoryLocationRange &LeftRange,
+    std::size_t DimIdx, const Dimension &Right, Dimension &Intersection,
+    llvm::SmallVectorImpl<MemoryLocationRange> *LC,
+    llvm::SmallVectorImpl<MemoryLocationRange> *RC, IntersectVarInfo &Info) {
+  auto Grow = getGrowFunction(LeftRange, DimIdx);
+  auto &Left = LeftRange.DimList[DimIdx];
+  assert(!isa<SCEVConstant>(Left.Start) && isa<SCEVConstant>(Left.End) &&
+         !isa<SCEVConstant>(Right.Start) && isa<SCEVConstant>(Right.End));
+  auto SE = LeftRange.SE;
+  auto *AM = LeftRange.AM;
+  // Let the First dimension be a dimension whose End is less than the End
+  // of the Second dimension. We will denote the segments as follows:
+  // First = [M, n], Second = [P, q], where lowercase letters mean constants,
+  // and capital letters mean variables.
+  auto *First { &Left }, *Second { &Right };
+  auto *FC { LC }, *SC { RC };
+  auto CmpMP { Info.CmpEnd };
+  if (cast<SCEVConstant>(Left.End)->getAPInt().getSExtValue() >
+      cast<SCEVConstant>(Right.End)->getAPInt().getSExtValue()) {
+    std::swap(First, Second);
+    std::swap(FC, SC);
+    if (CmpMP)
+      *CmpMP = -(*CmpMP);
+  }
+  auto *M = First->Start, *N = First->End;
+  auto *P = Second->Start, *Q = Second->End;
+  auto NInt = cast<SCEVConstant>(N)->getAPInt().getSExtValue();
+  auto QInt = cast<SCEVConstant>(Q)->getAPInt().getSExtValue();
+  if (!CmpMP)
+    return Info.UnknownIntersection;
+  if (NInt == QInt) {
+    // [max(M, P), n]
+    Intersection.Start = *CmpMP > 0 ? M : P;
+    Intersection.End = N;
+    if (FC && *CmpMP < 0) {
+      // [M, P-1]
+      auto &Dim = Grow(FC);
+      Dim.Start = M;
+      Dim.End = subtractOneFromSCEV(P, SE);
+    }
+    if (SC && *CmpMP > 0) {
+      // [P+1, M]
+      auto &Dim = Grow(SC);
+      Dim.Start = addOneToSCEV(P, SE);
+      Dim.End = M;
+    }
+  } else {
+    if (M == P) {
+      // [M, min(n, q)]
+      Intersection.Start = M;
+      Intersection.End = NInt < QInt ? N : Q;
+      if (FC && NInt > QInt)
+        llvm_unreachable("N must be less than or equal to Q!");
+      if (SC && QInt > NInt) {
+        // [n+1, q]
+        auto &Dim = Grow(SC);
+        Dim.Start = addOneToSCEV(N, SE);
+        Dim.End = Q;
+      }
+    } else {
+      auto BM = parseBoundExpression(M);
+      auto BP = parseBoundExpression(P);
+      if (!BM || !BP || !AM)
+        return Info.UnknownIntersection;
+      auto BMItr = AM->find(BM->first);
+      auto BPItr = AM->find(BP->first);
+      if (BMItr == AM->end() || BPItr == AM->end())
+        return Info.UnknownIntersection;
+      auto BoundsM = BMItr->second;
+      auto BoundsP = BPItr->second;
+      shiftBounds(BoundsM, BM->second);
+      shiftBounds(BoundsP, BP->second);
+      if (BoundsM.Lower && QInt < *BoundsM.Lower) {
+        return Info.EmptyIntersection;
+      } else if (BoundsM.Upper && QInt >= *BoundsM.Upper) {
+        // [max(M, P), min(n, q)]
+        Intersection.Start = *CmpMP > 0 ? M : P;
+        Intersection.End = NInt < QInt ? N : Q;
+        if (FC && *CmpMP < 0) {
+          // [M, P-1]
+          auto &Dim = Grow(FC);
+          Dim.Start = M;
+          Dim.End = subtractOneFromSCEV(P, SE);
+        }
+        if (SC && NInt < QInt) {
+          // [N+1, Q]
+          auto &Dim = Grow(SC);
+          Dim.Start = addOneToSCEV(N, SE);
+          Dim.End = Q;
+        }
+      } else {
+        return Info.UnknownIntersection;
+      }
+    }
+  }
+  return Info.TrueIntersection;
+}
+
+IntersectionResult processOneConstOtherSemiconst(
+    const MemoryLocationRange &LeftRange, std::size_t DimIdx,
+    const Dimension &Right, Dimension &Intersection,
+    llvm::SmallVectorImpl<MemoryLocationRange> *LC,
+    llvm::SmallVectorImpl<MemoryLocationRange> *RC, IntersectVarInfo &Info) {
+  auto Grow = getGrowFunction(LeftRange, DimIdx);
+  auto &Left = LeftRange.DimList[DimIdx];
+  assert((isa<SCEVConstant>(Left.Start) && isa<SCEVConstant>(Left.End) &&
+         (isa<SCEVConstant>(Right.Start) ^ isa<SCEVConstant>(Right.End))) ||
+         (isa<SCEVConstant>(Right.Start) && isa<SCEVConstant>(Right.End) &&
+         (isa<SCEVConstant>(Left.Start) ^ isa<SCEVConstant>(Left.End))));
+  auto SE = LeftRange.SE;
+  auto *AM = LeftRange.AM;
+  // Let the First dimension be a dimension whose Start and End are constant.
+  // We will denote the segments as follows: First = [m, n], Second = [p, Q]
+  // (or [P, q]), where lowercase letters mean constants, and capital letters
+  // mean variables.
+  auto *First { &Left }, *Second { &Right };
+  auto *FC { LC }, *SC { RC };
+  if (isa<SCEVConstant>(Left.Start) ^ isa<SCEVConstant>(Left.End)) {
+    std::swap(First, Second);
+    std::swap(FC, SC);
+  }
+  auto *M = First->Start, *N = First->End;
+  auto *P = Second->Start, *Q = Second->End;
+  auto MInt = cast<SCEVConstant>(M)->getAPInt().getSExtValue();
+  auto NInt = cast<SCEVConstant>(N)->getAPInt().getSExtValue();
+  auto BP = parseBoundExpression(P);
+  auto BQ = parseBoundExpression(Q);
+  if (isa<SCEVConstant>(P)) {
+    auto PInt = cast<SCEVConstant>(P)->getAPInt().getSExtValue();
+    if (PInt > NInt)
+      return Info.EmptyIntersection;
+    if (!BQ || !AM)
+      return Info.UnknownIntersection;
+    auto BQItr = AM->find(BQ->first);
+    if (BQItr == AM->end())
+      return Info.UnknownIntersection;
+    auto BoundsQ = BQItr->second;
+    shiftBounds(BoundsQ, BQ->second);
+    if (BoundsQ.Lower && NInt < *BoundsQ.Lower) {
+      // [max(m, p), n]
+      Intersection.Start = MInt > PInt ? M : P;
+      Intersection.End = N;
+      if (FC && MInt < PInt) {
+        // [m, p-1]
+        auto &Dim = Grow(FC);
+        Dim.Start = M;
+        Dim.End = subtractOneFromSCEV(P, SE);
+      }
+      if (SC) {
+        // [n+1, Q]
+        auto &Dim1 = Grow(SC);
+        Dim1.Start = addOneToSCEV(N, SE);
+        Dim1.End = Q;
+        if (PInt < MInt) {
+          // [p, m-1]
+          auto &Dim2 = Grow(SC);
+          Dim2.Start = P;
+          Dim2.End = subtractOneFromSCEV(M, SE);
+        }
+      }
+    } else if (BoundsQ.Upper) {
+      if (*BoundsQ.Upper < MInt)
+        return Info.EmptyIntersection;
+      if (NInt > BoundsQ.Upper) {
+        // [max(m, p), Q]
+        Intersection.Start = MInt > PInt ? M : P;
+        Intersection.End = Q;
+        if (FC) {
+          // [Q+1, n]
+          auto &Dim1 = Grow(FC);
+          Dim1.Start = addOneToSCEV(Q, SE);
+          Dim1.End = N;
+          if (MInt < PInt) {
+            // [m, p-1]
+            auto &Dim2 = Grow(FC);
+            Dim2.Start = M;
+            Dim2.End = subtractOneFromSCEV(P, SE);
+          }
+        }
+        if (SC && PInt < MInt) {
+          // [p, m-1]
+          auto &Dim = Grow(SC);
+          Dim.Start = P;
+          Dim.End = subtractOneFromSCEV(M, SE);
+        }
+      } else {
+        return Info.UnknownIntersection;
+      }
+    } else {
+      return Info.UnknownIntersection;
+    }
+  } else {
+    auto QInt = cast<SCEVConstant>(Q)->getAPInt().getSExtValue();
+    if (MInt > QInt)
+      return Info.EmptyIntersection;
+    if (!BP || !AM)
+      return Info.UnknownIntersection;
+    auto BPItr = AM->find(BP->first);
+    if (BPItr == AM->end())
+      return Info.UnknownIntersection;
+    auto BoundsP = BPItr->second;
+    shiftBounds(BoundsP, BP->second);
+    if (BoundsP.Upper && MInt > *BoundsP.Upper) {
+      // [m, min(n, q)]
+      Intersection.Start = M;
+      Intersection.End = NInt < QInt ? N : Q;
+      if (FC && NInt > QInt) {
+        // [q+1, n]
+        auto &Dim = Grow(FC);
+        Dim.Start = addOneToSCEV(Q, SE);
+        Dim.End = N;
+      }
+      if (SC) {
+        // [P, m-1]
+        auto &Dim1 = Grow(SC);
+        Dim1.Start = P;
+        Dim1.End = subtractOneFromSCEV(M, SE);
+        if (QInt > NInt) {
+          // [n+1, q]
+          auto &Dim2 = Grow(SC);
+          Dim2.Start = addOneToSCEV(N, SE);
+          Dim2.End = Q;
+        }
+      }
+    } else if (BoundsP.Lower) {
+      if (*BoundsP.Lower > NInt)
+        return Info.EmptyIntersection;
+      if (MInt < BoundsP.Lower) {
+        // [P, min(n, q)]
+        Intersection.Start = P;
+        Intersection.End = NInt < QInt ? N : Q;
+        if (FC) {
+          // [m, P-1]
+          auto &Dim1 = Grow(FC);
+          Dim1.Start = M;
+          Dim1.End = subtractOneFromSCEV(P, SE);
+          if (NInt > QInt) {
+            // [q+1, n]
+            auto &Dim2 = Grow(FC);
+            Dim2.Start = addOneToSCEV(Q, SE);
+            Dim2.End = N;
+          }
+        }
+        if (SC && QInt > NInt) {
+          // [n+1, q]
+          auto &Dim = Grow(SC);
+          Dim.Start = addOneToSCEV(N, SE);
+          Dim.End = Q;
+        }
+      } else {
+        return Info.UnknownIntersection;
+      }
+    } else {
+      return Info.UnknownIntersection;
+    }
+  }
+  return Info.TrueIntersection;
+}
+
+IntersectionResult processOneVariableOtherSemiconst(
+    const MemoryLocationRange &LeftRange, std::size_t DimIdx,
+    const Dimension &Right, Dimension &Intersection,
+    llvm::SmallVectorImpl<MemoryLocationRange> *LC,
+    llvm::SmallVectorImpl<MemoryLocationRange> *RC, IntersectVarInfo &Info) {
+  auto Grow = getGrowFunction(LeftRange, DimIdx);
+  auto &Left = LeftRange.DimList[DimIdx];
+  assert((!isa<SCEVConstant>(Left.Start) && !isa<SCEVConstant>(Left.End) &&
+         (isa<SCEVConstant>(Right.Start) ^ isa<SCEVConstant>(Right.End))) ||
+         (!isa<SCEVConstant>(Right.Start) && !isa<SCEVConstant>(Right.End) &&
+         (isa<SCEVConstant>(Left.Start) ^ isa<SCEVConstant>(Left.End))));
+  auto SE = LeftRange.SE;
+  auto *AM = LeftRange.AM;
+  // Let the First dimension be a dimension whose Start and End are variable.
+  // We will denote the segments as follows: First = [M, N], Second = [p, Q]
+  // (or [P, q]), where lowercase letters mean constants, and capital letters
+  // mean variables.
+  auto *First { &Left }, *Second { &Right };
+  auto *FC { LC }, *SC { RC };
+  auto &CmpMQ = Info.CmpLeftStartRightEnd;
+  auto &CmpNQ = Info.CmpEnd;
+  auto &CmpMP = Info.CmpStart;
+  auto &CmpNP = Info.CmpLeftEndRightStart;
+  if (isa<SCEVConstant>(Left.Start) || isa<SCEVConstant>(Left.End)) {
+    std::swap(First, Second);
+    std::swap(FC, SC);
+    if (CmpMQ)
+      *CmpMQ = -(*CmpMQ);
+    if (CmpNQ)
+      *CmpNQ = -(*CmpNQ);
+    if (CmpMP)
+      *CmpMP = -(*CmpMP);
+    if (CmpNP)
+      *CmpNP = -(*CmpNP);
+  }
+  auto *M = First->Start, *N = First->End;
+  auto *P = Second->Start, *Q = Second->End;
+  auto BM = parseBoundExpression(M);
+  auto BN = parseBoundExpression(N);
+  if (!BM || !BN || !AM)
+      return Info.UnknownIntersection;
+  auto BMItr = AM->find(BM->first);
+  auto BNItr = AM->find(BN->first);
+  if (BMItr == AM->end() || BNItr == AM->end())
+    return Info.UnknownIntersection;
+  auto BoundsM = BMItr->second;
+  auto BoundsN = BNItr->second;
+  shiftBounds(BoundsM, BM->second);
+  shiftBounds(BoundsN, BN->second);
+  if (isa<SCEVConstant>(P)) {
+    auto PInt = cast<SCEVConstant>(P)->getAPInt().getSExtValue();
+    auto BQ = parseBoundExpression(Q);
+    if (!BQ)
+      return Info.UnknownIntersection;
+    auto BQItr = AM->find(BQ->first);
+    if (BQItr == AM->end())
+      return Info.UnknownIntersection;
+    auto BoundsQ = BQItr->second;
+    shiftBounds(BoundsQ, BQ->second);
+    if (BoundsN.Upper && *BoundsN.Upper < PInt ||
+        BoundsQ.Upper && BoundsM.Lower && *BoundsQ.Upper < *BoundsM.Lower ||
+        CmpMQ && *CmpMQ > 0)
+      return Info.EmptyIntersection;
+    if (BoundsM.Upper && PInt > *BoundsM.Upper) {
+      if (BoundsQ.Upper && BoundsN.Lower && *BoundsQ.Upper < *BoundsN.Lower ||
+          CmpNQ && *CmpNQ > 0) {
+        // [p, Q]
+        Intersection.Start = P;
+        Intersection.End = Q;
+        if (FC) {
+          // [M, p-1]
+          auto &Dim1 = Grow(FC);
+          Dim1.Start = M;
+          Dim1.End = subtractOneFromSCEV(P, SE);
+          // [Q+1, N]
+          auto &Dim2 = Grow(FC);
+          Dim2.Start = addOneToSCEV(Q, SE);
+          Dim2.End = N;
+        }
+      } else if (BoundsN.Upper && BoundsQ.Lower &&
+                 *BoundsN.Upper < *BoundsQ.Lower ||
+                 CmpNQ && *CmpNQ < 0) {
+        // [p, N]
+        Intersection.Start = P;
+        Intersection.End = N;
+        if (FC) {
+          // [M, p-1]
+          auto &Dim = Grow(FC);
+          Dim.Start = M;
+          Dim.End = subtractOneFromSCEV(P, SE);
+        }
+        if (SC) {
+          // [N+1, Q]
+          auto &Dim = Grow(SC);
+          Dim.Start = addOneToSCEV(N, SE);
+          Dim.End = Q;
+        }
+      } else {
+        return Info.UnknownIntersection;
+      }
+    } else if (BoundsM.Lower && PInt < *BoundsM.Lower) {
+      if (BoundsQ.Upper && BoundsN.Lower && *BoundsQ.Upper < *BoundsN.Lower ||
+          CmpNQ && *CmpNQ > 0) {
+        // [M, Q]
+        Intersection.Start = M;
+        Intersection.End = Q;
+        if (FC) {
+          // [Q+1, N]
+          auto &Dim = Grow(FC);
+          Dim.Start = addOneToSCEV(Q, SE);
+          Dim.End = N;
+        }
+        if (SC) {
+          // [p, M-1]
+          auto &Dim = Grow(SC);
+          Dim.Start = P;
+          Dim.End = subtractOneFromSCEV(M, SE);
+        }
+      } else if (BoundsN.Upper && BoundsQ.Lower &&
+                 *BoundsN.Upper < *BoundsQ.Lower ||
+                 CmpNQ && *CmpNQ < 0) {
+        Intersection.Start = M;
+        Intersection.End = N;
+        if (SC) {
+          // [p, M-1]
+          auto &Dim1 = Grow(SC);
+          Dim1.Start = P;
+          Dim1.End = subtractOneFromSCEV(M, SE);
+          // [N+1, Q]
+          auto &Dim2 = Grow(SC);
+          Dim2.Start = addOneToSCEV(N, SE);
+          Dim2.End = Q;
+        }
+      } else if (CmpNQ && *CmpNQ <= 0) {
+        Intersection.Start = M;
+        Intersection.End = N;
+        if (SC) {
+          // [p, M-1]
+          auto &Dim1 = Grow(SC);
+          Dim1.Start = P;
+          Dim1.End = subtractOneFromSCEV(M, SE);
+          if (*CmpNQ < 0) {
+            // [N+1, Q]
+            auto &Dim2 = Grow(SC);
+            Dim2.Start = addOneToSCEV(N, SE);
+            Dim2.End = Q;
+          }
+        }
+      } else {
+        return Info.UnknownIntersection;
+      }
+    } else {
+      return Info.UnknownIntersection;
+    }
+  } else {
+    auto QInt = cast<SCEVConstant>(Q)->getAPInt().getSExtValue();
+    auto BP = parseBoundExpression(P);
+    if (!BP)
+      return Info.UnknownIntersection;
+    auto BPItr = AM->find(BP->first);
+    if (BPItr == AM->end())
+      return Info.UnknownIntersection;
+    auto BoundsP = BPItr->second;
+    shiftBounds(BoundsP, BP->second);
+    if (BoundsM.Lower && *BoundsM.Lower > QInt ||
+        BoundsP.Lower && BoundsN.Upper && *BoundsP.Lower > *BoundsN.Upper ||
+        CmpNP && *CmpNP < 0)
+      return Info.EmptyIntersection;
+    if (BoundsM.Upper && BoundsP.Lower && *BoundsP.Lower > *BoundsM.Upper ||
+        CmpMP && *CmpMP < 0) {
+      if (BoundsN.Lower && QInt < *BoundsN.Lower) {
+        // [p, Q]
+        Intersection.Start = P;
+        Intersection.End = Q;
+        if (FC) {
+          // [M, p-1]
+          auto &Dim1 = Grow(FC);
+          Dim1.Start = M;
+          Dim1.End = subtractOneFromSCEV(P, SE);
+          // [Q+1, N]
+          auto &Dim2 = Grow(FC);
+          Dim2.Start = addOneToSCEV(Q, SE);
+          Dim2.End = N;
+        }
+      } else if (BoundsN.Upper && *BoundsN.Upper < QInt) {
+        // [p, N]
+        Intersection.Start = P;
+        Intersection.End = N;
+        if (FC) {
+          // [M, p-1]
+          auto &Dim = Grow(FC);
+          Dim.Start = M;
+          Dim.End = subtractOneFromSCEV(P, SE);
+        }
+        if (SC) {
+          // [N+1, Q]
+          auto &Dim = Grow(SC);
+          Dim.Start = addOneToSCEV(N, SE);
+          Dim.End = Q;
+        }
+      } else {
+        return Info.UnknownIntersection;
+      }
+    } else if (BoundsM.Lower && BoundsP.Upper &&
+               *BoundsP.Upper < *BoundsM.Lower ||
+               CmpMP && *CmpMP > 0) {
+      if (BoundsN.Lower && QInt < *BoundsN.Lower) {
+        // [M, Q]
+        Intersection.Start = M;
+        Intersection.End = Q;
+        if (FC) {
+          // [Q+1, N]
+          auto &Dim = Grow(FC);
+          Dim.Start = addOneToSCEV(Q, SE);
+          Dim.End = N;
+        }
+        if (SC) {
+          // [p, M-1]
+          auto &Dim = Grow(SC);
+          Dim.Start = P;
+          Dim.End = subtractOneFromSCEV(M, SE);
+        }
+      } else if (BoundsN.Upper && *BoundsN.Upper < QInt) {
+        Intersection.Start = M;
+        Intersection.End = N;
+        if (SC) {
+          // [p, M-1]
+          auto &Dim1 = Grow(SC);
+          Dim1.Start = P;
+          Dim1.End = subtractOneFromSCEV(M, SE);
+          // [N+1, Q]
+          auto &Dim2 = Grow(SC);
+          Dim2.Start = addOneToSCEV(N, SE);
+          Dim2.End = Q;
+        }
+      } else {
+        return Info.UnknownIntersection;
+      }
+    } else {
+      return Info.UnknownIntersection;
+    }
+  }
+  return Info.TrueIntersection;
+}
+
+IntersectionResult processOneConstOtherVariable(
+    const MemoryLocationRange &LeftRange, std::size_t DimIdx,
+    const Dimension &Right, Dimension &Intersection,
+    llvm::SmallVectorImpl<MemoryLocationRange> *LC,
+    llvm::SmallVectorImpl<MemoryLocationRange> *RC, IntersectVarInfo &Info) {
+  auto Grow = getGrowFunction(LeftRange, DimIdx);
+  auto &Left = LeftRange.DimList[DimIdx];
+  assert(isa<SCEVConstant>(Left.Start) && isa<SCEVConstant>(Left.End) &&
+        !isa<SCEVConstant>(Right.Start) && !isa<SCEVConstant>(Right.End) ||
+         isa<SCEVConstant>(Right.Start) && isa<SCEVConstant>(Right.End) &&
+        !isa<SCEVConstant>(Left.Start) && !isa<SCEVConstant>(Left.End));
+  auto SE = LeftRange.SE;
+  auto *AM = LeftRange.AM;
+  // Let the First dimension be a dimension whose Start and End are constant.
+  // We will denote the segments as follows: First = [m, n], Second = [P, Q]
+  // where lowercase letters mean constants, and capital letter mean
+  // variables.
+  auto *First { &Left }, *Second { &Right };
+  auto *FC { LC }, *SC { RC };
+  if (!isa<SCEVConstant>(Left.Start)) {
+    std::swap(First, Second);
+    std::swap(FC, SC);
+  }
+  auto *M = First->Start, *N = First->End;
+  auto *P = Second->Start, *Q = Second->End;
+  auto BP = parseBoundExpression(P);
+  auto BQ = parseBoundExpression(Q);
+  if (!BP || !BQ || !AM)
+      return Info.UnknownIntersection;
+  auto BPItr = AM->find(BP->first);
+  auto BQItr = AM->find(BQ->first);
+  if (BPItr == AM->end() || BQItr == AM->end())
+    return Info.UnknownIntersection;
+  auto BoundsP = BPItr->second;
+  auto BoundsQ = BQItr->second;
+  shiftBounds(BoundsP, BP->second);
+  shiftBounds(BoundsQ, BQ->second);
+  auto MInt = cast<SCEVConstant>(M)->getAPInt().getSExtValue();
+  auto NInt = cast<SCEVConstant>(N)->getAPInt().getSExtValue();
+  if (BoundsQ.Upper && *BoundsQ.Upper < MInt ||
+      BoundsP.Lower && *BoundsP.Lower > NInt)
+    return Info.EmptyIntersection;
+  if (BoundsP.Lower && MInt < *BoundsP.Lower) {
+    if (BoundsQ.Upper && *BoundsQ.Upper < NInt) {
+      // [P, Q]
+      Intersection.Start = P;
+      Intersection.End = Q;
+      if (FC) {
+        // [m, P-1]
+        auto &Dim1 = Grow(FC);
+        Dim1.Start = M;
+        Dim1.End = subtractOneFromSCEV(P, SE);
+        // [Q+1, n]
+        auto &Dim2 = Grow(FC);
+        Dim2.Start = addOneToSCEV(Q, SE);
+        Dim2.End = N;
+      }
+    } else if (BoundsQ.Lower && *BoundsQ.Lower > NInt) {
+      // [P, n]
+      Intersection.Start = P;
+      Intersection.End = N;
+      if (FC) {
+        // [m, P-1]
+        auto &Dim = Grow(FC);
+        Dim.Start = M;
+        Dim.End = subtractOneFromSCEV(P, SE);
+      }
+      if (SC) {
+        // [n+1, Q]
+        auto &Dim = Grow(SC);
+        Dim.Start = addOneToSCEV(N, SE);
+        Dim.End = Q;
+      }
+    } else {
+      return Info.UnknownIntersection;
+    }
+  } else if (BoundsP.Upper && MInt > *BoundsP.Upper) {
+    if (BoundsQ.Upper && *BoundsQ.Upper < NInt) {
+      // [m, Q]
+      Intersection.Start = M;
+      Intersection.End = Q;
+      if (FC) {
+        // [Q+1, n]
+        auto &Dim = Grow(FC);
+        Dim.Start = addOneToSCEV(Q, SE);
+        Dim.End = N;
+      }
+      if (SC) {
+        // [P, m-1]
+        auto &Dim = Grow(SC);
+        Dim.Start = P;
+        Dim.End = subtractOneFromSCEV(M, SE);
+      }
+    } else if (BoundsQ.Lower && *BoundsQ.Lower > NInt) {
+        Intersection.Start = M;
+        Intersection.End = N;
+        if (SC) {
+          // [P, m-1]
+          auto &Dim1 = Grow(SC);
+          Dim1.Start = P;
+          Dim1.End = subtractOneFromSCEV(M, SE);
+          // [n+1, Q]
+          auto &Dim2 = Grow(SC);
+          Dim2.Start = addOneToSCEV(N, SE);
+          Dim2.End = Q;
+        }
+    } else {
+      return Info.UnknownIntersection;
+    }
+  } else {
+    return Info.UnknownIntersection;
+  }
+  return Info.TrueIntersection;
+}
+
+/// \brief Intersects dimensions where at least one dimension has a variable 
+/// bound.
+///
+/// \param [in] LeftRange A full MemoryLocationRange for the first dimension 
+/// to intersect. This dimension is stored in `LeftRange.DimList[DimIdx].`
+/// \param [in] DimIdx The index of the first dimension to intersect (described 
+/// above).
+/// \param [in] Right The second dimension to intersect.
+/// \param [in] PairKind A kind of the pair of dimensions.
+/// \param [out] Intersection The result of intersection.
+/// \param [out] LC List of memory locations to store the difference 
+/// between locations LeftRange[DimIdx] and Intersection. It will not be 
+/// changed if the intersection is empty. If `LC == nullptr`, the difference 
+/// will not be calculated and will not be stored anywhere.
+/// \param [out] RC List of memory locations to store the difference 
+/// between locations Right and Intersection. It will not be changed if the 
+/// intersection is empty. If `RC == nullptr`, the difference will not be 
+/// calculated and will not be stored anywhere.
+/// \return A pair of an optional MemoryLocationRange and a flag. The 
+/// MemoryLocationRange is set to default if the intersection is unknown and
+/// is set to `None` if the intersection is empty. The flag is set to `false` if
+/// the intersection is neither empty or unknown (and the real intersection is
+/// stored in `Intersection`) and is set to `true` otherwise.
+IntersectionResult intersectVarDims(const MemoryLocationRange &LeftRange,
+    std::size_t DimIdx, const Dimension &Right, DimPairKind PairKind,
+    Dimension &Intersection, llvm::SmallVectorImpl<MemoryLocationRange> *LC,
+    llvm::SmallVectorImpl<MemoryLocationRange> *RC) {
+  IntersectVarInfo Info;
+  auto &Left = LeftRange.DimList[DimIdx];
+  Info.UnknownIntersection = std::make_pair(MemoryLocationRange(), true);
+  Info.EmptyIntersection = std::make_pair(llvm::None, true);
+  Info.TrueIntersection = std::make_pair(llvm::None, false);
+  Info.IsValidStep = Left.Step == Right.Step && isa<SCEVConstant>(Left.Step) &&
+      cast<SCEVConstant>(Left.Step)->getAPInt().getSExtValue() == 1;
+  Info.CmpStart = compareSCEVs(Left.Start, Right.Start, LeftRange.SE);
+  Info.CmpEnd = compareSCEVs(Left.End, Right.End, LeftRange.SE);
+  Info.CmpLeftEndRightStart = compareSCEVs(Left.End, Right.Start, LeftRange.SE);
+  Info.CmpLeftStartRightEnd = compareSCEVs(Left.Start, Right.End, LeftRange.SE);
+  switch (PairKind) {
+  case DimPairKind::BothVariable:
+    return processBothVariable(LeftRange, DimIdx, Right, Info, Intersection,
+                               LC, RC);
+  case DimPairKind::OneStartOtherEndConst:
+    return processOneStartOtherEndConst(LeftRange, DimIdx, Right,
+                                        Intersection, LC, RC, Info);
+  case DimPairKind::BothStartConst:
+    return processBothStartConst(LeftRange, DimIdx, Right, Intersection, LC,
+                                 RC, Info);
+  case DimPairKind::BothEndConst:
+    return processBothEndConst(LeftRange, DimIdx, Right, Intersection, LC, RC,
+                               Info);
+  case DimPairKind::OneConstOtherSemiconst:
+    return processOneConstOtherSemiconst(LeftRange, DimIdx, Right,
+                                         Intersection, LC, RC, Info);
+  case DimPairKind::OneVariableOtherSemiconst:
+    return processOneVariableOtherSemiconst(LeftRange, DimIdx, Right,
+                                            Intersection, LC, RC, Info);
+  case DimPairKind::OneConstOtherVariable:
+    return processOneConstOtherVariable(LeftRange, DimIdx, Right,
+                                        Intersection, LC, RC, Info);
+  default:
+    llvm_unreachable("Invalid kind of dimension with variable bounds.");
+  }
+}
 };
 
 namespace tsar {
@@ -232,7 +1384,7 @@ llvm::Optional<MemoryLocationRange> intersect(
   typedef std::pair<ValueT, ValueT> VarRange;
   typedef MemoryLocationRange::LocKind LocKind;
   assert(LHS.Ptr && RHS.Ptr &&
-      "Pointers of intersected memory locations must not be null!");
+         "Pointers of intersected memory locations must not be null!");
   // Return a location that may be an intersection, but cannot be calculated 
   // exactly.
   LLVM_DEBUG(
@@ -262,23 +1414,43 @@ llvm::Optional<MemoryLocationRange> intersect(
       LHS.DimList == RHS.DimList)
     return LHS;
   MemoryLocationRange Int(LHS);
+  assert(LHS.SE && RHS.SE && "ScalarEvolution must be specified!");
+  assert(LHS.SE == RHS.SE
+         && "ScalarEvolution must be common for memory locations!");
+  auto SE = LHS.SE;
   for (std::size_t I = 0; I < LHS.DimList.size(); ++I) {
     auto &Left = LHS.DimList[I];
     auto &Right = RHS.DimList[I];
-    if (Left.DimSize != Right.DimSize)
+    if (Left.DimSize != Right.DimSize &&
+       !(LHS.DimList.size() == 1 && Left.DimSize ^ Right.DimSize))
       return MemoryLocationRange();
-    auto LeftEnd = Left.Start + Left.Step * (Left.TripCount - 1);
-    auto RightEnd = Right.Start + Right.Step * (Right.TripCount - 1);
-    if (LeftEnd < Right.Start || RightEnd < Left.Start)
+    auto &Intersection = Int.DimList[I];
+    auto PairKind = getDimPairKind(Left, Right);
+    LLVM_DEBUG(dbgs() << "[INTERSECT] Pair kind: " <<
+               getKindAsString(PairKind) << "\n");
+    if (PairKind != DimPairKind::BothConst) {
+      auto Res = intersectVarDims(LHS, I, Right, PairKind, Intersection, LC, RC);
+      if (Res.second)
+        return Res.first;
+      continue;
+    }
+    auto LeftStart = cast<SCEVConstant>(Left.Start)->getValue()->getZExtValue();
+    auto LeftEnd = cast<SCEVConstant>(Left.End)->getValue()->getZExtValue();
+    auto LeftStep = cast<SCEVConstant>(Left.Step)->getValue()->getZExtValue();
+    auto RightStart = cast<SCEVConstant>(Right.Start)->getValue()->getZExtValue();
+    auto RightEnd = cast<SCEVConstant>(Right.End)->getValue()->getZExtValue();
+    auto RightStep = cast<SCEVConstant>(Right.Step)->getValue()->getZExtValue();
+    if (LeftEnd < RightStart || RightEnd < LeftStart)
       return llvm::None;
     ColumnInfo Info;
     // We guarantee that K1 and K2 will not be equal to 0.
-    assert(Left.Step > 0 && Right.Step > 0 && "Steps must be positive!");
-    assert(Left.TripCount > 0 && Right.TripCount > 0 &&
-        "Trip count must be positive!");
-    ValueT L1 = Left.Start, K1 = Left.Step;
-    ValueT L2 = Right.Start, K2 = Right.Step;
-    VarRange XRange(0, Left.TripCount - 1), YRange(0, Right.TripCount - 1);
+    assert(LeftStep > 0 && RightStep > 0 && "Steps must be positive!");
+    assert(LeftStart <= LeftEnd && RightStart <= RightEnd &&
+        "Start of dimension must be less or equal than End.");
+    ValueT L1 = LeftStart, K1 = LeftStep;
+    ValueT L2 = RightStart, K2 = RightStep;
+    VarRange XRange(0, (LeftEnd - LeftStart) / LeftStep),
+             YRange(0, (RightEnd - RightStart) / RightStep);
     LinearSystem System;
     System.push_back(Monom(0, K1), Monom(1, -K2), L2 - L1);
     System.instantiate(Info);
@@ -306,17 +1478,15 @@ llvm::Optional<MemoryLocationRange> intersect(
     Tmax -= Shift;
     ValueT Step = K1 * B;
     ValueT Start = (K1 * A + L1) + Step * Shift;
-    auto &Intersection = Int.DimList[I];
-    Intersection.Start = Start;
-    Intersection.Step = Step;
-    Intersection.TripCount = Tmax + 1;
-    Intersection.DimSize = Left.DimSize;
+    Intersection.Start = SE->getConstant(Left.Start->getType(), Start);
+    Intersection.Step = SE->getConstant(Left.Step->getType(), Step);
+    Intersection.End = SE->getConstant(Left.End->getType(), Start + Step * Tmax);
+    Intersection.DimSize = std::max(Left.DimSize, Right.DimSize);
     assert(Start >= 0 && "Start must be non-negative!");
     assert(Step > 0 && "Step must be positive!");
-    assert(Intersection.TripCount > 0 && "Trip count must be non-negative!");
     if (LC) {
       llvm::SmallVector<Dimension, 3> ComplLeft;
-      if (!difference(Left, Intersection, ComplLeft, Threshold)) {
+      if (!difference(Left, Intersection, ComplLeft, SE, Threshold)) {
         return MemoryLocationRange();
       } else {
         for (auto &Comp : ComplLeft)
@@ -325,7 +1495,7 @@ llvm::Optional<MemoryLocationRange> intersect(
     }
     if (RC) {
       llvm::SmallVector<Dimension, 3> ComplRight;
-      if (!difference(Right, Intersection, ComplRight, Threshold)) {
+      if (!difference(Right, Intersection, ComplRight, SE, Threshold)) {
         return MemoryLocationRange();
       } else {
         for (auto &Comp : ComplRight)
@@ -337,3 +1507,30 @@ llvm::Optional<MemoryLocationRange> intersect(
   return Int;
 }
 }
+
+void Dimension::print(llvm::raw_ostream &OS, bool IsDebug) const {
+  auto PrintSCEV = [](const llvm::SCEV *Expr, llvm::raw_ostream &OS) {
+    if (!Expr)
+      OS << "(nullptr)";
+    else
+      Expr->print(OS);
+  };
+  if (IsDebug) {
+    OS << "{Start: ";
+    PrintSCEV(Start, OS);
+    OS << ", End: ";
+    PrintSCEV(End, OS);
+    OS << ", Step: ";
+    PrintSCEV(Step, OS);
+    OS << ", DimSize: " << DimSize << "}";
+  } else {
+    OS << "[";
+    PrintSCEV(Start, OS);
+    OS << ":";
+    PrintSCEV(End, OS);
+    OS << ":";
+    PrintSCEV(Step, OS);
+    OS << "," << DimSize;
+    OS << "]";
+  }
+}
\ No newline at end of file
diff --git a/lib/Analysis/Memory/Passes.cpp b/lib/Analysis/Memory/Passes.cpp
index bef87fe3..e9e72397 100644
--- a/lib/Analysis/Memory/Passes.cpp
+++ b/lib/Analysis/Memory/Passes.cpp
@@ -48,4 +48,5 @@ void llvm::initializeMemoryAnalysis(PassRegistry &Registry) {
   initializeDIArrayAccessWrapperPass(Registry);
   initializeAllocasAAWrapperPassPass(Registry);
   initializeGlobalsAccessWrapperPass(Registry);
+  initializeAssumptionInfoPassPass(Registry);
 }
diff --git a/lib/Core/Query.cpp b/lib/Core/Query.cpp
index 236a03a0..a6fbdf4a 100644
--- a/lib/Core/Query.cpp
+++ b/lib/Core/Query.cpp
@@ -187,6 +187,8 @@ void addAfterSROAAnalysis(const GlobalOptions &GO, const DataLayout &DL,
   Passes.add(createMemoryMatcherPass());
   Passes.add(createGlobalsAccessCollector());
   Passes.add(createCallExtractorPass());
+  Passes.add(createRedundantEdgeEliminationPass());
+  Passes.add(createUnreachableBlockEliminationPass());
   Passes.add(createGlobalDefinedMemoryPass());
   Passes.add(createGlobalLiveMemoryPass());
   Passes.add(createFunctionMemoryAttrsAnalysis());
@@ -219,6 +221,8 @@ void addAfterLoopRotateAnalysis(legacy::PassManager &Passes) {
   Passes.add(createMemoryMatcherPass());
   Passes.add(createGlobalsAccessCollector());
   Passes.add(createCallExtractorPass());
+  Passes.add(createRedundantEdgeEliminationPass());
+  Passes.add(createUnreachableBlockEliminationPass());
   Passes.add(createGlobalDefinedMemoryPass());
   Passes.add(createGlobalLiveMemoryPass());
   Passes.add(createFunctionMemoryAttrsAnalysis());
diff --git a/lib/Support/SCEVUtils.cpp b/lib/Support/SCEVUtils.cpp
index 04308cf9..c776c999 100644
--- a/lib/Support/SCEVUtils.cpp
+++ b/lib/Support/SCEVUtils.cpp
@@ -34,6 +34,8 @@ using namespace llvm;
 using namespace tsar;
 
 namespace {
+typedef SmallVector<PointerIntPair<Type *, 1, bool>, 1> TypeQueue;
+
 static inline int sizeOfSCEV(const SCEV *S) {
   struct FindSCEVSize {
     int Size;
@@ -427,6 +429,28 @@ inline const SCEV * stripCastIfNot(const SCEV *S, bool IsSafeTypeCast) {
       S = Cast->getOperand();
   return S;
 }
+
+const SCEV *getTypeQueue(TypeQueue &TQ, const SCEV *S) {
+  while (auto Cast{dyn_cast<SCEVCastExpr>(S)}) {
+    if (isa<SCEVSignExtendExpr>(Cast))
+      TQ.emplace_back(Cast->getType(), true);
+    else
+      TQ.emplace_back(Cast->getType(), false);
+    S = Cast->getOperand();
+  }
+  return S;
+};
+
+const SCEV *restoreCasts(const TypeQueue &TQ,
+                         const SCEV *S,
+                         ScalarEvolution *SE) {
+  assert(S && "SCEV must be specified!");
+  assert(SE && "ScalarEvolution must be specified!");
+  for (auto &T : reverse(TQ))
+    S = T.getInt() ? SE->getTruncateOrSignExtend(S, T.getPointer()) :
+                     SE->getTruncateOrZeroExtend(S, T.getPointer());
+  return S;
+}
 }
 
 namespace tsar {
@@ -618,4 +642,137 @@ std::vector<std::size_t> countPrimeNumbers(std::size_t Bound) {
   return Primes;
 }
 
+const SCEV *subtractSCEVAndCast(const SCEV *LHS,
+                                const SCEV *RHS,
+                                ScalarEvolution *SE) {
+  assert(SE && "ScalarEvolution must be specified!");
+  assert(LHS && RHS && "SCEV must be specified!");
+  TypeQueue TQLHS, TQRHS;
+  auto InnerLHS = getTypeQueue(TQLHS, LHS);
+  auto InnerRHS = getTypeQueue(TQRHS, RHS);
+  if (TQLHS != TQRHS) {
+    auto LC = dyn_cast<SCEVConstant>(InnerLHS);
+    auto RC = dyn_cast<SCEVConstant>(InnerRHS);
+    if (LC && RC) {
+      llvm_unreachable("Subtract constant SCEVs with a different cast.");
+    } else if (LC && !RC) {
+      InnerLHS = SE->getConstant(InnerRHS->getType(),
+          LC->getAPInt().getSExtValue());
+      return restoreCasts(TQRHS, SE->getMinusSCEV(InnerLHS, InnerRHS), SE);
+    } else if (!LC && RC) {
+      InnerRHS = SE->getConstant(InnerLHS->getType(),
+          RC->getAPInt().getSExtValue());
+      return restoreCasts(TQLHS, SE->getMinusSCEV(InnerLHS, InnerRHS), SE);
+    }
+    return SE->getMinusSCEV(LHS, RHS);
+  }
+  return restoreCasts(TQLHS, SE->getMinusSCEV(InnerLHS, InnerRHS), SE);
+}
+
+const SCEV *addSCEVAndCast(const SCEV *LHS,
+                           const SCEV *RHS,
+                           ScalarEvolution *SE) {
+  assert(SE && "ScalarEvolution must be specified!");
+  assert(LHS && RHS && "SCEV must be specified!");
+  TypeQueue TQLHS, TQRHS;
+  auto InnerLHS = getTypeQueue(TQLHS, LHS);
+  auto InnerRHS = getTypeQueue(TQRHS, RHS); 
+  if (TQLHS != TQRHS) {
+    auto LC = dyn_cast<SCEVConstant>(LHS);
+    auto RC = dyn_cast<SCEVConstant>(RHS);
+    if (LC && RC) {
+      llvm_unreachable("Add constant SCEVs with a different cast.");
+    } else if (LC && !RC) {
+      InnerLHS = SE->getConstant(InnerRHS->getType(),
+          LC->getAPInt().getSExtValue());
+      return restoreCasts(TQRHS, SE->getAddExpr(InnerLHS, InnerRHS), SE);
+    } else if (!LC && RC) {
+      InnerRHS = SE->getConstant(InnerLHS->getType(),
+          RC->getAPInt().getSExtValue());
+      return restoreCasts(TQLHS, SE->getAddExpr(InnerLHS, InnerRHS), SE);
+    }
+    return SE->getAddExpr(LHS, RHS);
+  }
+  return restoreCasts(TQLHS, SE->getAddExpr(InnerLHS, InnerRHS), SE);
+}
+
+const SCEV *addOneToSCEV(const SCEV *S, ScalarEvolution *SE) {
+  return addSCEVAndCast(S, SE->getOne(S->getType()), SE);
+}
+
+const SCEV *subtractOneFromSCEV(const SCEV *S, ScalarEvolution *SE) {
+  return subtractSCEVAndCast(S, SE->getOne(S->getType()), SE);
+}
+
+const SCEV *evaluateAtIteration(const SCEVAddRecExpr *ARE, const SCEV *It,
+                                ScalarEvolution *SE) {
+  assert(SE && "ScalarEvolution must be specified!");
+  assert(ARE && "SCEVAddRecExpr must be specified!");
+  auto *S = ARE->evaluateAtIteration(It, *SE);
+  if (auto Add{dyn_cast<SCEVAddExpr>(S)})
+    S = addSCEVAndCast(Add->getOperand(0), Add->getOperand(1), SE);
+  return S;
+}
+
+Optional<int64_t> compareSCEVs(const SCEV *LHS, const SCEV *RHS,
+                               ScalarEvolution *SE) {
+  assert(SE && "ScalarEvolution must be specified!");
+  assert(LHS && RHS && "SCEV must be specified!");
+  if (LHS == RHS)
+    return 0;
+  TypeQueue TQLHS, TQRHS;
+  auto InnerLHS = getTypeQueue(TQLHS, LHS);
+  auto InnerRHS = getTypeQueue(TQRHS, RHS);
+  if (TQLHS != TQRHS) {
+    // For cases like LHS = { zext(%v) - Const1 }, RHS = { zext(%v - Const2) }
+    // TODO (yukki.lapenko@gmail.com): can we extend this check for sext?
+    if (isa<SCEVZeroExtendExpr>(LHS) && isa<SCEVAddExpr>(RHS) ||
+        isa<SCEVAddExpr>(LHS) && isa<SCEVZeroExtendExpr>(RHS)) {
+      int SwapMult = 1;
+      auto First{LHS}, Second{RHS};
+      // Let the first SCEV be of kind { zext(%v) - Const1 } and the second
+      // be of kind { zext(%v - Const2) }.
+      if (isa<SCEVZeroExtendExpr>(LHS) && isa<SCEVAddExpr>(RHS)) {
+        std::swap(First, Second);
+        SwapMult = -1;
+      }
+      auto *FirstAdd = cast<SCEVAddExpr>(First);
+      auto *FirstOp0 = FirstAdd->getOperand(0);
+      auto *FirstOp1 = FirstAdd->getOperand(1);
+      // Let the first operand always be a non-constant value.
+      if (isa<SCEVConstant>(FirstOp0))
+        std::swap(FirstOp0, FirstOp1);
+      auto *FirstCast = dyn_cast<SCEVZeroExtendExpr>(FirstOp0);
+      if (!FirstCast)
+        return None;
+      auto *FirstVar = FirstCast->getOperand();
+      if (!isa<SCEVUnknown>(FirstVar))
+        return None;
+      auto *SecondCast = dyn_cast<SCEVZeroExtendExpr>(Second);
+      if (!SecondCast || !isa<SCEVAddExpr>(SecondCast->getOperand()))
+        return None;
+      auto *SecondAdd = cast<SCEVAddExpr>(SecondCast->getOperand());
+      auto *SecondOp0 = SecondAdd->getOperand(0);
+      auto *SecondOp1 = SecondAdd->getOperand(1);
+      if (isa<SCEVConstant>(SecondOp0))
+        std::swap(SecondOp0, SecondOp1);
+      if (!isa<SCEVUnknown>(SecondOp0))
+        return None;
+      auto FirstVarVal = cast<SCEVUnknown>(FirstVar)->getValue();
+      auto FirstConst = cast<SCEVConstant>(FirstOp1)->getAPInt().getSExtValue();
+      auto SecondVarVal = cast<SCEVUnknown>(SecondOp0)->getValue();
+      auto SecondConst =
+          cast<SCEVConstant>(SecondOp1)->getAPInt().getSExtValue();
+      if (FirstVarVal == SecondVarVal)
+        return (FirstConst - SecondConst) * SwapMult;
+    }
+    return None;
+  }
+  if (InnerLHS == InnerRHS)
+    return 0;
+  auto Const = SE->computeConstantDifference(InnerLHS, InnerRHS);
+  if (Const)
+    return Const->getSExtValue();
+  return None;
+}
 }
diff --git a/lib/Transform/IR/CMakeLists.txt b/lib/Transform/IR/CMakeLists.txt
index 64443454..ac63a9db 100644
--- a/lib/Transform/IR/CMakeLists.txt
+++ b/lib/Transform/IR/CMakeLists.txt
@@ -1,6 +1,6 @@
 set(TRANSFORM_SOURCES Passes.cpp DeadCodeElimination.cpp InterprocAttr.cpp
   MetadataUtils.cpp Utils.cpp CallExtractor.cpp DependenceInliner.cpp
-  NoCaptureAnalysis.cpp PointerScalarizer.cpp)
+  NoCaptureAnalysis.cpp PointerScalarizer.cpp RedundantEdgeElimination.cpp)
 
 if(MSVC_IDE)
   file(GLOB_RECURSE TRANSFORM_HEADERS RELATIVE ${CMAKE_CURRENT_SOURCE_DIR}
diff --git a/lib/Transform/IR/RedundantEdgeElimination.cpp b/lib/Transform/IR/RedundantEdgeElimination.cpp
new file mode 100644
index 00000000..67c7d01c
--- /dev/null
+++ b/lib/Transform/IR/RedundantEdgeElimination.cpp
@@ -0,0 +1,84 @@
+//===-RedundantEdgeElimination.cpp - Redundant Edge Elimination -*- C++ -*-===//
+//
+//                       Traits Static Analyzer (SAPFOR)
+//
+// Copyright 2021 DVM System Group
+//
+// Licensed under the Apache License, Version 2.0 (the "License");
+// you may not use this file except in compliance with the License.
+// You may obtain a copy of the License at
+//
+// http://www.apache.org/licenses/LICENSE-2.0
+//
+// Unless required by applicable law or agreed to in writing, software
+// distributed under the License is distributed on an "AS IS" BASIS,
+// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
+// See the License for the specific language governing permissions and
+// limitations under the License.
+//
+//===----------------------------------------------------------------------===//
+//
+// This file implements a pass to replace the always true conditional branch
+// instructions with an unconditional branch instruction.
+//
+//===----------------------------------------------------------------------===//
+
+#include "tsar/Transform/IR/Passes.h"
+#include <bcl/utility.h>
+#include <llvm/IR/Constants.h>
+#include <llvm/IR/Instructions.h>
+#include <llvm/Pass.h>
+#include <llvm/Support/Debug.h>
+#include <llvm/Transforms/Utils/BasicBlockUtils.h>
+
+#undef DEBUG_TYPE
+#define DEBUG_TYPE "red-edge"
+
+using namespace llvm;
+
+namespace {
+class RedundantEdgeEliminationPass :
+    public FunctionPass, private bcl::Uncopyable {
+public:
+  static char ID;
+
+  RedundantEdgeEliminationPass() : FunctionPass(ID) {
+    initializeRedundantEdgeEliminationPassPass(*PassRegistry::getPassRegistry());
+  }
+
+  bool runOnFunction(Function &F) override;
+};
+}
+
+char RedundantEdgeEliminationPass::ID = 0;
+
+INITIALIZE_PASS_BEGIN(RedundantEdgeEliminationPass, "red-edge",
+  "Redundant Edge Elimination", true, false)
+INITIALIZE_PASS_END(RedundantEdgeEliminationPass, "red-edge",
+  "Redundant Edge Elimination", true, false)
+
+FunctionPass * llvm::createRedundantEdgeEliminationPass() {
+  return new RedundantEdgeEliminationPass;
+}
+
+bool RedundantEdgeEliminationPass::runOnFunction(Function &F) {
+  LLVM_DEBUG(dbgs() << "[REDUNDANT EDGE]: analyze " << F.getName() << "\n");
+  for (auto &BB : F.getBasicBlockList()) {
+    if (auto *TI = BB.getTerminator()) {
+      if (auto *BI = dyn_cast<BranchInst>(TI)) {
+        LLVM_DEBUG(dbgs() << "[REDUNDANT EDGE] instruction: "; BI->dump());
+        if (BI->isConditional() && isa<ConstantInt>(BI->getCondition())) {
+          auto IsCondTrue = !cast<ConstantInt>(BI->getCondition())->equalsInt(0);
+          BI->getSuccessor(IsCondTrue ? 1 : 0)->removePredecessor(&BB);
+          ReplaceInstWithInst(
+              BI, IsCondTrue ?
+                  BranchInst::Create(BI->getSuccessor(0)) :
+                  BranchInst::Create(BI->getSuccessor(1)));
+          LLVM_DEBUG(dbgs() << "[REDUNDANT EDGE] after: "; BB.dump());
+        }
+      }
+    }
+  }
+  LLVM_DEBUG(dbgs() << "[REDUNDANT EDGE]: leave " << F.getName() << "\n");
+  return true;
+}
diff --git a/lib/Unparse/Utils.cpp b/lib/Unparse/Utils.cpp
index e41ea361..91a1c851 100644
--- a/lib/Unparse/Utils.cpp
+++ b/lib/Unparse/Utils.cpp
@@ -31,6 +31,7 @@
 #include "tsar/Unparse/DIUnparser.h"
 #include "tsar/Unparse/SourceUnparserUtils.h"
 #include "tsar/Unparse/VariableLocation.h"
+#include <llvm/Analysis/ValueTracking.h>
 #include <llvm/IR/DebugInfo.h>
 #include <llvm/Support/raw_ostream.h>
 #include <llvm/Transforms/Utils/Local.h>
@@ -84,12 +85,8 @@ void printLocationSource(llvm::raw_ostream &O, const MemoryLocationRange &Loc,
   if (!IsDebug) {
     if (!Loc.DimList.empty()) {
       O << ", ";
-      for (auto &Dim : Loc.DimList) {
-        O << "[";
-        O << Dim.Start << ":" << Dim.TripCount << ":" << Dim.Step << "," <<
-             Dim.DimSize;
-        O << "]";
-      }
+      for (auto &Dim : Loc.DimList)
+        Dim.print(O);
     }
   }
   O << ">";
@@ -97,13 +94,12 @@ void printLocationSource(llvm::raw_ostream &O, const MemoryLocationRange &Loc,
     if (!Loc.DimList.empty()) {
       O << ", {";
       for (auto &Dimension : Loc.DimList)
-        O << "{Start: " << Dimension.Start << ", Step: " << Dimension.Step <<
-            ", TripCount: " << Dimension.TripCount << ", DimSize: " <<
-            Dimension.DimSize << "}";
+        Dimension.print(O, true);
       O << "}";
     }
     O << " (" << Loc.getKindAsString() << ") ";
     O << " [" << Loc.Ptr << "]";
+    O << " [Underlying: " << getUnderlyingObject(Loc.Ptr, 0) << "]";
   }
 }
 void printLocationSource(llvm::raw_ostream &O, const EstimateMemory &EM,