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

via cfe-commits cfe-commits at lists.llvm.org
Sat Sep 13 03:46:24 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);
+      }
----------------
vabridgers wrote:

Hi @NagyDonat , you're correct. This particular workaround approach could be a bit more narrow. I'll work on that. 

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


More information about the cfe-commits mailing list