diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index ea8ad765a..155b30b42 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -114,7 +114,7 @@ bool CHC::visit(ContractDefinition const& _contract)
 
 	initContract(_contract);
 
-	m_stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
+	m_stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
 	m_stateSorts = stateSorts(_contract);
 
 	clearIndices(&_contract);
@@ -738,24 +738,10 @@ set<frontend::Expression const*, CHC::IdCompare> CHC::transactionAssertions(ASTN
 	return assertions;
 }
 
-vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
-{
-	return fold(
-		_contract.annotation().linearizedBaseContracts,
-		vector<VariableDeclaration const*>{},
-		[](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); }
-	);
-}
-
-vector<VariableDeclaration const*> CHC::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
-{
-	return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
-}
-
 vector<smtutil::SortPointer> CHC::stateSorts(ContractDefinition const& _contract)
 {
 	return applyMap(
-		stateVariablesIncludingInheritedAndPrivate(_contract),
+		SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
 		[](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); }
 	);
 }
@@ -848,7 +834,7 @@ smtutil::SortPointer CHC::sort(ASTNode const* _node)
 
 smtutil::SortPointer CHC::summarySort(FunctionDefinition const& _function, ContractDefinition const& _contract)
 {
-	auto stateVariables = stateVariablesIncludingInheritedAndPrivate(_contract);
+	auto stateVariables = SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract);
 	auto sorts = stateSorts(_contract);
 
 	auto smtSort = [](auto _var) { return smt::smtSortAbstractFunction(*_var->type()); };
@@ -878,7 +864,7 @@ void CHC::defineInterfacesAndSummaries(SourceUnit const& _source)
 		if (auto const* contract = dynamic_cast<ContractDefinition const*>(node.get()))
 			for (auto const* base: contract->annotation().linearizedBaseContracts)
 			{
-				for (auto const* var: stateVariablesIncludingInheritedAndPrivate(*base))
+				for (auto const* var: SMTEncoder::stateVariablesIncludingInheritedAndPrivate(*base))
 					if (!m_context.knownVariable(*var))
 						createVariable(*var);
 
@@ -1048,7 +1034,7 @@ vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index)
 vector<smtutil::Expression> CHC::stateVariablesAtIndex(unsigned _index, ContractDefinition const& _contract)
 {
 	return applyMap(
-		stateVariablesIncludingInheritedAndPrivate(_contract),
+		SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract),
 		[&](auto _var) { return valueAtIndex(*_var, _index); }
 	);
 }
@@ -1061,7 +1047,7 @@ vector<smtutil::Expression> CHC::currentStateVariables()
 
 vector<smtutil::Expression> CHC::currentStateVariables(ContractDefinition const& _contract)
 {
-	return applyMap(stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
+	return applyMap(SMTEncoder::stateVariablesIncludingInheritedAndPrivate(_contract), [this](auto _var) { return currentValue(*_var); });
 }
 
 vector<smtutil::Expression> CHC::currentFunctionVariables()
diff --git a/libsolidity/formal/CHC.h b/libsolidity/formal/CHC.h
index 8b1c09a2b..619223388 100644
--- a/libsolidity/formal/CHC.h
+++ b/libsolidity/formal/CHC.h
@@ -111,8 +111,6 @@ private:
 	void clearIndices(ContractDefinition const* _contract, FunctionDefinition const* _function = nullptr) override;
 	void setCurrentBlock(Predicate const& _block, std::vector<smtutil::Expression> const* _arguments = nullptr);
 	std::set<Expression const*, IdCompare> transactionAssertions(ASTNode const* _txRoot);
-	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
-	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
 	//@}
 
 	/// Sort helpers.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 8cbed6712..306440e63 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1982,6 +1982,20 @@ FunctionDefinition const* SMTEncoder::functionCallToDefinition(FunctionCall cons
 	return funDef;
 }
 
+vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract)
+{
+	return fold(
+		_contract.annotation().linearizedBaseContracts,
+		vector<VariableDeclaration const*>{},
+		[](auto&& _acc, auto _contract) { return _acc + _contract->stateVariables(); }
+	);
+}
+
+vector<VariableDeclaration const*> SMTEncoder::stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function)
+{
+	return stateVariablesIncludingInheritedAndPrivate(dynamic_cast<ContractDefinition const&>(*_function.scope()));
+}
+
 void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
 {
 	FunctionDefinition const* funDef = functionCallToDefinition(_funCall);
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index fb5dce405..6e7388155 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -62,6 +62,9 @@ public:
 	/// if possible or nullptr.
 	static FunctionDefinition const* functionCallToDefinition(FunctionCall const& _funCall);
 
+	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(ContractDefinition const& _contract);
+	static std::vector<VariableDeclaration const*> stateVariablesIncludingInheritedAndPrivate(FunctionDefinition const& _function);
+
 protected:
 	// TODO: Check that we do not have concurrent reads and writes to a variable,
 	// because the order of expression evaluation is undefined