Merge remote-tracking branch 'origin/develop' into breaking

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, "");

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);

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),