solver doesn't realize that `z > x && z < y` is unsat with the fact `x == y`
Opened this issue · 0 comments
0x21af commented
extern void clang_analyzer_eval();
extern void clang_analyzer_warnIfReached();
int foo(int x, int y, int z)
{
if (x == y)
{
if (z > x)
{
clang_analyzer_eval(x == y);
clang_analyzer_eval(z < y);
if (z < y)
{
clang_analyzer_warnIfReached();
}
}
}
}
report: llvm/llvm-project#62215