Review comments

2 files changed, 8 insertions, 10 deletions

diff --git a/libsolidity/formal/SMTChecker.cpp b/libsolidity/formal/SMTChecker.cpp
index be968173..773fc332 100644
--- a/libsolidity/formal/SMTChecker.cpp
+++ b/libsolidity/formal/SMTChecker.cpp
@@ -98,7 +98,7 @@ void SMTChecker::endVisit(FunctionDefinition const&)
 	// TOOD we could check for "reachability", i.e. satisfiability here.
 	// We only handle local variables, so we clear at the beginning of the function.
 	// If we add storage variables, those should be cleared differently.
-	clearLocalVariables();
+	removeLocalVariables();
 	m_currentFunction = nullptr;
 }
 
@@ -729,9 +729,8 @@ void SMTChecker::resetStateVariables()
 {
 	for (auto const& variable: m_variables)
 	{
-		VariableDeclaration const* _decl = dynamic_cast<VariableDeclaration const*>(variable.first);
-		solAssert(_decl, "");
-		if (_decl->isStateVariable())
+		VariableDeclaration const& _decl = dynamic_cast<VariableDeclaration const&>(*variable.first);
+		if (_decl.isStateVariable())
 		{
 			newValue(*variable.first);
 			setUnknownValue(*variable.first);
@@ -895,13 +894,12 @@ void SMTChecker::addPathImpliedExpression(smt::Expression const& _e)
 	m_interface->addAssertion(smt::Expression::implies(currentPathConditions(), _e));
 }
 
-void SMTChecker::clearLocalVariables()
+void SMTChecker::removeLocalVariables()
 {
 	for (auto it = m_variables.begin(); it != m_variables.end(); )
 	{
-		VariableDeclaration const* _decl = dynamic_cast<VariableDeclaration const*>(it->first);
-		solAssert(_decl, "");
-		if (_decl->isLocalVariable())
+		VariableDeclaration const& _decl = dynamic_cast<VariableDeclaration const&>(*it->first);
+		if (_decl.isLocalVariable())
 			it = m_variables.erase(it);
 		else
 			++it;
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index b5c5cfd7..b7d0f6a8 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -161,8 +161,8 @@ private:
 	/// Add to the solver: the given expression implied by the current path conditions
 	void addPathImpliedExpression(smt::Expression const& _e);
 
-	/// Clears the local variables of a function.
-	void clearLocalVariables();
+	/// Removes the local variables of a function.
+	void removeLocalVariables();
 
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::shared_ptr<VariableUsage> m_variableUsage;