diff --git a/libsmtutil/Z3Interface.h b/libsmtutil/Z3Interface.h
index 22f793337..23534fd75 100644
--- a/libsmtutil/Z3Interface.h
+++ b/libsmtutil/Z3Interface.h
@@ -49,9 +49,7 @@ public:
 
 	// 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 10000000,
-	// so using double that.
-	static int const resourceLimit = 20000000;
+	static int const resourceLimit = 12500000;
 
 private:
 	void declareFunction(std::string const& _name, Sort const& _sort);