Merge pull request #11377 from ethereum/smt_cast_rational

[SMTChecker] Assign cast from constants directly
This commit is contained in:
Leonardo
2021-05-11 14:47:51 +02:00
committed by GitHub
+8
View File
@@ -1113,6 +1113,14 @@ void SMTEncoder::visitTypeConversion(FunctionCall const& _funCall)
{
solAssert(smt::isNumber(*funCallType), "");
RationalNumberType const* rationalType = isConstant(*argument);
if (rationalType)
{
// The TypeChecker guarantees that a constant fits in the cast size.
defineExpr(_funCall, symbArg);
return;
}
auto const* fixedCast = dynamic_cast<FixedBytesType const*>(funCallType);
auto const* fixedArg = dynamic_cast<FixedBytesType const*>(argType);
if (fixedCast && fixedArg)