2 ms·
> A question: have you verified that the Z3 support is enabled in the LLVM toolchain you use for Clang SA? It is in Debian Bookworm, but not in Buster, and from
by ryao 4y ago
> A question: have you verified that the Z3 support is enabled in the LLVM toolchain you use for Clang SA? It is in Debian Bookworm, but not in Buster, and from memory I don't think it is for Ubuntu 20.04 (LTS) due to a packaging snafu.
That was one of the first things I did. Recompiling with z3 support made little difference. That said, I thought --z3-refutation Was the default when it was available.
I will try rerunning tests with it explicitly specified, but I do not expect much from that, since running tests with --z3, which replaces the range checker with z3, did not really eliminate reports beyond those that were in files that caused clang’s static analyzer to crash when that was set.
- yaantc 4y agoYes, if the LLVM toolchain has Z3 support then `--z3-refutation` will be the default. It's only useful if you want an error in case the LLVM toolchain may not have this support. I've read somewhere that the "full Z3" mode with `--z3` is very experimental and not well maintained. It didn't crash when I tried it but was no better and way too slow: typically 15 times slower on average, but a few files took over 24 hours to check.