diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index 267ea9269..414ab3311 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -174,6 +174,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	smtutil::Expression zeroes(true);
 	for (auto var: stateVariablesIncludingInheritedAndPrivate(_contract))
 		zeroes = zeroes && currentValue(*var) == smt::zeroValue(var->type());
+	zeroes = zeroes && state().destructedFlag() == 0;
 	// The contract's address might already have funds before deployment,
 	// so the balance must be at least `msg.value`, but not equals.
 	auto initialBalanceConstraint = state().balance(state().thisAddress()) >= state().txMember("msg.value");
@@ -214,9 +215,12 @@ void CHC::endVisit(ContractDefinition const& _contract)
 	for (auto base: _contract.annotation().linearizedBaseContracts | ranges::views::reverse)
 	{
 		errorFlag().increaseIndex();
+		auto destructedPre = state().destructedFlag();
 		m_context.addAssertion(smt::constructorCall(*m_contractInitializers.at(&_contract).at(base), m_context));
 		connectBlocks(m_currentBlock, summary(_contract), errorFlag().currentValue() > 0);
+		auto destructedPost = state().destructedFlag();
 		m_context.addAssertion(errorFlag().currentValue() == 0);
+		m_context.addAssertion(state().newDestructedFlag() == destructedPre + destructedPost);
 	}
 
 	connectBlocks(m_currentBlock, summary(_contract));
@@ -231,7 +235,7 @@ void CHC::endVisit(ContractDefinition const& _contract)
 		if (!constructor || !constructor->isPayable())
 			txConstraints = txConstraints && state().txNonPayableConstraint();
 		m_queryPlaceholders[&_contract].push_back({txConstraints, errorFlag().currentValue(), m_currentBlock});
-		connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0);
+		connectBlocks(m_currentBlock, interface(), txConstraints && errorFlag().currentValue() == 0 && state().destructedFlag() == 0);
 	}
 
 	solAssert(m_scopes.back() == &_contract, "");
@@ -258,7 +262,7 @@ bool CHC::visit(FunctionDefinition const& _function)
 		)
 			conj = conj && currentEqualInitialVarsConstraints(stateVariablesIncludingInheritedAndPrivate(_function));
 
-		conj = conj && errorFlag().currentValue() == 0;
+		conj = conj && errorFlag().currentValue() == 0 && state().destructedFlag() == 0;
 		addRule(smtutil::Expression::implies(conj, summary(_function)), "summary_function_" + to_string(_function.id()));
 		return false;
 	}
@@ -335,7 +339,7 @@ void CHC::endVisit(FunctionDefinition const& _function)
 		auto sum = externalSummary(_function);
 
 		m_queryPlaceholders[&_function].push_back({sum, errorFlag().currentValue(), ifacePre});
-		connectBlocks(ifacePre, interface(), sum && errorFlag().currentValue() == 0);
+		connectBlocks(ifacePre, interface(), sum && errorFlag().currentValue() == 0 && state().destructedFlag(0) == 0);
 	}
 
 	m_currentFunction = nullptr;
@@ -565,6 +569,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);
@@ -738,6 +743,8 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 			m_callGraph[m_currentContract].insert(function);
 	}
 
+	auto destructedPre = state().destructedFlag();
+
 	m_context.addAssertion(predicate(_funCall));
 
 	solAssert(m_errorDest, "");
@@ -747,6 +754,8 @@ void CHC::internalFunctionCall(FunctionCall const& _funCall)
 		errorFlag().currentValue() > 0
 	);
 	m_context.addAssertion(errorFlag().currentValue() == 0);
+	auto destructedPost = state().destructedFlag();
+	m_context.addAssertion(state().newDestructedFlag() == destructedPre + destructedPost);
 }
 
 void CHC::externalFunctionCall(FunctionCall const& _funCall)
@@ -811,6 +820,8 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 	}
 
 	auto error = errorFlag().increaseIndex();
+	auto destructedPre = state().destructedFlag();
+	auto destructedPost = state().newDestructedFlag();
 
 	Predicate const& callPredicate = *createSymbolicBlock(
 		nondetInterfaceSort(*m_currentContract, state()),
@@ -819,7 +830,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 		&_funCall
 	);
 	auto postCallState = vector<smtutil::Expression>{state().state()} + currentStateVariables();
-	vector<smtutil::Expression> stateExprs{error, state().thisAddress(), state().abi(), state().crypto()};
+	vector<smtutil::Expression> stateExprs{error, destructedPost, state().thisAddress(), state().abi(), state().crypto()};
 
 	auto nondet = (*m_nondetInterfaces.at(m_currentContract))(stateExprs + preCallState + postCallState);
 	auto nondetCall = callPredicate(stateExprs + preCallState + postCallState);
@@ -838,6 +849,7 @@ void CHC::externalFunctionCall(FunctionCall const& _funCall)
 				m_callGraph[m_currentFunction].insert(definedFunction);
 
 	m_context.addAssertion(errorFlag().currentValue() == 0);
+	m_context.addAssertion(state().newDestructedFlag() == destructedPre + destructedPost);
 }
 
 void CHC::externalFunctionCallToTrustedCode(FunctionCall const& _funCall)
@@ -1176,11 +1188,17 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 					auto state2 = stateVariablesAtIndex(2, *contract);
 
 					auto errorPre = errorFlag().currentValue();
+					auto destructedPre = state().destructedFlag();
 					auto nondetPre = smt::nondetInterface(iface, *contract, m_context, 0, 1);
+
 					auto errorPost = errorFlag().increaseIndex();
+					auto destructedPost = state().newDestructedFlag();
 					auto nondetPost = smt::nondetInterface(iface, *contract, m_context, 0, 2);
 
-					vector<smtutil::Expression> args{errorPost, state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
+					auto destructedSummary = state().newDestructedFlag();
+					m_context.addAssertion(destructedPost == destructedPre + destructedSummary);
+
+					vector<smtutil::Expression> args{errorPost, destructedPre + destructedPost, state().thisAddress(), state().abi(), state().crypto(), state().tx(), state().state(1)};
 					args += state1 +
 						applyMap(function->parameters(), [this](auto _var) { return valueAtIndex(*_var, 0); }) +
 						vector<smtutil::Expression>{state().state(2)} +
@@ -1218,6 +1236,7 @@ void CHC::defineExternalFunctionInterface(FunctionDefinition const& _function, C
 	state().addBalance(state().thisAddress(), k.currentValue());
 
 	errorFlag().increaseIndex();
+	state().newDestructedFlag();
 	m_context.addAssertion(summaryCall(_function));
 
 	connectBlocks(functionPred, externalSummary(_function));
@@ -1249,9 +1268,13 @@ void CHC::defineContractInitializer(ContractDefinition const& _contract, Contrac
 	if (auto constructor = _contract.constructor())
 	{
 		errorFlag().increaseIndex();
+		auto destructedPre = state().destructedFlag();
+		state().newDestructedFlag();
 		m_context.addAssertion(smt::functionCall(*m_summaries.at(&_contextContract).at(constructor), &_contextContract, m_context));
 		connectBlocks(m_currentBlock, initializer(_contract, _contextContract), errorFlag().currentValue() > 0);
 		m_context.addAssertion(errorFlag().currentValue() == 0);
+		auto destructedPost = state().destructedFlag();
+		m_context.addAssertion(state().newDestructedFlag() == destructedPre + destructedPost);
 	}
 
 	connectBlocks(m_currentBlock, initializer(_contract, _contextContract));
@@ -1495,7 +1518,7 @@ smtutil::Expression CHC::predicate(FunctionCall const& _funCall)
 		solAssert(false, "Unreachable!");
 	};
 	errorFlag().increaseIndex();
-	vector<smtutil::Expression> args{errorFlag().currentValue(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};
+	vector<smtutil::Expression> args{errorFlag().currentValue(), state().newDestructedFlag(), contractAddressValue(_funCall), state().abi(), state().crypto(), state().tx(), state().state()};
 
 	auto const* contract = function->annotation().contract;
 	auto const& hierarchy = m_currentContract->annotation().linearizedBaseContracts;
diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp
index 91513a00c..565d77e4a 100644
--- a/libsolidity/formal/Predicate.cpp
+++ b/libsolidity/formal/Predicate.cpp
@@ -272,7 +272,7 @@ string Predicate::formatSummaryCall(
 		}
 
 		// Here we are interested in txData from the summary predicate.
-		auto txValues = readTxVars(_args.at(4));
+		auto txValues = readTxVars(_args.at(5));
 		vector<string> values;
 		for (auto const& _var: txVars)
 			if (auto v = txValues.at(_var))
@@ -290,7 +290,7 @@ string Predicate::formatSummaryCall(
 	auto const* fun = programFunction();
 	solAssert(fun, "");
 
-	auto first = _args.begin() + 6 + static_cast<int>(stateVars->size());
+	auto first = _args.begin() + 7 + static_cast<int>(stateVars->size());
 	auto last = first + static_cast<int>(fun->parameters().size());
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 	solAssert(last >= _args.begin() && last <= _args.end(), "");
@@ -334,12 +334,12 @@ vector<optional<string>> Predicate::summaryStateValues(vector<smtutil::Expressio
 	vector<smtutil::Expression>::const_iterator stateLast;
 	if (auto const* function = programFunction())
 	{
-		stateFirst = _args.begin() + 6 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
+		stateFirst = _args.begin() + 7 + static_cast<int>(stateVars->size()) + static_cast<int>(function->parameters().size()) + 1;
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
 	else if (programContract())
 	{
-		stateFirst = _args.begin() + 7 + static_cast<int>(stateVars->size());
+		stateFirst = _args.begin() + 8 + static_cast<int>(stateVars->size());
 		stateLast = stateFirst + static_cast<int>(stateVars->size());
 	}
 	else
@@ -366,7 +366,7 @@ vector<optional<string>> Predicate::summaryPostInputValues(vector<smtutil::Expre
 
 	auto const& inParams = function->parameters();
 
-	auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
+	auto first = _args.begin() + 7 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) + 1;
 	auto last = first + static_cast<int>(inParams.size());
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
@@ -390,7 +390,7 @@ vector<optional<string>> Predicate::summaryPostOutputValues(vector<smtutil::Expr
 
 	auto const& inParams = function->parameters();
 
-	auto first = _args.begin() + 6 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
+	auto first = _args.begin() + 7 + static_cast<int>(stateVars->size()) * 2 + static_cast<int>(inParams.size()) * 2 + 1;
 
 	solAssert(first >= _args.begin() && first <= _args.end(), "");
 
@@ -443,10 +443,10 @@ map<string, string> Predicate::expressionSubstitution(smtutil::Expression const&
 	if (isInterface())
 	{
 		solAssert(starts_with(predName, "interface"), "");
-		subst[_predExpr.arguments.at(0).name] = "address(this)";
-		solAssert(nArgs == stateVars.size() + 4, "");
+		subst[_predExpr.arguments.at(1).name] = "address(this)";
+		solAssert(nArgs == stateVars.size() + 5, "");
 		for (size_t i = nArgs - stateVars.size(); i < nArgs; ++i)
-			subst[_predExpr.arguments.at(i).name] = stateVars.at(i - 4)->name();
+			subst[_predExpr.arguments.at(i).name] = stateVars.at(i - 5)->name();
 	}
 	// The signature of a nondet interface predicate is
 	// nondet_interface(error, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
@@ -459,8 +459,8 @@ map<string, string> Predicate::expressionSubstitution(smtutil::Expression const&
 	{
 		solAssert(starts_with(predName, "nondet_interface"), "");
 		subst[_predExpr.arguments.at(0).name] = "<errorCode>";
-		subst[_predExpr.arguments.at(1).name] = "address(this)";
-		solAssert(nArgs == stateVars.size() * 2 + 6, "");
+		subst[_predExpr.arguments.at(2).name] = "address(this)";
+		solAssert(nArgs == stateVars.size() * 2 + 7, "");
 		for (size_t i = nArgs - stateVars.size(), s = 0; i < nArgs; ++i, ++s)
 			subst[_predExpr.arguments.at(i).name] = stateVars.at(s)->name() + "'";
 		for (size_t i = nArgs - (stateVars.size() * 2 + 1), s = 0; i < nArgs - (stateVars.size() + 1); ++i, ++s)
diff --git a/libsolidity/formal/PredicateInstance.cpp b/libsolidity/formal/PredicateInstance.cpp
index aff6aa19b..c41392d8b 100644
--- a/libsolidity/formal/PredicateInstance.cpp
+++ b/libsolidity/formal/PredicateInstance.cpp
@@ -30,14 +30,14 @@ namespace solidity::frontend::smt
 smtutil::Expression interfacePre(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state(0)};
+	vector<smtutil::Expression> stateExprs{state.destructedFlag(0), state.thisAddress(0), state.abi(0), state.crypto(0), state.state(0)};
 	return _pred(stateExprs + initialStateVariables(_contract, _context));
 }
 
 smtutil::Expression interface(Predicate const& _pred, ContractDefinition const& _contract, EncodingContext& _context)
 {
 	auto const& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.thisAddress(0), state.abi(0), state.crypto(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.destructedFlag(), state.thisAddress(0), state.abi(0), state.crypto(0), state.state()};
 	return _pred(stateExprs + currentStateVariables(_contract, _context));
 }
 
@@ -49,7 +49,7 @@ smtutil::Expression nondetInterface(
 	unsigned _postIdx)
 {
 	auto const& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(), state.abi(), state.crypto()};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.destructedFlag(), state.thisAddress(), state.abi(), state.crypto()};
 	return _pred(
 		stateExprs +
 		vector<smtutil::Expression>{_context.state().state(_preIdx)} +
@@ -66,7 +66,7 @@ smtutil::Expression constructor(Predicate const& _pred, EncodingContext& _contex
 		return _pred(currentFunctionVariablesForDefinition(*constructor, &contract, _context));
 
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.destructedFlag(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0), state.state()};
 	return _pred(stateExprs + initialStateVariables(contract, _context) + currentStateVariables(contract, _context));
 }
 
@@ -77,7 +77,7 @@ smtutil::Expression constructorCall(Predicate const& _pred, EncodingContext& _co
 		return _pred(currentFunctionVariablesForCall(*constructor, &contract, _context));
 
 	auto& state = _context.state();
-	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
+	vector<smtutil::Expression> stateExprs{state.errorFlag().currentValue(), state.destructedFlag(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
 	state.newState();
 	stateExprs += vector<smtutil::Expression>{state.state()};
 	stateExprs += currentStateVariables(contract, _context);
@@ -153,7 +153,7 @@ vector<smtutil::Expression> currentFunctionVariablesForDefinition(
 )
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0)};
+	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.destructedFlag(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state(0)};
 	exprs += _contract ? initialStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->valueAtIndex(0); });
 	exprs += vector<smtutil::Expression>{state.state()};
@@ -170,7 +170,7 @@ vector<smtutil::Expression> currentFunctionVariablesForCall(
 )
 {
 	auto& state = _context.state();
-	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
+	vector<smtutil::Expression> exprs{state.errorFlag().currentValue(), state.destructedFlag(), state.thisAddress(0), state.abi(0), state.crypto(0), state.tx(0), state.state()};
 	exprs += _contract ? currentStateVariables(*_contract, _context) : vector<smtutil::Expression>{};
 	exprs += applyMap(_function.parameters(), [&](auto _var) { return _context.variable(*_var)->currentValue(); });
 
diff --git a/libsolidity/formal/PredicateSort.cpp b/libsolidity/formal/PredicateSort.cpp
index dc134766d..7f1936866 100644
--- a/libsolidity/formal/PredicateSort.cpp
+++ b/libsolidity/formal/PredicateSort.cpp
@@ -31,7 +31,7 @@ namespace solidity::frontend::smt
 SortPointer interfaceSort(ContractDefinition const& _contract, SymbolicState& _state)
 {
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
+		vector<SortPointer>{_state.destructedFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.stateSort()} + stateSorts(_contract),
 		SortProvider::boolSort
 	);
 }
@@ -41,7 +41,7 @@ SortPointer nondetInterfaceSort(ContractDefinition const& _contract, SymbolicSta
 	auto varSorts = stateSorts(_contract);
 	vector<SortPointer> stateSort{_state.stateSort()};
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} +
+		vector<SortPointer>{_state.errorFlagSort(), _state.destructedFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort()} +
 			stateSort +
 			varSorts +
 			stateSort +
@@ -58,7 +58,7 @@ SortPointer constructorSort(ContractDefinition const& _contract, SymbolicState&
 	auto varSorts = stateSorts(_contract);
 	vector<SortPointer> stateSort{_state.stateSort()};
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
+		vector<SortPointer>{_state.errorFlagSort(), _state.destructedFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort(), _state.stateSort()} + varSorts + varSorts,
 		SortProvider::boolSort
 	);
 }
@@ -70,7 +70,7 @@ SortPointer functionSort(FunctionDefinition const& _function, ContractDefinition
 	auto inputSorts = applyMap(_function.parameters(), smtSort);
 	auto outputSorts = applyMap(_function.returnParameters(), smtSort);
 	return make_shared<FunctionSort>(
-		vector<SortPointer>{_state.errorFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
+		vector<SortPointer>{_state.errorFlagSort(), _state.destructedFlagSort(), _state.thisAddressSort(), _state.abiSort(), _state.cryptoSort(), _state.txSort(), _state.stateSort()} +
 			varSorts +
 			inputSorts +
 			vector<SortPointer>{_state.stateSort()} +
diff --git a/libsolidity/formal/PredicateSort.h b/libsolidity/formal/PredicateSort.h
index 563858254..5382b3493 100644
--- a/libsolidity/formal/PredicateSort.h
+++ b/libsolidity/formal/PredicateSort.h
@@ -33,25 +33,25 @@ namespace solidity::frontend::smt
  *
  * 1. Interface
  * The idle state of a contract. Signature:
- * interface(this, abiFunctions, cryptoFunctions, blockchainState, stateVariables).
+ * interface(destructed, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables).
  *
  * 2. Nondet interface
  * The nondeterminism behavior of a contract. Signature:
- * nondet_interface(error, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
+ * nondet_interface(error, destructed, this, abiFunctions, cryptoFunctions, blockchainState, stateVariables, blockchainState', stateVariables').
  *
  * 3. Constructor entry/summary
  * The summary of a contract's deployment procedure.
  * Signature:
  * If the contract has a constructor function, this is the same as the summary of that function. Otherwise:
- * constructor_summary(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables').
+ * constructor_summary(error, destructed, this, abiFunctions, cryptoFunctions, txData, blockchainState, blockchainState', stateVariables, stateVariables').
  *
  * 4. Function entry/summary
  * The entry point of a function definition. Signature:
- * function_entry(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
+ * function_entry(error, destructed, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables').
  *
  * 5. Function body
  * Use for any predicate within a function. Signature:
- * function_body(error, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables).
+ * function_body(error, destructed, this, abiFunctions, cryptoFunctions, txData, blockchainState, stateVariables, inputVariables, blockchainState', stateVariables', inputVariables', outputVariables', localVariables).
  */
 
 /// @returns the interface predicate sort for _contract.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 8c5dd647e..2e860311c 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -705,6 +705,9 @@ void SMTEncoder::endVisit(FunctionCall const& _funCall)
 	case FunctionType::Kind::ObjectCreation:
 		visitObjectCreation(_funCall);
 		return;
+	case FunctionType::Kind::Selfdestruct:
+		visitSelfDestruct(_funCall);
+		break;
 	case FunctionType::Kind::DelegateCall:
 	case FunctionType::Kind::BareCallCode:
 	case FunctionType::Kind::BareDelegateCall:
@@ -909,6 +912,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 888bd6a3d..ef4dc35bd 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);
diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp
index b1fd7978f..1069f4be1 100644
--- a/libsolidity/formal/SymbolicState.cpp
+++ b/libsolidity/formal/SymbolicState.cpp
@@ -74,6 +74,7 @@ smtutil::Expression BlockchainVariable::assignMember(string const& _member, smtu
 void SymbolicState::reset()
 {
 	m_error.resetIndex();
+	m_destructed.resetIndex();
 	m_thisAddress.resetIndex();
 	m_state.reset();
 	m_tx.reset();
diff --git a/libsolidity/formal/SymbolicState.h b/libsolidity/formal/SymbolicState.h
index 309d545b8..7d55a309e 100644
--- a/libsolidity/formal/SymbolicState.h
+++ b/libsolidity/formal/SymbolicState.h
@@ -59,6 +59,7 @@ private:
 /**
  * Symbolic representation of the blockchain context:
  * - error flag
+ * - destructed (0: non-destructed, 1: destructed, 2: pending destruction)
  * - this (the address of the currently executing contract)
  * - state, represented as a tuple of:
  *   - balances
@@ -94,6 +95,14 @@ public:
 	smtutil::SortPointer const& errorFlagSort() const { return m_error.sort(); }
 	//@}
 
+	/// Destructed flag.
+	//@{
+	smtutil::Expression destructedFlag() const { return m_destructed.currentValue(); }
+	smtutil::Expression destructedFlag(unsigned _idx) const { return m_destructed.valueAtIndex(_idx); }
+	smtutil::Expression newDestructedFlag() { return m_destructed.increaseIndex(); }
+	smtutil::SortPointer const& destructedFlagSort() const { return m_destructed.sort(); }
+	//@}
+
 	/// This.
 	//@{
 	/// @returns the symbolic value of the currently executing contract's address.
@@ -180,6 +189,13 @@ private:
 		m_context
 	};
 
+	SymbolicIntVariable m_destructed{
+		TypeProvider::uint256(),
+		TypeProvider::uint256(),
+		"destructed",
+		m_context
+	};
+
 	SymbolicAddressVariable m_thisAddress{
 		"this",
 		m_context