[cfe-dev] Integration of Z3 for constraint solving [r299463]

[Paulo Matos via cfe-dev]

On 10/04/17 21:21, Dominic Chen wrote:
> This is for the clang static analyzer, when performing symbolic
> execution on input C code. Since the variables are all fixed-width
> bitvectors, and there are no existential/universal quantifiers, in
> practice the performance is decent, although still slower than the
> current range-based constraint manager. However, it allows for reasoning
> over more complex queries, e.g. involving multiple symbolic variables,
> symbolic truncation/extension, and symbolic floating-point expressions
> (these are all follow-up patches that have not yet been merged). There's
> a longer discussion and more concrete performance numbers starting
> around comment https://reviews.llvm.org/D28952#652510 .
> 

Ah, interesting. Thanks for the explanation. That's what I needed to know.

-- 
Paulo Matos