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

DonĂ¡t Nagy via cfe-commits cfe-commits at lists.llvm.org
Fri Sep 12 05:59:03 PDT 2025


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

This seems to be triggered for all unary operators (and not just negation). Is this intentional?

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


More information about the cfe-commits mailing list