================
@@ -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()))
----------------
NagyDonat wrote:
```suggestion
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.
```
I like that you documented this situation in the test file, and a determined
reader would be able to find that (by checking git blame), but let's also
document this logic here for the lazier readers :)
(Feel free to tweak my suggested comment if you think that you can improve it.)
https://github.com/llvm/llvm-project/pull/158276
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
