diff --git a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
--- a/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
+++ b/llvm/lib/Transforms/Scalar/ConstraintElimination.cpp
@@ -192,8 +192,10 @@
 
   ConstraintTy() = default;
 
-  ConstraintTy(SmallVector<int64_t, 8> Coefficients, bool IsSigned, bool IsEq)
-      : Coefficients(Coefficients), IsSigned(IsSigned), IsEq(IsEq) {}
+  ConstraintTy(SmallVector<int64_t, 8> Coefficients, bool IsSigned, bool IsEq,
+               bool IsNe)
+      : Coefficients(Coefficients), IsSigned(IsSigned), IsEq(IsEq), IsNe(IsNe) {
+  }
 
   unsigned size() const { return Coefficients.size(); }
 
@@ -205,6 +207,8 @@
 
   bool isEq() const { return IsEq; }
 
+  bool isNe() const { return IsNe; }
+
   /// Check if the current constraint is implied by the given ConstraintSystem.
   ///
   /// \return true or false if the constraint is proven to be respectively true,
@@ -214,6 +218,7 @@
 
 private:
   bool IsEq = false;
+  bool IsNe = false;
 };
 
 /// Wrapper encapsulating separate constraint systems and corresponding value
@@ -502,6 +507,8 @@
                               SmallVectorImpl<Value *> &NewVariables) const {
   assert(NewVariables.empty() && "NewVariables must be empty when passed in");
   bool IsEq = false;
+  bool IsNe = false;
+
   // Try to convert Pred to one of ULE/SLT/SLE/SLT.
   switch (Pred) {
   case CmpInst::ICMP_UGT:
@@ -521,10 +528,13 @@
     }
     break;
   case CmpInst::ICMP_NE:
-    if (!match(Op1, m_Zero()))
-      return {};
-    Pred = CmpInst::getSwappedPredicate(CmpInst::ICMP_UGT);
-    std::swap(Op0, Op1);
+    if (match(Op1, m_Zero())) {
+      Pred = CmpInst::getSwappedPredicate(CmpInst::ICMP_UGT);
+      std::swap(Op0, Op1);
+    } else {
+      IsNe = true;
+      Pred = CmpInst::ICMP_ULE;
+    }
     break;
   default:
     break;
@@ -571,7 +581,7 @@
   // subtracting all coefficients from B.
   ConstraintTy Res(
       SmallVector<int64_t, 8>(Value2Index.size() + NewVariables.size() + 1, 0),
-      IsSigned, IsEq);
+      IsSigned, IsEq, IsNe);
   // Collect variables that are known to be positive in all uses in the
   // constraint.
   DenseMap<Value *, bool> KnownNonNegativeVariables;
@@ -653,15 +663,16 @@
 ConstraintTy::isImpliedBy(const ConstraintSystem &CS) const {
   bool IsConditionImplied = CS.isConditionImplied(Coefficients);
 
-  if (IsEq) {
+  if (IsEq || IsNe) {
     auto NegatedOrEqual = ConstraintSystem::negateOrEqual(Coefficients);
     bool IsNegatedOrEqualImplied =
         !NegatedOrEqual.empty() && CS.isConditionImplied(NegatedOrEqual);
 
-    // In order to check that `%a == %b` is true, we want to check that `%a >=
-    // %b` and `%a <= %b` must hold.
+    // In order to check that `%a == %b` is true (equality), both conditions `%a
+    // >= %b` and `%a <= %b` must hold true. When checking for equality (`IsEq`
+    // is true), we return true if they both hold, false in the other cases.
     if (IsConditionImplied && IsNegatedOrEqualImplied)
-      return true;
+      return IsEq;
 
     auto Negated = ConstraintSystem::negate(Coefficients);
     bool IsNegatedImplied = !Negated.empty() && CS.isConditionImplied(Negated);
@@ -670,10 +681,12 @@
     bool IsStrictLessThanImplied =
         !StrictLessThan.empty() && CS.isConditionImplied(StrictLessThan);
 
-    // In order to check that `%a == %b` is false, we want to check whether
-    // either `%a > %b` or `%a < %b` holds.
+    // In order to check that `%a != %b` is true (non-equality), either
+    // condition `%a > %b` or `%a < %b` must hold true. When checking for
+    // non-equality (`IsNe` is true), we return true if one of the two holds,
+    // false in the other cases.
     if (IsNegatedImplied || IsStrictLessThanImplied)
-      return false;
+      return IsNe;
 
     return std::nullopt;
   }
@@ -1141,7 +1154,9 @@
   // hold.
   SmallVector<Value *> NewVariables;
   auto R = getConstraint(Pred, A, B, NewVariables);
-  if (!R.isValid(*this))
+
+  // TODO: Support non-equality for facts as well.
+  if (!R.isValid(*this) || R.isNe())
     return;
 
   LLVM_DEBUG(dbgs() << "Adding '" << Pred << " ";
diff --git a/llvm/test/Transforms/ConstraintElimination/constants-unsigned-predicates.ll b/llvm/test/Transforms/ConstraintElimination/constants-unsigned-predicates.ll
--- a/llvm/test/Transforms/ConstraintElimination/constants-unsigned-predicates.ll
+++ b/llvm/test/Transforms/ConstraintElimination/constants-unsigned-predicates.ll
@@ -94,9 +94,9 @@
 ; CHECK-NEXT:  entry:
 ; CHECK-NEXT:    [[T_0:%.*]] = icmp ne i8 10, 11
 ; CHECK-NEXT:    [[F_0:%.*]] = icmp ne i8 10, 10
-; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 [[T_0]], [[F_0]]
+; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 true, false
 ; CHECK-NEXT:    [[T_1:%.*]] = icmp ne i8 10, 9
-; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[T_1]]
+; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], true
 ; CHECK-NEXT:    ret i1 [[RES_2]]
 ;
 entry:
diff --git a/llvm/test/Transforms/ConstraintElimination/ne.ll b/llvm/test/Transforms/ConstraintElimination/ne.ll
--- a/llvm/test/Transforms/ConstraintElimination/ne.ll
+++ b/llvm/test/Transforms/ConstraintElimination/ne.ll
@@ -1,6 +1,8 @@
 ; NOTE: Assertions have been autogenerated by utils/update_test_checks.py UTC_ARGS: --check-attributes
 ; RUN: opt -passes=constraint-elimination -S %s | FileCheck %s
 
+declare void @llvm.assume(i1)
+
 define i1 @test_eq_ne_0(i8 %a, i8 %b) {
 ; CHECK-LABEL: @test_eq_ne_0(
 ; CHECK-NEXT:  entry:
@@ -10,7 +12,7 @@
 ; CHECK-NEXT:    [[F_1:%.*]] = icmp ne i8 [[A]], 0
 ; CHECK-NEXT:    [[C_1:%.*]] = icmp ne i8 [[A]], 1
 ; CHECK-NEXT:    [[C_2:%.*]] = icmp ne i8 [[A]], [[B:%.*]]
-; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 false, [[C_1]]
+; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 false, true
 ; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[C_2]]
 ; CHECK-NEXT:    ret i1 [[RES_2]]
 ; CHECK:       else:
@@ -69,7 +71,7 @@
 ; CHECK:       else:
 ; CHECK-NEXT:    [[F_1:%.*]] = icmp ne i8 [[A]], 0
 ; CHECK-NEXT:    [[C_7:%.*]] = icmp ne i8 [[A]], 1
-; CHECK-NEXT:    [[RES_9:%.*]] = xor i1 false, [[C_7]]
+; CHECK-NEXT:    [[RES_9:%.*]] = xor i1 false, true
 ; CHECK-NEXT:    [[C_8:%.*]] = icmp ne i8 [[A]], [[B]]
 ; CHECK-NEXT:    [[RES_10:%.*]] = xor i1 [[RES_9]], [[C_8]]
 ; CHECK-NEXT:    [[C_9:%.*]] = icmp eq i8 [[A]], [[B]]
@@ -156,7 +158,7 @@
 ; CHECK-NEXT:    [[F_1:%.*]] = icmp ne i8 [[A]], 0
 ; CHECK-NEXT:    [[C_1:%.*]] = icmp ne i8 [[A]], 1
 ; CHECK-NEXT:    [[C_2:%.*]] = icmp ne i8 [[A]], [[B:%.*]]
-; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 true, [[C_1]]
+; CHECK-NEXT:    [[RES_1:%.*]] = xor i1 true, false
 ; CHECK-NEXT:    [[RES_2:%.*]] = xor i1 [[RES_1]], [[C_2]]
 ; CHECK-NEXT:    ret i1 [[RES_2]]
 ; CHECK:       else:
@@ -215,7 +217,7 @@
 ; CHECK:       else:
 ; CHECK-NEXT:    [[T_2:%.*]] = icmp ne i8 [[A]], 0
 ; CHECK-NEXT:    [[C_9:%.*]] = icmp ne i8 [[A]], 1
-; CHECK-NEXT:    [[RES_9:%.*]] = xor i1 true, [[C_9]]
+; CHECK-NEXT:    [[RES_9:%.*]] = xor i1 true, false
 ; CHECK-NEXT:    [[C_10:%.*]] = icmp ne i8 [[A]], [[B]]
 ; CHECK-NEXT:    [[RES_10:%.*]] = xor i1 [[RES_9]], [[C_10]]
 ; CHECK-NEXT:    [[C_11:%.*]] = icmp eq i8 [[A]], [[B]]
@@ -292,3 +294,157 @@
 
   ret i1 %res.16
 }
+
+define i1 @assume_b_plus_1_ult_a(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_b_plus_1_ult_a(
+; CHECK-NEXT:    [[TMP1:%.*]] = add nuw i64 [[B:%.*]], 1
+; CHECK-NEXT:    [[TMP2:%.*]] = icmp ult i64 [[TMP1]], [[A:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP2]])
+; CHECK-NEXT:    [[TMP3:%.*]] = icmp ne i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 true
+;
+  %1 = add nuw i64 %b, 1
+  %2 = icmp ult i64 %1, %a
+  tail call void @llvm.assume(i1 %2)
+  %3 = icmp ne i64 %a, %b
+  ret i1 %3
+}
+
+define i1 @assume_a_gt_b_and_b_ge_c(i64 %a, i64 %b, i64 %c) {
+; CHECK-LABEL: @assume_a_gt_b_and_b_ge_c(
+; CHECK-NEXT:    [[TMP1:%.*]] = icmp ugt i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP1]])
+; CHECK-NEXT:    [[TMP2:%.*]] = icmp uge i64 [[B]], [[C:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP2]])
+; CHECK-NEXT:    [[TMP3:%.*]] = icmp ne i64 [[A]], [[C]]
+; CHECK-NEXT:    ret i1 true
+;
+  %1 = icmp ugt i64 %a, %b
+  tail call void @llvm.assume(i1 %1)
+  %2 = icmp uge i64 %b, %c
+  tail call void @llvm.assume(i1 %2)
+  %3 = icmp ne i64 %a, %c
+  ret i1 %3
+}
+
+define i1 @assume_a_ne_b_and_b_ne_c(i64 %a, i64 %b, i64 %c) {
+; CHECK-LABEL: @assume_a_ne_b_and_b_ne_c(
+; CHECK-NEXT:    [[TMP1:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP1]])
+; CHECK-NEXT:    [[TMP2:%.*]] = icmp ne i64 [[B]], [[C:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[TMP2]])
+; CHECK-NEXT:    [[TMP3:%.*]] = icmp ne i64 [[A]], [[C]]
+; CHECK-NEXT:    ret i1 [[TMP3]]
+;
+  %1 = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %1)
+  %2 = icmp ne i64 %b, %c
+  tail call void @llvm.assume(i1 %2)
+  %3 = icmp ne i64 %a, %c
+  ret i1 %3
+}
+
+define i1 @assume_1a(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_1a(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp ugt i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp ugt i64 %a, %b
+  ret i1 %ret
+}
+
+define i1 @assume_1b(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_1b(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp uge i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp uge i64 %a, %b
+  ret i1 %ret
+}
+
+define i1 @assume_2a(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_2a(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp ult i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp ult i64 %a, %b
+  ret i1 %ret
+}
+
+define i1 @assume_2b(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_2b(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp ule i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp ule i64 %a, %b
+  ret i1 %ret
+}
+
+; TODO: extend to support signed comparisons
+define i1 @assume_3a(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_3a(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp sgt i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp sgt i64 %a, %b
+  ret i1 %ret
+}
+
+define i1 @assume_3b(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_3b(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp sge i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp sge i64 %a, %b
+  ret i1 %ret
+}
+
+define i1 @assume_4a(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_4a(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp slt i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp slt i64 %a, %b
+  ret i1 %ret
+}
+
+define i1 @assume_4b(i64 %a, i64 %b) {
+; CHECK-LABEL: @assume_4b(
+; CHECK-NEXT:    [[NE:%.*]] = icmp ne i64 [[A:%.*]], [[B:%.*]]
+; CHECK-NEXT:    tail call void @llvm.assume(i1 [[NE]])
+; CHECK-NEXT:    [[RET:%.*]] = icmp sle i64 [[A]], [[B]]
+; CHECK-NEXT:    ret i1 [[RET]]
+;
+  %ne = icmp ne i64 %a, %b
+  tail call void @llvm.assume(i1 %ne)
+  %ret = icmp sle i64 %a, %b
+  ret i1 %ret
+}