diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp
index 630eb0619..fb2423e5a 100644
--- a/libsmtutil/CHCSmtLib2Interface.cpp
+++ b/libsmtutil/CHCSmtLib2Interface.cpp
@@ -16,12 +16,16 @@
 */
 // SPDX-License-Identifier: GPL-3.0
 
+#include <boost/filesystem/operations.hpp>
 #include <libsmtutil/CHCSmtLib2Interface.h>
 
 #include <libsolutil/Keccak256.h>
 
 #include <boost/algorithm/string/join.hpp>
 #include <boost/algorithm/string/predicate.hpp>
+#include <boost/filesystem.hpp>
+#include <boost/filesystem/fstream.hpp>
+#include <boost/process.hpp>
 
 #include <range/v3/view.hpp>
 
@@ -40,12 +44,14 @@ using namespace solidity::smtutil;
 CHCSmtLib2Interface::CHCSmtLib2Interface(
 	map<h256, string> const& _queryResponses,
 	ReadCallback::Callback _smtCallback,
+	SMTSolverChoice _enabledSolvers,
 	optional<unsigned> _queryTimeout
 ):
 	CHCSolverInterface(_queryTimeout),
 	m_smtlib2(make_unique<SMTLib2Interface>(_queryResponses, _smtCallback, m_queryTimeout)),
 	m_queryResponses(move(_queryResponses)),
-	m_smtCallback(_smtCallback)
+	m_smtCallback(_smtCallback),
+	m_enabledSolvers(_enabledSolvers)
 {
 	reset();
 }
@@ -203,12 +209,46 @@ string CHCSmtLib2Interface::querySolver(string const& _input)
 	util::h256 inputHash = util::keccak256(_input);
 	if (m_queryResponses.count(inputHash))
 		return m_queryResponses.at(inputHash);
-	if (m_smtCallback)
+
+	if (m_enabledSolvers.smtlib2 && m_smtCallback)
 	{
 		auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery), _input);
 		if (result.success)
 			return result.responseOrErrorMessage;
 	}
+
+	if (m_enabledSolvers.eld)
+	{
+		auto tempDir = boost::filesystem::temp_directory_path();
+		auto queryFileName = tempDir / "query.smt2";
+
+		auto queryFile = boost::filesystem::ofstream(queryFileName);
+		queryFile << _input;
+
+		auto eldBin = boost::process::search_path("eld");
+		if (!eldBin.empty())
+		{
+			boost::process::ipstream is;
+			boost::process::child eld(
+				eldBin,
+				"-ssol",
+				"-scex",
+				queryFileName,
+				boost::process::std_out > is
+			);
+
+			vector<string> data;
+			string line;
+			while (eld.running() && std::getline(is, line))
+				if (!line.empty())
+					data.push_back(line);
+
+			eld.wait();
+
+			return boost::join(data, "\n");
+		}
+	}
+
 	m_unhandledQueries.push_back(_input);
 	return "unknown\n";
 }
diff --git a/libsmtutil/CHCSmtLib2Interface.h b/libsmtutil/CHCSmtLib2Interface.h
index a7dfb7692..4748af8da 100644
--- a/libsmtutil/CHCSmtLib2Interface.h
+++ b/libsmtutil/CHCSmtLib2Interface.h
@@ -35,6 +35,7 @@ public:
 	explicit CHCSmtLib2Interface(
 		std::map<util::h256, std::string> const& _queryResponses = {},
 		frontend::ReadCallback::Callback _smtCallback = {},
+		SMTSolverChoice _enabledSolvers = SMTSolverChoice::All(),
 		std::optional<unsigned> _queryTimeout = {}
 	);
 
@@ -78,6 +79,7 @@ private:
 	std::vector<std::string> m_unhandledQueries;
 
 	frontend::ReadCallback::Callback m_smtCallback;
+	SMTSolverChoice m_enabledSolvers;
 
 	std::map<Sort const*, std::string> m_sortNames;
 };
diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h
index ca4c497de..79e81be74 100644
--- a/libsmtutil/SolverInterface.h
+++ b/libsmtutil/SolverInterface.h
@@ -42,14 +42,16 @@ namespace solidity::smtutil
 struct SMTSolverChoice
 {
 	bool cvc4 = false;
+	bool eld = false;
 	bool smtlib2 = false;
 	bool z3 = false;
 
-	static constexpr SMTSolverChoice All() noexcept { return {true, true, true}; }
-	static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false}; }
-	static constexpr SMTSolverChoice SMTLIB2() noexcept { return {false, true, false}; }
-	static constexpr SMTSolverChoice Z3() noexcept { return {false, false, true}; }
-	static constexpr SMTSolverChoice None() noexcept { return {false, false, false}; }
+	static constexpr SMTSolverChoice All() noexcept { return {true, true, true, true}; }
+	static constexpr SMTSolverChoice CVC4() noexcept { return {true, false, false, false}; }
+	static constexpr SMTSolverChoice ELD() noexcept { return {false, true, false, false}; }
+	static constexpr SMTSolverChoice SMTLIB2() noexcept { return {false, false, true, false}; }
+	static constexpr SMTSolverChoice Z3() noexcept { return {false, false, false, true}; }
+	static constexpr SMTSolverChoice None() noexcept { return {false, false, false, false}; }
 
 	static std::optional<SMTSolverChoice> fromString(std::string const& _solvers)
 	{
@@ -57,6 +59,7 @@ struct SMTSolverChoice
 		if (_solvers == "all")
 		{
 			smtAssert(solvers.setSolver("cvc4"), "");
+			smtAssert(solvers.setSolver("eld"), "");
 			smtAssert(solvers.setSolver("smtlib2"), "");
 			smtAssert(solvers.setSolver("z3"), "");
 		}
@@ -71,6 +74,7 @@ struct SMTSolverChoice
 	SMTSolverChoice& operator&=(SMTSolverChoice const& _other)
 	{
 		cvc4 &= _other.cvc4;
+		eld &= _other.eld;
 		smtlib2 &= _other.smtlib2;
 		z3 &= _other.z3;
 		return *this;
@@ -87,17 +91,20 @@ struct SMTSolverChoice
 	bool operator==(SMTSolverChoice const& _other) const noexcept
 	{
 		return cvc4 == _other.cvc4 &&
+			eld == _other.eld &&
 			smtlib2 == _other.smtlib2 &&
 			z3 == _other.z3;
 	}
 
 	bool setSolver(std::string const& _solver)
 	{
-		static std::set<std::string> const solvers{"cvc4", "smtlib2", "z3"};
+		static std::set<std::string> const solvers{"cvc4", "eld", "smtlib2", "z3"};
 		if (!solvers.count(_solver))
 			return false;
 		if (_solver == "cvc4")
 			cvc4 = true;
+		if (_solver == "eld")
+			eld = true;
 		else if (_solver == "smtlib2")
 			smtlib2 = true;
 		else if (_solver == "z3")
@@ -106,8 +113,8 @@ struct SMTSolverChoice
 	}
 
 	bool none() const noexcept { return !some(); }
-	bool some() const noexcept { return cvc4 || smtlib2 || z3; }
-	bool all() const noexcept { return cvc4 && smtlib2 && z3; }
+	bool some() const noexcept { return cvc4 || eld || smtlib2 || z3; }
+	bool all() const noexcept { return cvc4 && eld && smtlib2 && z3; }
 };
 
 enum class CheckResult
diff --git a/libsolidity/formal/CHC.cpp b/libsolidity/formal/CHC.cpp
index d6b318520..80a0852c9 100644
--- a/libsolidity/formal/CHC.cpp
+++ b/libsolidity/formal/CHC.cpp
@@ -18,6 +18,8 @@
 
 #include <libsolidity/formal/CHC.h>
 
+#include <libsolidity/formal/ModelChecker.h>
+
 #ifdef HAVE_Z3
 #include <libsmtutil/Z3CHCInterface.h>
 #endif
@@ -89,7 +91,7 @@ void CHC::analyze(SourceUnit const& _source)
 	}
 #endif
 
-	if (!usesZ3 && !m_settings.solvers.smtlib2)
+	if (!usesZ3 && !m_settings.solvers.smtlib2 && !m_settings.solvers.eld)
 	{
 		m_errorReporter.warning(
 			7649_error,
@@ -99,6 +101,20 @@ void CHC::analyze(SourceUnit const& _source)
 		return;
 	}
 
+	if (
+		m_settings.solvers == SMTSolverChoice::ELD() &&
+		!ModelChecker::availableSolvers().eld
+	)
+	{
+		m_errorReporter.warning(
+			7267_error,
+			SourceLocation(),
+			"CHC analysis was not possible since Eldarica was the only"
+			" Horn solver enabled, but it was not found in the system."
+		);
+		return;
+	}
+
 	resetSourceAnalysis();
 
 	auto sources = sourceDependencies(_source);
@@ -115,7 +131,8 @@ void CHC::analyze(SourceUnit const& _source)
 
 	bool ranSolver = true;
 	// If ranSolver is true here it's because an SMT solver callback was
-	// actually given and the queries were solved.
+	// actually given and the queries were solved,
+	// or Eldarica was chosen and was present in the system.
 	if (auto const* smtLibInterface = dynamic_cast<CHCSmtLib2Interface const*>(m_interface.get()))
 		ranSolver = smtLibInterface->unhandledQueries().empty();
 	if (!ranSolver)
@@ -1179,7 +1196,7 @@ void CHC::resetSourceAnalysis()
 		solAssert(m_settings.solvers.smtlib2);
 
 		if (!m_interface)
-			m_interface = make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.timeout);
+			m_interface = make_unique<CHCSmtLib2Interface>(m_smtlib2Responses, m_smtCallback, m_settings.solvers, m_settings.timeout);
 
 		auto smtlib2Interface = dynamic_cast<CHCSmtLib2Interface*>(m_interface.get());
 		solAssert(smtlib2Interface, "");
diff --git a/libsolidity/formal/ModelChecker.cpp b/libsolidity/formal/ModelChecker.cpp
index cf7a398ec..08a0c05a7 100644
--- a/libsolidity/formal/ModelChecker.cpp
+++ b/libsolidity/formal/ModelChecker.cpp
@@ -21,6 +21,8 @@
 #include <libsmtutil/Z3Interface.h>
 #endif
 
+#include <boost/process.hpp>
+
 #include <range/v3/algorithm/any_of.hpp>
 #include <range/v3/view.hpp>
 
@@ -138,6 +140,7 @@ vector<string> ModelChecker::unhandledQueries()
 solidity::smtutil::SMTSolverChoice ModelChecker::availableSolvers()
 {
 	smtutil::SMTSolverChoice available = smtutil::SMTSolverChoice::SMTLIB2();
+	available.eld = !boost::process::search_path("eld").empty();
 #ifdef HAVE_Z3
 	available.z3 = solidity::smtutil::Z3Interface::available();
 #endif