From fc957ee59b5df92a27e55adc86da6ea097deaa19 Mon Sep 17 00:00:00 2001
From: Leo Alt <leo@ethereum.org>
Date: Sun, 15 May 2022 16:46:35 +0200
Subject: [PATCH] [SMTChecker] Support selfdestruct

---
 libsolidity/formal/CHC.cpp        |  1 +
 libsolidity/formal/SMTEncoder.cpp | 12 ++++++++++++
 libsolidity/formal/SMTEncoder.h   |  1 +
 3 files changed, 14 insertions(+)

diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 80a0852c9..d8e669a4d 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -602,6 +602,7 @@ void CHC::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::MulMod:
 	case FunctionType::Kind::Unwrap:
 	case FunctionType::Kind::Wrap:
+	case FunctionType::Kind::Selfdestruct:
 		[[fallthrough]];
 	default:
 		SMTEncoder::endVisit(_funCall);
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index a8d2ab04b..2ed43fb4a 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -714,6 +714,9 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 				" with the CHC engine."
 			);
 		break;
+	case FunctionType::Kind::Selfdestruct:
+		visitSelfDestruct(_funCall);
+		break;
 	case FunctionType::Kind::DelegateCall:
 	case FunctionType::Kind::BareCallCode:
 	case FunctionType::Kind::BareDelegateCall:
@@ -917,6 +920,15 @@ void SMTEncoder::visitObjectCreation(FunctionCall const& _funCall)
 	m_context.addAssertion(symbArray->elements() == zeroElements);
 }
 
+void SMTEncoder::visitSelfDestruct(FunctionCall const& _funCall)
+{
+	auto const& args = _funCall.arguments();
+	solAssert(args.size() == 1);
+	solAssert(args.at(0));
+
+	state().transfer(state().thisAddress(), expr(*args.at(0)), state().balance(state().thisAddress()));
+}
+
 void SMTEncoder::endVisit(Identifier const& _identifier)
 {
 	if (auto decl = identifierToVariable(_identifier))
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index e81af6d4d..7a475f230 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -216,6 +216,7 @@ protected:
 	virtual void visitAddMulMod(FunctionCall const& _funCall);
 	void visitWrapUnwrap(FunctionCall const& _funCall);
 	void visitObjectCreation(FunctionCall const& _funCall);
+	void visitSelfDestruct(FunctionCall const& _funCall);
 	void visitTypeConversion(FunctionCall const& _funCall);
 	void visitStructConstructorCall(FunctionCall const& _funCall);
 	void visitFunctionIdentifier(Identifier const& _identifier);