================
@@ -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
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
