diff --git a/libsmtutil/SMTPortfolio.h b/libsmtutil/SMTPortfolio.h
index aca50eef7..aab92f996 100644
--- a/libsmtutil/SMTPortfolio.h
+++ b/libsmtutil/SMTPortfolio.h
@@ -58,7 +58,7 @@ public:
 	std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;
 
 	std::vector<std::string> unhandledQueries() override;
-	unsigned solvers() override { return m_solvers.size(); }
+	size_t solvers() override { return m_solvers.size(); }
 private:
 	static bool solverAnswered(CheckResult result);
 
diff --git a/libsmtutil/SolverInterface.h b/libsmtutil/SolverInterface.h
index a3a3fb497..8dd73b035 100644
--- a/libsmtutil/SolverInterface.h
+++ b/libsmtutil/SolverInterface.h
@@ -402,7 +402,7 @@ public:
 	virtual std::vector<std::string> unhandledQueries() { return {}; }
 
 	/// @returns how many SMT solvers this interface has.
-	virtual unsigned solvers() { return 1; }
+	virtual size_t solvers() { return 1; }
 
 protected:
 	std::optional<unsigned> m_queryTimeout;
diff --git a/libsmtutil/Z3Interface.cpp b/libsmtutil/Z3Interface.cpp
index 3e01dd62c..46e601fdf 100644
--- a/libsmtutil/Z3Interface.cpp
+++ b/libsmtutil/Z3Interface.cpp
@@ -217,7 +217,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 		else if (n == "int2bv")
 		{
 			size_t size = std::stoul(_expr.arguments[1].name);
-			return z3::int2bv(size, arguments[0]);
+			return z3::int2bv(static_cast<unsigned>(size), arguments[0]);
 		}
 		else if (n == "bv2int")
 		{
@@ -240,7 +240,7 @@ z3::expr Z3Interface::toZ3Expr(Expression const& _expr)
 		else if (n == "tuple_get")
 		{
 			size_t index = stoul(_expr.arguments[1].name);
-			return z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, z3Sort(*_expr.arguments[0].sort), index))(arguments[0]);
+			return z3::func_decl(m_context, Z3_get_tuple_sort_field_decl(m_context, z3Sort(*_expr.arguments[0].sort), static_cast<unsigned>(index)))(arguments[0]);
 		}
 		else if (n == "tuple_constructor")
 		{
@@ -367,7 +367,7 @@ z3::sort Z3Interface::z3Sort(Sort const& _sort)
 		z3::func_decl_vector projs(m_context);
 		z3::func_decl tupleConstructor = m_context.tuple_sort(
 			tupleSort.name.c_str(),
-			tupleSort.members.size(),
+			static_cast<unsigned>(tupleSort.members.size()),
 			cMembers.data(),
 			sorts.data(),
 			projs
diff --git a/libsolidity/formal/EncodingContext.h b/libsolidity/formal/EncodingContext.h
index 204c0e178..7c001f452 100644
--- a/libsolidity/formal/EncodingContext.h
+++ b/libsolidity/formal/EncodingContext.h
@@ -142,7 +142,7 @@ public:
 	void pushSolver();
 	void popSolver();
 	void addAssertion(smtutil::Expression const& _e);
-	unsigned solverStackHeigh() { return m_assertions.size(); } const
+	size_t solverStackHeigh() { return m_assertions.size(); } const
 	smtutil::SolverInterface* solver()
 	{
 		solAssert(m_solver, "");
diff --git a/libsolidity/formal/Predicate.cpp b/libsolidity/formal/Predicate.cpp
index 8d1eba1b4..fb2ef9e8e 100644
--- a/libsolidity/formal/Predicate.cpp
+++ b/libsolidity/formal/Predicate.cpp
@@ -349,7 +349,7 @@ bool Predicate::fillArray(smtutil::Expression const& _expr, vector<string>& _arr
 			return false;
 		// Sometimes the solver assigns huge lengths that are not related,
 		// we should catch and ignore those.
-		unsigned index;
+		unsigned long index;
 		try
 		{
 			index = stoul(*indexStr);
diff --git a/libsolidity/formal/SymbolicState.cpp b/libsolidity/formal/SymbolicState.cpp
index 16bc6e7bf..5d38eac0f 100644
--- a/libsolidity/formal/SymbolicState.cpp
+++ b/libsolidity/formal/SymbolicState.cpp
@@ -41,7 +41,7 @@ BlockchainVariable::BlockchainVariable(
 	{
 		members.emplace_back(component);
 		sorts.emplace_back(sort);
-		m_componentIndices[component] = members.size() - 1;
+		m_componentIndices[component] = static_cast<unsigned>(members.size() - 1);
 	}
 	m_tuple = make_unique<SymbolicTupleVariable>(
 		make_shared<smtutil::TupleSort>(m_name + "_type", members, sorts),