| Issue |
165779
|
| Summary |
z3 refutation crash - fatal error: error in backend: Z3 error: operator is applied to arguments of the wrong sort
|
| Labels |
new issue
|
| Assignees |
|
| Reporter |
vabridgers
|
The simple reproducer
``
void z3_crash(long a) {
if (~-(5 && a)) {
long *c;
*c; // expected-warning{{Dereference of undefined pointer value (loaded from variable 'c')}}
}
}
``
To run:
clang --analyze -Xclang -analyzer-config -Xclang crosscheck-with-z3=true z3.c
``
![]()
_______________________________________________
llvm-bugs mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/llvm-bugs
