diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index 7c8c089e3..2d2f05ec2 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -494,10 +494,10 @@ void SMTChecker::createVariable(VariableDeclaration const& _varDecl, bool _setTo
 	{
 		solAssert(m_currentSequenceCounter.count(&_varDecl) == 0, "");
 		solAssert(m_nextFreeSequenceCounter.count(&_varDecl) == 0, "");
-		solAssert(m_Variables.count(&_varDecl) == 0, "");
+		solAssert(m_variables.count(&_varDecl) == 0, "");
 		m_currentSequenceCounter[&_varDecl] = 0;
 		m_nextFreeSequenceCounter[&_varDecl] = 1;
-		m_Variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
+		m_variables.emplace(&_varDecl, m_interface->newFunction(uniqueSymbol(_varDecl), smt::Sort::Int, smt::Sort::Int));
 		setValue(_varDecl, _setToZero);
 	}
 	else
@@ -566,7 +566,7 @@ smt::Expression SMTChecker::maxValue(IntegerType const& _t)
 
 smt::Expression SMTChecker::expr(Expression const& _e)
 {
-	if (!m_Expressions.count(&_e))
+	if (!m_expressions.count(&_e))
 	{
 		solAssert(_e.annotation().type, "");
 		switch (_e.annotation().type->category())
@@ -575,24 +575,24 @@ smt::Expression SMTChecker::expr(Expression const& _e)
 		{
 			if (RationalNumberType const* rational = dynamic_cast<RationalNumberType const*>(_e.annotation().type.get()))
 				solAssert(!rational->isFractional(), "");
-			m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
+			m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
 			break;
 		}
 		case Type::Category::Integer:
-			m_Expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
+			m_expressions.emplace(&_e, m_interface->newInteger(uniqueSymbol(_e)));
 			break;
 		case Type::Category::Bool:
-			m_Expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
+			m_expressions.emplace(&_e, m_interface->newBool(uniqueSymbol(_e)));
 			break;
 		default:
 			solAssert(false, "Type not implemented.");
 		}
 	}
-	return m_Expressions.at(&_e);
+	return m_expressions.at(&_e);
 }
 
 smt::Expression SMTChecker::var(Declaration const& _decl)
 {
-	solAssert(m_Variables.count(&_decl), "");
-	return m_Variables.at(&_decl);
+	solAssert(m_variables.count(&_decl), "");
+	return m_variables.at(&_decl);
 }
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index d23fd201b..faaac6396 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -103,8 +103,8 @@ private:
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::map<Declaration const*, int> m_currentSequenceCounter;
 	std::map<Declaration const*, int> m_nextFreeSequenceCounter;
-	std::map<Expression const*, smt::Expression> m_Expressions;
-	std::map<Declaration const*, smt::Expression> m_Variables;
+	std::map<Expression const*, smt::Expression> m_expressions;
+	std::map<Declaration const*, smt::Expression> m_variables;
 	ErrorReporter& m_errorReporter;
 
 	FunctionDefinition const* m_currentFunction = nullptr;