From 853175135ef64900ff9c054d4ce0e7cea147d6a5 Mon Sep 17 00:00:00 2001 From: Alex Beregszaszi Date: Wed, 23 Sep 2020 23:29:27 +0100 Subject: [PATCH] f --- libsolidity/formal/SMTEncoder.cpp | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp index 45e6d7eb9..e1d646766 100644 --- a/libsolidity/formal/SMTEncoder.cpp +++ b/libsolidity/formal/SMTEncoder.cpp @@ -664,6 +664,7 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) break; case FunctionType::Kind::Send: case FunctionType::Kind::Transfer: + case FunctionType::Kind::Selfdestruct: { auto const& memberAccess = dynamic_cast(_funCall.expression()); auto const& address = memberAccess.expression(); @@ -674,6 +675,10 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall) setSymbolicUnknownValue(thisBalance, TypeProvider::uint256(), m_context); m_context.state().transfer(m_context.state().thisAddress(), expr(address), expr(*value)); + + // Execution is stopped after selfdestruct. + if (funType.kind() == FunctionType::Kind::Selfdestruct) + addPathImplifiedExpression(smtutil::Expression(false)); break; } case FunctionType::Kind::ArrayPush: