[clang] [analyzer] Correct crash in Z3 wrapper (PR #158276)

[Donát Nagy via cfe-commits]

================
@@ -455,6 +455,14 @@ class SMTConv {
       QualType OperandTy;
       llvm::SMTExprRef OperandExp =
           getSymExpr(Solver, Ctx, USE->getOperand(), &OperandTy, hasComparison);
+
+      if (const BinarySymExpr *BSE =
+              dyn_cast<BinarySymExpr>(USE->getOperand())) {
+        if (USE->getOpcode() == UO_Minus &&
+            BinaryOperator::isComparisonOp(BSE->getOpcode()))
----------------
NagyDonat wrote:

```suggestion
            BinaryOperator::isComparisonOp(BSE->getOpcode()))
            // The comparison operator yields a boolean value in the Z3
            // language and applying the unary minus operator on a boolean
            // crashes Z3. However, the unary minus does nothing in this
            // context (a number is truthy if and only if its negative is
            // truthy), so let's just ignore the unary minus.
            // TODO: Replace this with a more general solution.
```
I like that you documented this situation in the test file, and a determined reader would be able to find that (by checking git blame), but let's also document this logic here for the lazier readers :)

(Feel free to tweak my suggested comment if you think that you can improve it.)

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