cerc-io/solidity
11
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Fix ICE on tuples of one element that actually have tuple type

Browse Source
This commit is contained in:
Leonardo Alt
2020-09-01 08:31:57 +02:00
parent 5cafbeebec
commit 238b8a929e
3 changed files with 19 additions and 8 deletions
Download Patch File Download Diff File Expand all files Collapse all files
libsolidity/formal/SMTEncoder.cpp
+4 -8
View File
@@ -420,8 +420,11 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
_tuple.location(),
"Assertion checker does not yet implement inline arrays."
);
else if (_tuple.annotation().type->category() == Type::Category::Tuple)
else if (_tuple.components().size() == 1)
defineExpr(_tuple, expr(*_tuple.components().front()));
else
{
solAssert(_tuple.annotation().type->category() == Type::Category::Tuple, "");
auto const& symbTuple = dynamic_pointer_cast<smt::SymbolicTupleVariable>(m_context.expression(_tuple));
solAssert(symbTuple, "");
auto const& symbComponents = symbTuple->components();
@@ -445,13 +448,6 @@ void SMTEncoder::endVisit(TupleExpression const& _tuple)
}
}
}
else
{
/// Parenthesized expressions are also TupleExpression regardless their type.
auto const& components = _tuple.components();
solAssert(components.size() == 1, "");
defineExpr(_tuple, expr(*components.front()));
}
}
void SMTEncoder::endVisit(UnaryOperation const& _op)