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

_______________________________________________
cfe-commits mailing list
cfe-commits@lists.llvm.org
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits

Reply via email to