[PATCH] D83660: [analyzer] Fix a crash for dereferencing an empty llvm::Optional variable in SMTConstraintManager.h.

Wed Mar 31 10:01:17 PDT 2021

steakhal added a comment.

In D83660#2661646 <https://reviews.llvm.org/D83660#2661646>, @OikawaKirie wrote:

> Can we automatically enable all test cases requiring z3 if clang is built with z3? I do not think the patch D83677 <https://reviews.llvm.org/D83677> really make the problem fixed.

Z3 constraint manager is unsupported, thus no test runs those parts. And yea, crashes more often than not.

The primary goal of D83677 <https://reviews.llvm.org/D83677> is to run the analyzer with the dummy range-based constraint manager, but with Z3 bugreport refutation. This scenario is monitored and maintained currently by us, Ericsson. We put effort into fixing crashes relating to this, thus it would be nice to state a test requirement that it `// REQUIRES: z3`, but only for refutation - which is really fast, has negligible overhead.
The main concern with the Z3 constraint manager is that it's really slow, beyond comfortable for tight CI loops.
So, `// REQUIRES: z3` means a little bit different than it supposed. `z3-solver` would be closer to reality.

CHANGES SINCE LAST ACTION
  https://reviews.llvm.org/D83660/new/

https://reviews.llvm.org/D83660