[clang] [analyzer] Fix crash in Z3 SMTConv when negating a boolean expression (#165779) (PR #168034)

[Balázs Benics via cfe-commits]

================
@@ -456,17 +456,15 @@ class SMTConv {
       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()))
-          // 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.
-          return OperandExp;
+      // When the operand is a bool expr, but the operator is an integeral
+      // operator, casting the bool expr to the integer before creating the
+      // unary operator.
+      // E.g. -(5 && a)
+      if (OperandTy == Ctx.BoolTy && OperandTy != *RetTy &&
----------------
steakhal wrote:

You are right. Fishy.

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