diff --git a/libsmtutil/CHCSmtLib2Interface.cpp b/libsmtutil/CHCSmtLib2Interface.cpp
index 8df9fe355..9bc1d5a2e 100644
--- a/libsmtutil/CHCSmtLib2Interface.cpp
+++ b/libsmtutil/CHCSmtLib2Interface.cpp
@@ -201,19 +201,19 @@ std::string CHCSmtLib2Interface::querySolver(std::string const& _input)
 		if (m_enabledSolvers.eld)
 			return "eld";
 		if (m_enabledSolvers.z3)
-			return "z3 rlimit=1000000 fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false";
+			return "z3 -in rlimit=1000000 fp.spacer.q3.use_qgen=true fp.spacer.mbqi=false fp.spacer.ground_pobs=false";
 		return "";
 	}();
 	std::string z3Input = _input + "(get-model)\n";
 	auto const& query = boost::starts_with(solverBinary, "z3") ? z3Input : _input;
-	auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, query);
+	auto result = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ":" + solverBinary, query);
 	if (result.success)
 	{
 		if (m_enabledSolvers.z3 and boost::starts_with(result.responseOrErrorMessage, "unsat"))
 		{
 			solverBinary += " fp.xform.slice=false fp.xform.inline_linear=false fp.xform.inline_eager=false";
 			std::string extendedQuery = "(set-option :produce-proofs true)" + _input + "\n(get-proof)";
-			auto secondResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + " " + solverBinary, extendedQuery);
+			auto secondResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ":" + solverBinary, extendedQuery);
 			if (secondResult.success and boost::starts_with(secondResult.responseOrErrorMessage, "unsat"))
 				return secondResult.responseOrErrorMessage;
 		}
diff --git a/libsmtutil/SMTLib2Interface.cpp b/libsmtutil/SMTLib2Interface.cpp
index db3320490..6f52589df 100644
--- a/libsmtutil/SMTLib2Interface.cpp
+++ b/libsmtutil/SMTLib2Interface.cpp
@@ -168,16 +168,16 @@ std::pair<CheckResult, std::vector<std::string>> SMTLib2Interface::check(std::ve
 
 	std::vector<std::string> solverCommands;
 	if (m_enabledSolvers.z3)
-		solverCommands.emplace_back("z3 rlimit=1000000");
+		solverCommands.emplace_back("z3 -in rlimit=1000000");
 	if (m_enabledSolvers.cvc4)
-		solverCommands.emplace_back("cvc4");
+		solverCommands.emplace_back("cvc4 --lang smtlib2.6 --output-lang smtlib2.6");
 
 	CheckResult lastResult = CheckResult::ERROR;
 	std::vector<std::string> finalValues;
 	smtAssert(m_smtCallback);
 	for (auto const& s: solverCommands)
 	{
-		auto callBackResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ' ' + s, query);
+		auto callBackResult = m_smtCallback(ReadCallback::kindString(ReadCallback::Kind::SMTQuery) + ":" + s, query);
 		if (not callBackResult.success)
 			continue;
 		auto const& response = callBackResult.responseOrErrorMessage;
diff --git a/libsolidity/interface/SMTSolverCommand.cpp b/libsolidity/interface/SMTSolverCommand.cpp
index 07e17e77c..1e0e0aa1a 100644
--- a/libsolidity/interface/SMTSolverCommand.cpp
+++ b/libsolidity/interface/SMTSolverCommand.cpp
@@ -38,11 +38,11 @@ ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::stri
 {
 	try
 	{
-		auto pos = _kind.find(' ');
+		auto pos = _kind.find(":");
+		solAssert(pos != std::string::npos);
 		auto kind = _kind.substr(0, pos);
 		auto solverCommand = _kind.substr(pos + 1);
-		if (kind != ReadCallback::kindString(ReadCallback::Kind::SMTQuery))
-			solAssert(false, "SMTQuery callback used as callback kind " + kind);
+		solAssert(kind == ReadCallback::kindString(ReadCallback::Kind::SMTQuery), "SMTQuery callback used as callback kind " + kind);
 
 		std::vector<std::string> commandArgs;
 		boost::split(commandArgs, solverCommand, boost::is_any_of(" "));
@@ -55,9 +55,6 @@ ReadCallback::Result SMTSolverCommand::solve(std::string const& _kind, std::stri
 
 		commandArgs.erase(commandArgs.begin());
 
-		if (solverBinary == "z3")
-			commandArgs.insert(commandArgs.begin(), "-in");
-
 		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(
diff --git a/libsolidity/interface/SMTSolverCommand.h b/libsolidity/interface/SMTSolverCommand.h
index 96969d0ec..e3f037519 100644
--- a/libsolidity/interface/SMTSolverCommand.h
+++ b/libsolidity/interface/SMTSolverCommand.h
@@ -29,6 +29,7 @@ public:
 	SMTSolverCommand() = default;
 
 	/// Calls an SMT solver with the given query.
+	/// The whole command line for invoking the solver is part of @p _kind
 	frontend::ReadCallback::Result solve(std::string const& _kind, std::string const& _query);
 
 	frontend::ReadCallback::Callback solver()