[clang] [clang-tools-extra] Use Z3 (when available) for more complex cases in the clang dataflow framework (PR #222378)

[via cfe-commits]

github-actions[bot] wrote:

<!--LLVM CODE LINT COMMENT: clang-tidy-->


:warning: C/C++ code linter, clang-tidy found issues in your code. :warning:

<details>
<summary>
You can test this locally with the following command:
</summary>

```bash

git diff -U0 origin/main...HEAD -- clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.h |
python3 clang-tools-extra/clang-tidy/tool/clang-tidy-diff.py   -path build -p1 -quiet
```

</details>

<details>
<summary>
View the output from clang-tidy here.
</summary>

```
clang-tools-extra/clang-tidy/bugprone/UncheckedOptionalAccessCheck.cpp:61:70: warning: statement should have braces [readability-inconsistent-ifelse-braces]
   61 |               [this] { return dataflow::createSolver(SolverMode); }))
      |                                                                      ^
      |                                                                       {
   62 |     for (const UncheckedOptionalAccessDiagnostic &Diag : *Diags) {
   63 |       diag(Diag.Range.getBegin(), "unchecked access to optional value")
   64 |           << Diag.Range;
   65 |     }
   66 |   else {
      |   }
```

</details>


https://github.com/llvm/llvm-project/pull/222378