From d8c1a124e7e79dae3688d6364f328bde8e146a5c Mon Sep 17 00:00:00 2001
From: Martin Blicha <martin.blicha@gmail.com>
Date: Thu, 17 Aug 2023 09:13:46 +0200
Subject: [PATCH] Bring back solving with temporary file for Eldarica

---
 libsolidity/interface/SMTSolverCommand.cpp | 93 +++++++++++++++++-----
 1 file changed, 71 insertions(+), 22 deletions(-)

diff --git a/libsolidity/interface/SMTSolverCommand.cpp b/libsolidity/interface/SMTSolverCommand.cpp
index 1e0e0aa1a..da6210157 100644
--- a/libsolidity/interface/SMTSolverCommand.cpp
+++ b/libsolidity/interface/SMTSolverCommand.cpp
@@ -22,9 +22,12 @@
 #include <libsolutil/CommonIO.h>
 #include <libsolutil/Exceptions.h>
 #include <libsolutil/Keccak256.h>
+#include <libsolutil/TemporaryDirectory.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>
 
 using solidity::langutil::InternalCompilerError;
@@ -34,6 +37,71 @@ using solidity::util::errinfo_comment;
 namespace solidity::frontend
 {
 
+namespace
+{
+ReadCallback::Result solveWithTemporaryFile(
+		boost::filesystem::path const& _pathToBinary,
+		std::vector<std::string> _commandArgs,
+		std::string const& _query
+		)
+{
+	auto tempDir = solidity::util::TemporaryDirectory("smt");
+	util::h256 queryHash = util::keccak256(_query);
+	auto queryFileName = tempDir.path() / ("query_" + queryHash.hex() + ".smt2");
+	auto queryFile = boost::filesystem::ofstream(queryFileName);
+	queryFile << _query << std::flush;
+
+	_commandArgs.push_back(queryFileName.string());
+
+	boost::process::ipstream out; // output from subprocess read by main process
+	boost::process::child solver(
+			_pathToBinary,
+			boost::process::args(_commandArgs),
+			boost::process::std_out > out
+	);
+
+	std::vector<std::string> data;
+	std::string line;
+	while (std::getline(out, line))
+		if (!line.empty())
+			data.push_back(line);
+
+	solver.wait();
+
+	return ReadCallback::Result{true, boost::join(data, "\n")};
+}
+
+ReadCallback::Result solveWithPipe(
+		boost::filesystem::path const& _pathToBinary,
+		std::vector<std::string> _commandArgs,
+		std::string const& _query
+		)
+{
+	boost::process::opstream in;  // input to subprocess written to by main process
+	boost::process::ipstream out; // output from subprocess read by main process
+	boost::process::child solver(
+			_pathToBinary,
+			boost::process::args(_commandArgs),
+			boost::process::std_out > out,
+			boost::process::std_in < in
+	);
+
+	in << _query << std::flush;
+	in.pipe().close();
+	in.close();
+
+	std::vector<std::string> data;
+	std::string line;
+	while (std::getline(out, line))
+		if (!line.empty())
+			data.push_back(line);
+
+	solver.wait();
+
+	return ReadCallback::Result{true, boost::join(data, "\n")};
+}
+} // namespace
+
 ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::string const& _query)
 {
 	try
@@ -55,28 +123,9 @@ ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::stri
 
 		commandArgs.erase(commandArgs.begin());
 
-		boost::process::opstream in;  // input to subprocess written to by main process
-		boost::process::ipstream out; // output from subprocess read by main process
-		boost::process::child solver(
-			pathToBinary,
-			boost::process::args(commandArgs),
-			boost::process::std_out > out,
-			boost::process::std_in < in
-		);
-
-		in << _query << std::flush;
-		in.pipe().close();
-		in.close();
-
-		std::vector<std::string> data;
-		std::string line;
-		while (std::getline(out, line))
-			if (!line.empty())
-				data.push_back(line);
-
-		solver.wait();
-
-		return ReadCallback::Result{true, boost::join(data, "\n")};
+		if (solverBinary == "eld")
+			return solveWithTemporaryFile(pathToBinary, std::move(commandArgs), _query);
+		return solveWithPipe(pathToBinary, std::move(commandArgs), _query);
 	}
 	catch (...)
 	{