diff --git a/libsolidity/formal/BMC.cpp b/libsolidity/formal/BMC.cpp
index 8fb5bfd30..dd1e5136c 100644
--- a/libsolidity/formal/BMC.cpp
+++ b/libsolidity/formal/BMC.cpp
@@ -441,26 +441,7 @@ void BMC::inlineFunctionCall(FunctionCall const& _funCall)
 	}
 	else
 	{
-		vector<smt::Expression> funArgs;
-		Expression const* calledExpr = &_funCall.expression();
-		auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
-		solAssert(funType, "");
-
-		auto const& functionParams = funDef->parameters();
-		auto const& arguments = _funCall.arguments();
-		unsigned firstParam = 0;
-		if (funType->bound())
-		{
-			auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
-			solAssert(boundFunction, "");
-			funArgs.push_back(expr(boundFunction->expression(), functionParams.front()->type()));
-			firstParam = 1;
-		}
-
-		solAssert((arguments.size() + firstParam) == functionParams.size(), "");
-		for (unsigned i = 0; i < arguments.size(); ++i)
-			funArgs.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
-		initializeFunctionCallParameters(*funDef, funArgs);
+		initializeFunctionCallParameters(*funDef, symbolicArguments(_funCall));
 
 		// The reason why we need to pushCallStack here instead of visit(FunctionDefinition)
 		// is that there we don't have `_funCall`.
diff --git a/libsolidity/formal/SMTEncoder.cpp b/libsolidity/formal/SMTEncoder.cpp
index 2c86eae0b..ac81a5d87 100644
--- a/libsolidity/formal/SMTEncoder.cpp
+++ b/libsolidity/formal/SMTEncoder.cpp
@@ -1682,3 +1682,31 @@ void SMTEncoder::createReturnedExpressions(FunctionCall const& _funCall)
 	else if (returnParams.size() == 1)
 		defineExpr(_funCall, currentValue(*returnParams.front()));
 }
+
+vector<smt::Expression> SMTEncoder::symbolicArguments(FunctionCall const& _funCall)
+{
+	auto const* function = functionCallToDefinition(_funCall);
+	solAssert(function, "");
+
+	vector<smt::Expression> args;
+	Expression const* calledExpr = &_funCall.expression();
+	auto const& funType = dynamic_cast<FunctionType const*>(calledExpr->annotation().type);
+	solAssert(funType, "");
+
+	auto const& functionParams = function->parameters();
+	auto const& arguments = _funCall.arguments();
+	unsigned firstParam = 0;
+	if (funType->bound())
+	{
+		auto const& boundFunction = dynamic_cast<MemberAccess const*>(calledExpr);
+		solAssert(boundFunction, "");
+		args.push_back(expr(boundFunction->expression(), functionParams.front()->type()));
+		firstParam = 1;
+	}
+
+	solAssert((arguments.size() + firstParam) == functionParams.size(), "");
+	for (unsigned i = 0; i < arguments.size(); ++i)
+		args.push_back(expr(*arguments.at(i), functionParams.at(i + firstParam)->type()));
+
+	return args;
+}
diff --git a/libsolidity/formal/SMTEncoder.h b/libsolidity/formal/SMTEncoder.h
index 3dbcaba6d..b0a672574 100644
--- a/libsolidity/formal/SMTEncoder.h
+++ b/libsolidity/formal/SMTEncoder.h
@@ -230,6 +230,11 @@ protected:
 	/// and set them as the components of the symbolic tuple.
 	void createReturnedExpressions(FunctionCall const& _funCall);
 
+	/// @returns the symbolic arguments for a function call,
+	/// taking into account bound functions and
+	/// type conversion.
+	std::vector<smt::Expression> symbolicArguments(FunctionCall const& _funCall);
+
 	/// @returns a note to be added to warnings.
 	std::string extraComment();