================
@@ -270,8 +274,14 @@ class SMTConv {
QualType ToTy, uint64_t ToBitWidth,
QualType FromTy,
uint64_t FromBitWidth) {
- if ((FromTy.getAtomicUnqualifiedType()->isIntegralOrEnumerationType() &&
- ToTy.getAtomicUnqualifiedType()->isIntegralOrEnumerationType()) ||
+ FromTy = getSymbolicValueType(FromTy);
+ ToTy = getSymbolicValueType(ToTy);
+
+ if (FromTy == ToTy && FromBitWidth == ToBitWidth)
+ return Exp;
----------------
rdevshp wrote:
When FromTy->isBooleanType() && ToTy->isBooleanType(), the code returns
```
return Solver->mkIte(
Exp, Solver->mkBitvector(llvm::APSInt("1"), ToBitWidth),
Solver->mkBitvector(llvm::APSInt("0"), ToBitWidth));
```
which does not have the correct Z3 sort (should have Z3 sort Boolean and not
bitvector). The early return bypasses this and skips the cast. The type
canonicalization was there to make sure that the cast is correctly skipped in
this case.
https://github.com/llvm/llvm-project/pull/212050
_______________________________________________
cfe-commits mailing list
[email protected]
https://lists.llvm.org/cgi-bin/mailman/listinfo/cfe-commits
