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

Donát Nagy via cfe-commits cfe-commits at lists.llvm.org
Sun Sep 21 13:24:38 PDT 2025


================
@@ -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()))
+          return getSymBinExpr(Solver, Ctx, BSE, hasComparison, RetTy);
----------------
NagyDonat wrote:

```suggestion
          return OperandExp;
```
Here you want to calculate the SMT expression (`SMTExprRef`) corresponding to the operand of the numerical negation (`UO_Minus`); but if I understand it correctly, this was already calculated and saved in the variable `OperandExp`.

Before accepting this suggestion, please validate whether it is correct – I'm writing this based on an intuitive understanding of the logic and didn't validate that `getSymExpr` would resolve to the same `getSymBinExpr` call that you call explicitly.  

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


More information about the cfe-commits mailing list