diff --git a/libsolidity/formal/ExpressionFormatter.cpp b/libsolidity/formal/ExpressionFormatter.cpp
new file mode 100644
index 000000000..2591328f8
--- /dev/null
+++ b/libsolidity/formal/ExpressionFormatter.cpp
@@ -0,0 +1,184 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#include <libsolidity/formal/ExpressionFormatter.h>
+
+#include <libsolutil/Algorithms.h>
+#include <libsolutil/CommonData.h>
+
+#include <boost/algorithm/string.hpp>
+
+#include <range/v3/algorithm/for_each.hpp>
+
+#include <map>
+#include <vector>
+#include <string>
+
+using namespace std;
+using boost::algorithm::starts_with;
+using namespace solidity;
+using namespace solidity::util;
+using namespace solidity::smtutil;
+using namespace solidity::frontend::smt;
+
+namespace solidity::frontend::smt
+{
+
+namespace
+{
+
+string formatDatatypeAccessor(smtutil::Expression const& _expr, vector<string> const& _args)
+{
+	auto const& op = _expr.name;
+
+	// This is the most complicated part of the translation.
+	// Datatype accessor means access to a field of a datatype.
+	// In our encoding, datatypes are used to encode:
+	// - arrays/mappings as the tuple (array, length)
+	// - structs as the tuple (<member1>, ..., <memberK>)
+	// - hash and signature functions as the tuple (keccak256, sha256, ripemd160, ecrecover),
+	//   where each element is an array emulating an UF
+	// - abi.* functions as the tuple (<abiCall1>, ..., <abiCallK>).
+	if (op == "dt_accessor_keccak256")
+		return "keccak256";
+	if (op == "dt_accessor_sha256")
+		return "sha256";
+	if (op == "dt_accessor_ripemd160")
+		return "ripemd160";
+	if (op == "dt_accessor_ecrecover")
+		return "ecrecover";
+
+	string accessorStr = "accessor_";
+	// Struct members have suffix "accessor_<memberName>".
+	string type = op.substr(op.rfind(accessorStr) + accessorStr.size());
+	solAssert(_expr.arguments.size() == 1, "");
+
+	if (type == "length")
+		return _args.at(0) + ".length";
+	if (type == "array")
+		return _args.at(0);
+
+	if (
+		starts_with(type, "block") ||
+		starts_with(type, "msg") ||
+		starts_with(type, "tx") ||
+		starts_with(type, "abi")
+	)
+		return type;
+
+	if (starts_with(type, "t_function_abi"))
+		return type;
+
+	return _args.at(0) + "." + type;
+}
+
+string formatGenericOp(smtutil::Expression const& _expr, vector<string> const& _args)
+{
+	return _expr.name + "(" + boost::algorithm::join(_args, ", ") + ")";
+}
+
+string formatInfixOp(string const& _op, vector<string> const& _args)
+{
+	return "(" + boost::algorithm::join(_args, " " + _op + " ") + ")";
+}
+
+string formatArrayOp(smtutil::Expression const& _expr, vector<string> const& _args)
+{
+	if (_expr.name == "select")
+	{
+		auto const& a0 = _args.at(0);
+		static set<string> const ufs{"keccak256", "sha256", "ripemd160", "ecrecover"};
+		if (ufs.count(a0) || starts_with(a0, "t_function_abi"))
+			return _args.at(0) + "(" + _args.at(1) + ")";
+		return _args.at(0) + "[" + _args.at(1) + "]";
+	}
+	if (_expr.name == "store")
+		return "(" + _args.at(0) + "[" + _args.at(1) + "] := " + _args.at(2) + ")";
+	return formatGenericOp(_expr, _args);
+}
+
+string formatUnaryOp(smtutil::Expression const& _expr, vector<string> const& _args)
+{
+	if (_expr.name == "not")
+		return "!" + _args.at(0);
+	// Other operators such as exists may end up here.
+	return formatGenericOp(_expr, _args);
+}
+
+}
+
+smtutil::Expression substitute(smtutil::Expression _from, map<string, string> const& _subst)
+{
+	// TODO For now we ignore nested quantifier expressions,
+	// but we should support them in the future.
+	if (_from.name == "forall" || _from.name == "exists")
+		return smtutil::Expression(true);
+	if (_subst.count(_from.name))
+		_from.name = _subst.at(_from.name);
+	for (auto& arg: _from.arguments)
+		arg = substitute(arg, _subst);
+	return _from;
+}
+
+string toSolidityStr(smtutil::Expression const& _expr)
+{
+	auto const& op = _expr.name;
+
+	auto const& args = _expr.arguments;
+	auto strArgs = util::applyMap(args, [](auto const& _arg) { return toSolidityStr(_arg); });
+
+	// Constant or variable.
+	if (args.empty())
+		return op;
+
+	if (starts_with(op, "dt_accessor"))
+		return formatDatatypeAccessor(_expr, strArgs);
+
+	// Infix operators with format replacements.
+	static map<string, string> const infixOps{
+		{"and", "&&"},
+		{"or", "||"},
+		{"implies", "=>"},
+		{"=", "="},
+		{">", ">"},
+		{">=", ">="},
+		{"<", "<"},
+		{"<=", "<="},
+		{"+", "+"},
+		{"-", "-"},
+		{"*", "*"},
+		{"/", "/"},
+		{"div", "/"},
+		{"mod", "%"}
+	};
+	// Some of these (and, or, +, *) may have >= 2 arguments from z3.
+	if (infixOps.count(op))
+		return formatInfixOp(infixOps.at(op), strArgs);
+
+	static set<string> const arrayOps{"select", "store", "const_array"};
+	if (arrayOps.count(op))
+		return formatArrayOp(_expr, strArgs);
+
+	if (args.size() == 1)
+		return formatUnaryOp(_expr, strArgs);
+
+	// Other operators such as bv2int, int2bv may end up here.
+	return op + "(" + boost::algorithm::join(strArgs, ", ") + ")";
+}
+
+}
diff --git a/libsolidity/formal/ExpressionFormatter.h b/libsolidity/formal/ExpressionFormatter.h
new file mode 100644
index 000000000..3efbeb781
--- /dev/null
+++ b/libsolidity/formal/ExpressionFormatter.h
@@ -0,0 +1,41 @@
+/*
+	This file is part of solidity.
+
+	solidity is free software: you can redistribute it and/or modify
+	it under the terms of the GNU General Public License as published by
+	the Free Software Foundation, either version 3 of the License, or
+	(at your option) any later version.
+
+	solidity is distributed in the hope that it will be useful,
+	but WITHOUT ANY WARRANTY; without even the implied warranty of
+	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+	GNU General Public License for more details.
+
+	You should have received a copy of the GNU General Public License
+	along with solidity.  If not, see <http://www.gnu.org/licenses/>.
+*/
+// SPDX-License-Identifier: GPL-3.0
+
+#pragma once
+
+/**
+ * Formats SMT expressions into Solidity-like strings.
+ */
+
+#include <libsolidity/formal/Predicate.h>
+
+#include <map>
+#include <string>
+
+namespace solidity::frontend::smt
+{
+
+/// @returns another smtutil::Expressions where every term in _from
+/// may be replaced if it is in the substitution map _subst.
+smtutil::Expression substitute(smtutil::Expression _from, std::map<std::string, std::string> const& _subst);
+
+/// @returns a Solidity-like expression string built from _expr.
+/// This is done at best-effort and is not guaranteed to always create a perfect Solidity expression string.
+std::string toSolidityStr(smtutil::Expression const& _expr);
+
+}