<div dir="ltr">Hi All,<div>Can someone please explain why the following transformations are safe to do?</div><div><br></div><div>Say we have the following C code:</div><div><b><font face="monospace">int main(){<br>    int x;<br>    assume(x>=0);<br>    assert(x<=-1);<br>    assume(x==1);<br>    assert(x!=1); <br>}</font></b><br></div><div><b><font face="monospace"><br></font></b></div><div>The corresponding IR with -O0 is:</div><div><b><font face="monospace">define dso_local i32 @main() #0 {<br>  %1 = alloca i32, align 4<br>  %2 = load i32, i32* %1, align 4<br>  %3 = icmp sge i32 %2, 0<br>  %4 = zext i1 %3 to i32<br>  %5 = call i32 (i32, ...) bitcast (i32 (...)* @__CPROVER_assume to i32 (i32, ...)*)(i32 %4)<br>  %6 = load i32, i32* %1, align 4<br>  %7 = icmp sle i32 %6, -1<br>  %8 = zext i1 %7 to i32<br>  %9 = call i32 (i32, ...) bitcast (i32 (...)* @assert to i32 (i32, ...)*)(i32 %8)<br>  %10 = load i32, i32* %1, align 4<br>  %11 = icmp eq i32 %10, 1<br>  %12 = zext i1 %11 to i32<br>  %13 = call i32 (i32, ...) bitcast (i32 (...)* @__CPROVER_assume to i32 (i32, ...)*)(i32 %12)<br>  %14 = load i32, i32* %1, align 4<br>  %15 = icmp ne i32 %14, 1<br>  %16 = zext i1 %15 to i32<br>  %17 = call i32 (i32, ...) bitcast (i32 (...)* @assert to i32 (i32, ...)*)(i32 %16)<br>  ret i32 0<br>}</font></b><br></div><div><br></div><div>However, if you run -O1 on this IR we are left with the following:</div><div><b><font face="monospace">define dso_local i32 @main() local_unnamed_addr #0 {<br>  %1 = call i32 (i32, ...) bitcast (i32 (...)* @__CPROVER_assume to i32 (i32, ...)*)(i32 1) #2<br>  %2 = call i32 (i32, ...) bitcast (i32 (...)* @assert to i32 (i32, ...)*)(i32 1) #2<br>  %3 = call i32 (i32, ...) bitcast (i32 (...)* @__CPROVER_assume to i32 (i32, ...)*)(i32 0) #2<br>  %4 = call i32 (i32, ...) bitcast (i32 (...)* @assert to i32 (i32, ...)*)(i32 0) #2<br>  ret i32 0<br>}</font></b><br></div><div><br></div><div>Is there any particular reason why assert(x<=1) is taken as true while assert(x!=1) is taken as false?</div><div><br></div><div>Thanks,</div><div>Akash.</div><div><br></div></div>