Yes, 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 h

Yes, 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.