diff --git a/svf/include/AE/Svfexe/AbstractInterpretation.h b/svf/include/AE/Svfexe/AbstractInterpretation.h
index d86ad7769..4f7659320 100644
--- a/svf/include/AE/Svfexe/AbstractInterpretation.h
+++ b/svf/include/AE/Svfexe/AbstractInterpretation.h
@@ -282,6 +282,10 @@ class AbstractInterpretation
 
     void updateStateOnBinary(const BinaryOPStmt *binary);
 
+    IntervalValue comparePointerValues(const CmpStmt *cmp,
+                                       const AbstractValue& lhsValue,
+                                       const AbstractValue& rhsValue) const;
+
     void updateStateOnCmp(const CmpStmt *cmp);
 
     void updateStateOnLoad(const LoadStmt *load);
diff --git a/svf/lib/AE/Svfexe/AEDetector.cpp b/svf/lib/AE/Svfexe/AEDetector.cpp
index 7b611085c..991596093 100644
--- a/svf/lib/AE/Svfexe/AEDetector.cpp
+++ b/svf/lib/AE/Svfexe/AEDetector.cpp
@@ -470,6 +470,9 @@ bool BufOverflowDetector::canSafelyAccessMemory(const SVF::ValVar* value, const
     }
     for (const auto& addr : ptrVal.getAddrs())
     {
+        // Null cannot safely access a backing memory object.
+        if (AbstractState::isNullMem(addr))
+            return false;
         NodeID objId = ae.getAbsState(node).getIDFromAddr(addr);
         u32_t size = 0;
         // if the object is a constant size object, get the size directly
diff --git a/svf/lib/AE/Svfexe/AbsExtAPI.cpp b/svf/lib/AE/Svfexe/AbsExtAPI.cpp
index a595dc4df..ef143fe50 100644
--- a/svf/lib/AE/Svfexe/AbsExtAPI.cpp
+++ b/svf/lib/AE/Svfexe/AbsExtAPI.cpp
@@ -235,13 +235,9 @@ void AbsExtAPI::initExtFunMap()
         const AbstractValue& ptrVal = ae->getAbsValue(callNode->getArgument(0), callNode);
         for (auto addr: ptrVal.getAddrs())
         {
-            if (AbstractState::isBlackHoleObjAddr(addr))
-            {
-            }
-            else
-            {
+            if (!AbstractState::isBlackHoleObjAddr(addr) &&
+                    !AbstractState::isNullMem(addr))
                 as.addToFreedAddrs(addr);
-            }
         }
     };
     // Add all free-related functions to func_map
@@ -455,6 +451,9 @@ IntervalValue AbsExtAPI::getStrlen(const ValVar *strValue, const ICFGNode* node)
     const AbstractValue& ptrVal = ae->getAbsValue(strValue, node);
     for (const auto& addr : ptrVal.getAddrs())
     {
+        // Null has no backing buffer whose size can be inspected.
+        if (AbstractState::isNullMem(addr))
+            continue;
         NodeID objId = as.getIDFromAddr(addr);
         if (svfir->getBaseObject(objId)->isConstantByteSize())
         {
diff --git a/svf/lib/AE/Svfexe/AbstractInterpretation.cpp b/svf/lib/AE/Svfexe/AbstractInterpretation.cpp
index 3faea759f..cc3c4f7ef 100644
--- a/svf/lib/AE/Svfexe/AbstractInterpretation.cpp
+++ b/svf/lib/AE/Svfexe/AbstractInterpretation.cpp
@@ -241,9 +241,9 @@ void AbstractInterpretation::handleGlobalNode()
     // Use the manager's operator[] (auto-creates the entry if absent).
     AbstractState& init = abstractTrace[node];
     init = AbstractState();
-    // TODO: we cannot find right SVFVar for NullPtr, so we use init[NullPtr]
-    // directly. Same for BlkPtr below.
-    init[IRGraph::NullPtr] = AddressValue();
+    // NullPtr has no backing SVFVar. Model it directly as the singleton null
+    // address; BlkPtr is initialized directly below for the same reason.
+    init[IRGraph::NullPtr] = AddressValue(NullMemAddr);
 
     // Global Node, we just need to handle addr, load, store, copy and gep
     for (const SVFStmt *stmt: node->getSVFStmts())
@@ -495,23 +495,12 @@ bool AbstractInterpretation::isCmpBranchEdgeFeasible(const IntraCFGEdge* edge,
     s64_t succ = edge->getSuccessorCondValue();
     const CmpStmt* cmpStmt = SVFUtil::cast<CmpStmt>(
                                  *edge->getCondition()->getInEdges().begin());
-
-    if (cmpStmt->getOpVarID(0) == IRGraph::NullPtr ||
-            cmpStmt->getOpVarID(1) == IRGraph::NullPtr)
-        return true;
-
-    AbstractValue opVal[2] =
-    {
-        getAbsValue(cmpStmt->getOpVar(0), pred),
-        getAbsValue(cmpStmt->getOpVar(1), pred)
-    };
-
-    const bool hasIntervalCmp = opVal[0].isInterval() && opVal[1].isInterval();
-    if (!hasIntervalCmp && (opVal[0].isAddr() || opVal[1].isAddr()))
+    const AbstractValue& cmpValue = getAbsValue(cmpStmt->getRes(), pred);
+    if (!cmpValue.isInterval())
         return true;
 
     // Feasibility check: cmp result must be compatible with branch successor
-    IntervalValue resVal = getAbsValue(cmpStmt->getRes(), pred).getInterval();
+    IntervalValue resVal = cmpValue.getInterval();
     resVal.meet_with(IntervalValue((s64_t)succ, succ));
     if (resVal.isBottom())
         return false;
@@ -972,7 +961,8 @@ void AbstractInterpretation::handleSVFStatement(const SVFStmt *stmt)
         auto it = vmap.find(IRGraph::NullPtr);
         (void)it; // Suppress warning of unused variable under release build
         assert(it == vmap.end() ||
-               (!it->second.isInterval() && !it->second.isAddr()));
+               (it->second.isAddr() &&
+                it->second.getAddrs().equals(AddressValue(NullMemAddr))));
     }
 }
 
@@ -1138,229 +1128,136 @@ void AbstractInterpretation::updateStateOnBinary(const BinaryOPStmt *binary)
     updateAbsValue(binary->getRes(), resVal, node);
 }
 
+/// Equality is definitely true only for the same known singleton and may be
+/// true whenever the sets intersect or contain an unknown address.
+IntervalValue AbstractInterpretation::comparePointerValues(
+    const CmpStmt *cmp, const AbstractValue& lhsValue,
+    const AbstractValue& rhsValue) const
+{
+    const u32_t predicate = cmp->getPredicate();
+    bool negateResult;
+    // Equality uses the address-set result directly.
+    if (predicate == CmpStmt::ICMP_EQ)
+        negateResult = false;
+    // Inequality is the complement of a definite equality result.
+    else if (predicate == CmpStmt::ICMP_NE)
+        negateResult = true;
+    // Pointer ordering is not modelled, so either Boolean outcome is feasible.
+    else
+        return IntervalValue((s64_t)0, (s64_t)1);
+
+    // A pointer outside the address domain has no known target. Keep both
+    // outcomes instead of interpreting another abstract domain as an address.
+    if (!lhsValue.isAddr() || !rhsValue.isAddr())
+        return IntervalValue((s64_t)0, (s64_t)1);
+
+    const AddressValue lhs = lhsValue.getAddrs();
+    const AddressValue rhs = rhsValue.getAddrs();
+
+    // An unknown left address may equal any address on the right.
+    if (lhs.contains(BlackHoleObjAddr))
+        return IntervalValue((s64_t)0, (s64_t)1);
+
+    // An unknown right address may equal any address on the left.
+    if (rhs.contains(BlackHoleObjAddr))
+        return IntervalValue((s64_t)0, (s64_t)1);
+
+    bool equal;
+    // Two known, disjoint points-to sets are definitely unequal.
+    if (!lhs.hasIntersect(rhs))
+    {
+        equal = false;
+    }
+    else
+    {
+        // A non-singleton left set may select either an equal or unequal address.
+        if (lhs.size() != 1)
+            return IntervalValue((s64_t)0, (s64_t)1);
+
+        // The same uncertainty applies when only the right set is non-singleton.
+        if (rhs.size() != 1)
+            return IntervalValue((s64_t)0, (s64_t)1);
+
+        // Intersecting singleton sets necessarily contain the same address.
+        equal = true;
+    }
+
+    // The cases above establish equality; complement it only for ICMP_NE.
+    if (negateResult)
+        equal = !equal;
+    return IntervalValue((s64_t)equal);
+}
+
 void AbstractInterpretation::updateStateOnCmp(const CmpStmt *cmp)
 {
     const ICFGNode* node = cmp->getICFGNode();
-    u32_t op0 = cmp->getOpVarID(0);
-    u32_t op1 = cmp->getOpVarID(1);
     const AbstractValue& op0Val = getAbsValue(cmp->getOpVar(0), node);
     const AbstractValue& op1Val = getAbsValue(cmp->getOpVar(1), node);
 
-    // if it is address
-    if (op0Val.isAddr() && op1Val.isAddr())
-    {
-        IntervalValue resVal;
-        const AddressValue& addrOp0 = op0Val.getAddrs();
-        const AddressValue& addrOp1 = op1Val.getAddrs();
-        if (addrOp0.equals(addrOp1))
-        {
-            resVal = IntervalValue(1, 1);
-        }
-        else if (addrOp0.hasIntersect(addrOp1))
-        {
-            resVal = IntervalValue(0, 1);
-        }
-        else
-        {
-            resVal = IntervalValue(0, 0);
-        }
-        updateAbsValue(cmp->getRes(), resVal, node);
-    }
-    // if op0 or op1 is nullptr, compare abstractValue instead of touching addr or interval
-    else if (op0 == IRGraph::NullPtr || op1 == IRGraph::NullPtr)
+    if (cmp->getOpVar(0)->getType()->isPointerTy())
     {
-        IntervalValue resVal = (op0Val.equals(op1Val)) ? IntervalValue(1, 1) : IntervalValue(0, 0);
-        updateAbsValue(cmp->getRes(), resVal, node);
+        updateAbsValue(cmp->getRes(), comparePointerValues(cmp, op0Val, op1Val),
+                       node);
+        return;
     }
-    else
+
+    if (!op0Val.isInterval() || !op1Val.isInterval())
+        return;
+
+    const IntervalValue lhs = op0Val.getInterval();
+    const IntervalValue rhs = op1Val.getInterval();
+    IntervalValue resVal;
+    switch (cmp->getPredicate())
     {
-        {
-            IntervalValue resVal;
-            if (op0Val.isInterval() && op1Val.isInterval())
-            {
-                // Treat bottom (uninitialized) operands as top for soundness
-                IntervalValue lhs = op0Val.getInterval().isBottom() ? IntervalValue::top() : op0Val.getInterval(),
-                              rhs = op1Val.getInterval().isBottom() ? IntervalValue::top() : op1Val.getInterval();
-                // AbstractValue
-                auto predicate = cmp->getPredicate();
-                switch (predicate)
-                {
-                case CmpStmt::ICMP_EQ:
-                case CmpStmt::FCMP_OEQ:
-                case CmpStmt::FCMP_UEQ:
-                    resVal = (lhs == rhs);
-                    // resVal = (lhs.getInterval() == rhs.getInterval());
-                    break;
-                case CmpStmt::ICMP_NE:
-                case CmpStmt::FCMP_ONE:
-                case CmpStmt::FCMP_UNE:
-                    resVal = (lhs != rhs);
-                    break;
-                case CmpStmt::ICMP_UGT:
-                case CmpStmt::ICMP_SGT:
-                case CmpStmt::FCMP_OGT:
-                case CmpStmt::FCMP_UGT:
-                    resVal = (lhs > rhs);
-                    break;
-                case CmpStmt::ICMP_UGE:
-                case CmpStmt::ICMP_SGE:
-                case CmpStmt::FCMP_OGE:
-                case CmpStmt::FCMP_UGE:
-                    resVal = (lhs >= rhs);
-                    break;
-                case CmpStmt::ICMP_ULT:
-                case CmpStmt::ICMP_SLT:
-                case CmpStmt::FCMP_OLT:
-                case CmpStmt::FCMP_ULT:
-                    resVal = (lhs < rhs);
-                    break;
-                case CmpStmt::ICMP_ULE:
-                case CmpStmt::ICMP_SLE:
-                case CmpStmt::FCMP_OLE:
-                case CmpStmt::FCMP_ULE:
-                    resVal = (lhs <= rhs);
-                    break;
-                case CmpStmt::FCMP_FALSE:
-                    resVal = IntervalValue(0, 0);
-                    break;
-                case CmpStmt::FCMP_TRUE:
-                    resVal = IntervalValue(1, 1);
-                    break;
-                case CmpStmt::FCMP_ORD:
-                case CmpStmt::FCMP_UNO:
-                    // FCMP_ORD: true if both operands are not NaN
-                    // FCMP_UNO: true if either operand is NaN
-                    // Conservatively return [0, 1] since we don't track NaN
-                    resVal = IntervalValue(0, 1);
-                    break;
-                default:
-                    assert(false && "undefined compare: ");
-                }
-                updateAbsValue(cmp->getRes(), resVal, node);
-            }
-            else if (op0Val.isAddr() && op1Val.isAddr())
-            {
-                const AddressValue& lhs = op0Val.getAddrs();
-                const AddressValue& rhs = op1Val.getAddrs();
-                auto predicate = cmp->getPredicate();
-                switch (predicate)
-                {
-                case CmpStmt::ICMP_EQ:
-                case CmpStmt::FCMP_OEQ:
-                case CmpStmt::FCMP_UEQ:
-                {
-                    if (lhs.hasIntersect(rhs))
-                    {
-                        resVal = IntervalValue(0, 1);
-                    }
-                    else if (lhs.empty() && rhs.empty())
-                    {
-                        resVal = IntervalValue(1, 1);
-                    }
-                    else
-                    {
-                        resVal = IntervalValue(0, 0);
-                    }
-                    break;
-                }
-                case CmpStmt::ICMP_NE:
-                case CmpStmt::FCMP_ONE:
-                case CmpStmt::FCMP_UNE:
-                {
-                    if (lhs.hasIntersect(rhs))
-                    {
-                        resVal = IntervalValue(0, 1);
-                    }
-                    else if (lhs.empty() && rhs.empty())
-                    {
-                        resVal = IntervalValue(0, 0);
-                    }
-                    else
-                    {
-                        resVal = IntervalValue(1, 1);
-                    }
-                    break;
-                }
-                case CmpStmt::ICMP_UGT:
-                case CmpStmt::ICMP_SGT:
-                case CmpStmt::FCMP_OGT:
-                case CmpStmt::FCMP_UGT:
-                {
-                    if (lhs.size() == 1 && rhs.size() == 1)
-                    {
-                        resVal = IntervalValue(*lhs.begin() > *rhs.begin());
-                    }
-                    else
-                    {
-                        resVal = IntervalValue(0, 1);
-                    }
-                    break;
-                }
-                case CmpStmt::ICMP_UGE:
-                case CmpStmt::ICMP_SGE:
-                case CmpStmt::FCMP_OGE:
-                case CmpStmt::FCMP_UGE:
-                {
-                    if (lhs.size() == 1 && rhs.size() == 1)
-                    {
-                        resVal = IntervalValue(*lhs.begin() >= *rhs.begin());
-                    }
-                    else
-                    {
-                        resVal = IntervalValue(0, 1);
-                    }
-                    break;
-                }
-                case CmpStmt::ICMP_ULT:
-                case CmpStmt::ICMP_SLT:
-                case CmpStmt::FCMP_OLT:
-                case CmpStmt::FCMP_ULT:
-                {
-                    if (lhs.size() == 1 && rhs.size() == 1)
-                    {
-                        resVal = IntervalValue(*lhs.begin() < *rhs.begin());
-                    }
-                    else
-                    {
-                        resVal = IntervalValue(0, 1);
-                    }
-                    break;
-                }
-                case CmpStmt::ICMP_ULE:
-                case CmpStmt::ICMP_SLE:
-                case CmpStmt::FCMP_OLE:
-                case CmpStmt::FCMP_ULE:
-                {
-                    if (lhs.size() == 1 && rhs.size() == 1)
-                    {
-                        resVal = IntervalValue(*lhs.begin() <= *rhs.begin());
-                    }
-                    else
-                    {
-                        resVal = IntervalValue(0, 1);
-                    }
-                    break;
-                }
-                case CmpStmt::FCMP_FALSE:
-                    resVal = IntervalValue(0, 0);
-                    break;
-                case CmpStmt::FCMP_TRUE:
-                    resVal = IntervalValue(1, 1);
-                    break;
-                case CmpStmt::FCMP_ORD:
-                case CmpStmt::FCMP_UNO:
-                    // FCMP_ORD: true if both operands are not NaN
-                    // FCMP_UNO: true if either operand is NaN
-                    // Conservatively return [0, 1] since we don't track NaN
-                    resVal = IntervalValue(0, 1);
-                    break;
-                default:
-                    assert(false && "undefined compare: ");
-                }
-                updateAbsValue(cmp->getRes(), resVal, node);
-            }
-        }
+    case CmpStmt::ICMP_EQ:
+    case CmpStmt::FCMP_OEQ:
+    case CmpStmt::FCMP_UEQ:
+        resVal = (lhs == rhs);
+        break;
+    case CmpStmt::ICMP_NE:
+    case CmpStmt::FCMP_ONE:
+    case CmpStmt::FCMP_UNE:
+        resVal = (lhs != rhs);
+        break;
+    case CmpStmt::ICMP_UGT:
+    case CmpStmt::ICMP_SGT:
+    case CmpStmt::FCMP_OGT:
+    case CmpStmt::FCMP_UGT:
+        resVal = (lhs > rhs);
+        break;
+    case CmpStmt::ICMP_UGE:
+    case CmpStmt::ICMP_SGE:
+    case CmpStmt::FCMP_OGE:
+    case CmpStmt::FCMP_UGE:
+        resVal = (lhs >= rhs);
+        break;
+    case CmpStmt::ICMP_ULT:
+    case CmpStmt::ICMP_SLT:
+    case CmpStmt::FCMP_OLT:
+    case CmpStmt::FCMP_ULT:
+        resVal = (lhs < rhs);
+        break;
+    case CmpStmt::ICMP_ULE:
+    case CmpStmt::ICMP_SLE:
+    case CmpStmt::FCMP_OLE:
+    case CmpStmt::FCMP_ULE:
+        resVal = (lhs <= rhs);
+        break;
+    case CmpStmt::FCMP_FALSE:
+        resVal = IntervalValue(0, 0);
+        break;
+    case CmpStmt::FCMP_TRUE:
+        resVal = IntervalValue(1, 1);
+        break;
+    case CmpStmt::FCMP_ORD:
+    case CmpStmt::FCMP_UNO:
+        // Conservatively return [0, 1] since we do not track NaN.
+        resVal = IntervalValue(0, 1);
+        break;
+    default:
+        assert(false && "undefined compare: ");
     }
+    updateAbsValue(cmp->getRes(), resVal, node);
 }
 
 void AbstractInterpretation::updateStateOnLoad(const LoadStmt *load)
diff --git a/svf/lib/AE/Svfexe/AbstractStateManager.cpp b/svf/lib/AE/Svfexe/AbstractStateManager.cpp
index 6b0324581..aab43425b 100644
--- a/svf/lib/AE/Svfexe/AbstractStateManager.cpp
+++ b/svf/lib/AE/Svfexe/AbstractStateManager.cpp
@@ -324,6 +324,9 @@ AddressValue AbstractInterpretation::getGepObjAddrs(const ValVar* pointer, Inter
         const AbstractValue& addrs = getAbsValue(pointer, node);
         for (const auto& addr : addrs.getAddrs())
         {
+            // Null has no object from which a field address can be derived.
+            if (AbstractState::isNullMem(addr))
+                continue;
             s64_t baseObj = as.getIDFromAddr(addr);
             assert(SVFUtil::isa<ObjVar>(svfir->getSVFVar(baseObj)) && "Fail to get the base object address!");
             NodeID gepObj = svfir->getGepObjVar(baseObj, i);
@@ -341,6 +344,9 @@ AbstractValue AbstractInterpretation::loadValue(const ValVar* pointer, const ICF
     AbstractValue res;
     for (auto addr : ptrVal.getAddrs())
     {
+        // Null has no memory object from which a value can be loaded.
+        if (AbstractState::isNullMem(addr))
+            continue;
         res.join_with(
             getAbsValue(svfir->getSVFVar(as.getIDFromAddr(addr)), node));
     }
@@ -352,7 +358,12 @@ void AbstractInterpretation::storeValue(const ValVar* pointer, const AbstractVal
     const AbstractValue& ptrVal = getAbsValue(pointer, node);
     AbstractState& as = getAbsState(node);
     for (auto addr : ptrVal.getAddrs())
+    {
+        // Null has no memory object that can be updated.
+        if (AbstractState::isNullMem(addr))
+            continue;
         updateAbsValue(svfir->getSVFVar(as.getIDFromAddr(addr)), val, node);
+    }
 }
 
 const SVFType* AbstractInterpretation::getPointeeElement(const ObjVar* var, const ICFGNode* node)
@@ -399,4 +410,3 @@ u32_t AbstractInterpretation::getAllocaInstByteSize(const AddrStmt* addr)
     assert(false && "Addr rhs value is not ObjVar");
     abort();
 }
-