Refactoring how storage and local variables are managed.

1 files changed, 3 insertions, 1 deletions

diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h
index 50d40ab9..b5c5cfd7 100644
--- a/libsolidity/formal/SMTChecker.h
+++ b/libsolidity/formal/SMTChecker.h
@@ -161,12 +161,14 @@ 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();
+
 	std::shared_ptr<smt::SolverInterface> m_interface;
 	std::shared_ptr<VariableUsage> m_variableUsage;
 	bool m_loopExecutionHappened = false;
 	std::map<Expression const*, smt::Expression> m_expressions;
 	std::map<Declaration const*, SSAVariable> m_variables;
-	std::map<Declaration const*, SSAVariable> m_stateVariables;
 	std::vector<smt::Expression> m_pathConditions;
 	ErrorReporter& m_errorReporter;