diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp
index 80051f500..94521be30 100644
--- a/libsmtutil/CHCSmtLib2Interface.cpp
+++ b/libsmtutil/CHCSmtLib2Interface.cpp
@@ -189,7 +189,7 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
 		if (m_enabledSolvers.eld)
 			return "eld";
 		if (m_enabledSolvers.z3)
-			return "z3";
+			return "z3 rlimit=1000000";
 		return "";
 	}();
 	auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, _input);
diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp
index 0887a96f6..e4264557d 100644
--- a/libsmtutil/SMTLib2Interface.cpp
+++ b/libsmtutil/SMTLib2Interface.cpp
@@ -163,7 +163,7 @@ std::pair<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::ve
 
 	std::vector<std::string> solverCommands;
 	if (m_enabledSolvers.z3)
-		solverCommands.emplace_back("z3");
+		solverCommands.emplace_back("z3 rlimit=1000000");
 	if (m_enabledSolvers.cvc4)
 		solverCommands.emplace_back("cvc4");
 
diff --git a/libsolidity/interface/SMTSolverCommand.cpp b/libsolidity/interface/SMTSolverCommand.cpp
index 2c8209f75..aaa2e8edb 100644
--- a/libsolidity/interface/SMTSolverCommand.cpp
+++ b/libsolidity/interface/SMTSolverCommand.cpp
@@ -55,16 +55,21 @@ ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::stri
 
 		queryFile << _query;
 
-		std::string solverBinary = solverCommand.substr(0, solverCommand.find(' '));
+		std::vector<std::string> commandArgs;
+		boost::split(commandArgs, solverCommand, boost::is_any_of(" "));
+		solAssert(commandArgs.size() > 0, "SMT command was empty");
+		auto const& solverBinary = commandArgs[0];
 		auto pathToBinary = boost::process::search_path(solverBinary);
 
 		if (pathToBinary.empty())
 			return ReadCallback::Result{false, solverBinary + " binary not found."};
 
+		commandArgs.erase(commandArgs.begin());
+		commandArgs.push_back(queryFileName.string());
 		boost::process::ipstream pipe;
 		boost::process::child solver(
 			pathToBinary,
-			queryFileName,
+			boost::process::args(commandArgs),
 			boost::process::std_out > pipe
 		);