trunc(X - Y) != 0 implies X != Y

[dtcxzyw]

https://alive2.llvm.org/ce/z/ZM6AGq

define i1 @src201(i64 %0, i64 %1) local_unnamed_addr #0 {
entry:
  %2 = icmp eq i64 %1, %0
  %3 = sub i64 %0, %1
  %4 = trunc i64 %3 to i32
  %5 = icmp ugt i32 %4, 2
  tail call void @llvm.assume(i1 %5)
  ret i1 %2
}

; Function Attrs: mustprogress nofree norecurse nosync nounwind willreturn memory(none)
define noundef i1 @tgt201(i64 %0, i64 %1) local_unnamed_addr #2 {
entry:
  ret i1 false
}

tests/draco/optimized/kd_tree_attributes_encoder.cc.ll

[dtcxzyw]

https://alive2.llvm.org/ce/z/tYgWXL

; Function Attrs: mustprogress nofree norecurse nosync nounwind willreturn memory(inaccessiblemem: write)
define i1 @src1(i64 %0, i64 %1) local_unnamed_addr #0 {
entry:
  %2 = sub i64 %0, %1
  %3 = sdiv exact i64 %2, 12
  %4 = trunc i64 %3 to i32
  %5 = icmp ugt i32 %4, 2
  tail call void @llvm.assume(i1 %5)
  %6 = icmp eq i64 %1, %0
  ret i1 %6
}

; Function Attrs: mustprogress nocallback nofree nosync nounwind willreturn memory(inaccessiblemem: write)
declare void @llvm.assume(i1 noundef) #1

; Function Attrs: mustprogress nofree norecurse nosync nounwind willreturn memory(none)
define noundef i1 @tgt1(i64 %0, i64 %1) local_unnamed_addr #2 {
entry:
  ret i1 false
}

tests/draco/optimized/float_points_tree_encoder.cc.ll