Skip to content

[ConstraintElim] Y -nsw X s> NonNeg implies Y s> X #118211

Closed
@dtcxzyw

Description

@dtcxzyw

Alive2: https://alive2.llvm.org/ce/z/H7v8VG

define i1 @src(i32 %x, i32 %y, i32 range(i32 0, -2147483648) %z) {
entry:
  %sub = sub nsw i32 %y, %x
  %cond = icmp sgt i32 %sub, %z
  call void @llvm.assume(i1 %cond)
  %ret = icmp slt i32 %x, %y
  ret i1 %ret
}

define i1 @tgt(i32 %x, i32 %y, i32 %z) {
entry:
  ret i1 true
}

See dtcxzyw/llvm-tools#57

Metadata

Metadata

Assignees

Type

No type

Projects

No projects

Milestone

No milestone

Relationships

None yet

Development

No branches or pull requests

Issue actions