diff --git a/libsolidity/formal/CVC4Interface.cpp b/libsolidity/formal/CVC4Interface.cpp
index 377df32d2..03c12cf08 100644
--- a/libsolidity/formal/CVC4Interface.cpp
+++ b/libsolidity/formal/CVC4Interface.cpp
@@ -35,7 +35,7 @@ void CVC4Interface::reset()
 	m_variables.clear();
 	m_solver.reset();
 	m_solver.setOption("produce-models", true);
-	m_solver.setTimeLimit(queryTimeout);
+	m_solver.setResourceLimit(resourceLimit);
 }
 
 void CVC4Interface::push()
diff --git a/libsolidity/formal/CVC4Interface.h b/libsolidity/formal/CVC4Interface.h
index 28596bdcf..76318fdee 100644
--- a/libsolidity/formal/CVC4Interface.h
+++ b/libsolidity/formal/CVC4Interface.h
@@ -63,6 +63,12 @@ private:
 	CVC4::ExprManager m_context;
 	CVC4::SmtEngine m_solver;
 	std::map<std::string, CVC4::Expr> m_variables;
+
+	// CVC4 "basic resources" limit.
+	// This is used to make the runs more deterministic and platform/machine independent.
+	// The tests start failing for CVC4 with less than 6000,
+	// so using double that.
+	static int const resourceLimit = 12000;
 };
 
 }
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index 2889af25a..a39e699af 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -359,10 +359,6 @@ public:
 
 	/// @returns how many SMT solvers this interface has.
 	virtual unsigned solvers() { return 1; }
-
-protected:
-	// SMT query timeout in milliseconds.
-	static int const queryTimeout = 10000;
 };
 
 }
diff --git a/libsolidity/formal/Z3CHCInterface.cpp b/libsolidity/formal/Z3CHCInterface.cpp
index 87d0db0c4..d4c53f850 100644
--- a/libsolidity/formal/Z3CHCInterface.cpp
+++ b/libsolidity/formal/Z3CHCInterface.cpp
@@ -29,10 +29,9 @@ Z3CHCInterface::Z3CHCInterface():
 	m_context(m_z3Interface->context()),
 	m_solver(*m_context)
 {
-	// This needs to be set globally.
+	// These need to be set globally.
 	z3::set_param("rewriter.pull_cheap_ite", true);
-	// This needs to be set in the context.
-	m_context->set("timeout", queryTimeout);
+	z3::set_param("rlimit", Z3Interface::resourceLimit);
 
 	// Spacer options.
 	// These needs to be set in the solver.
diff --git a/libsolidity/formal/Z3CHCInterface.h b/libsolidity/formal/Z3CHCInterface.h
index 3acab97c3..858e4f40f 100644
--- a/libsolidity/formal/Z3CHCInterface.h
+++ b/libsolidity/formal/Z3CHCInterface.h
@@ -54,9 +54,6 @@ private:
 	z3::context* m_context;
 	// Horn solver.
 	z3::fixedpoint m_solver;
-
-	// SMT query timeout in milliseconds.
-	static int const queryTimeout = 10000;
 };
 
 }
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp
index aa20eb533..74b3cfe2b 100644
--- a/libsolidity/formal/Z3Interface.cpp
+++ b/libsolidity/formal/Z3Interface.cpp
@@ -27,10 +27,9 @@ using namespace dev::solidity::smt;
 Z3Interface::Z3Interface():
 	m_solver(m_context)
 {
-	// This needs to be set globally.
+	// These need to be set globally.
 	z3::set_param("rewriter.pull_cheap_ite", true);
-	// This needs to be set in the context.
-	m_context.set("timeout", queryTimeout);
+	z3::set_param("rlimit", resourceLimit);
 }
 
 void Z3Interface::reset()
diff --git a/libsolidity/formal/Z3Interface.h b/libsolidity/formal/Z3Interface.h
index 38734dd00..df5db8d26 100644
--- a/libsolidity/formal/Z3Interface.h
+++ b/libsolidity/formal/Z3Interface.h
@@ -50,6 +50,12 @@ public:
 
 	z3::context* context() { return &m_context; }
 
+	// Z3 "basic resources" limit.
+	// This is used to make the runs more deterministic and platform/machine independent.
+	// The tests start failing for Z3 with less than 20000000,
+	// so using double that.
+	static int const resourceLimit = 40000000;
+
 private:
 	void declareFunction(std::string const& _name, Sort const& _sort);