diff --git a/Changelog.md b/Changelog.md
index 5ce4057a4..eefabf7d6 100644
--- a/Changelog.md
+++ b/Changelog.md
@@ -8,6 +8,7 @@ Compiler Features:
 
 
 Bugfixes:
+ * SMTChecker: Fix internal error when using the custom NatSpec annotation to abstract free functions.
  * TypeChecker: Also allow external library functions in ``using for``.
 
 
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index c3286fa04..5c4fc5ded 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -2897,7 +2897,9 @@ vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedA
 
 vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
 {
-	return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
+	if (auto contract = dynamic_cast<ContractDefinition const*>(_function.scope()))
+		return stateVariablesIncludingInheritedAndPrivate(*contract);
+	return {};
 }
 
 vector<VariableDeclaration const*> SMTEncoder::localVariablesIncludingModifiers(FunctionDefinition const& _function, ContractDefinition const* _contract)
@@ -3020,14 +3022,6 @@ set<FunctionDefinition const*, ASTNode::CompareByID> const& SMTEncoder::contract
 	return m_contractFunctionsWithoutVirtual.at(&_contract);
 }
 
-SourceUnit const* SMTEncoder::sourceUnitContaining(Scopable const& _scopable)
-{
-	for (auto const* s = &_scopable; s; s = dynamic_cast<Scopable const*>(s->scope()))
-		if (auto const* source = dynamic_cast<SourceUnit const*>(s->scope()))
-			return source;
-	solAssert(false, "");
-}
-
 map<ContractDefinition const*, vector<ASTPointer<frontend::Expression>>> SMTEncoder::baseArguments(ContractDefinition const& _contract)
 {
 	map<ContractDefinition const*, vector<ASTPointer<Expression>>> baseArgs;
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 06b03a7eb..47e51b54d 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -113,9 +113,6 @@ public:
 	/// @returns the ModifierDefinition of a ModifierInvocation if possible, or nullptr.
 	static ModifierDefinition const* resolveModifierInvocation(ModifierInvocation const& _invocation, ContractDefinition const* _contract);
 
-	/// @returns the SourceUnit that contains _scopable.
-	static SourceUnit const* sourceUnitContaining(Scopable const& _scopable);
-
 	/// @returns the arguments for each base constructor call in the hierarchy of @a _contract.
 	std::map<ContractDefinition const*, std::vector<ASTPointer<frontend::Expression>>> baseArguments(ContractDefinition const& _contract);
 
diff --git a/test/libsolidity/smtCheckerTests/natspec/abstract_free_function_1.sol b/test/libsolidity/smtCheckerTests/natspec/abstract_free_function_1.sol
new file mode 100644
index 000000000..d01367059
--- /dev/null
+++ b/test/libsolidity/smtCheckerTests/natspec/abstract_free_function_1.sol
@@ -0,0 +1,17 @@
+// SPDX-License-Identifier: MIT
+pragma solidity >=0.8.13;
+
+contract C {
+    function f(uint x) external pure {
+        uint t = msb(x);
+        assert(t == 0); // should fail
+    }
+}
+
+/// @custom:smtchecker abstract-function-nondet
+function msb(uint256 x) pure returns (uint256 result) {}
+
+// ====
+// SMTEngine: chc
+// ----
+// Warning 6328: (144-158): CHC: Assertion violation happens here.