diff options
Diffstat (limited to 'libsolidity/formal/SMTChecker.h')
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index fd54fb5c..6e64235e 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -111,6 +111,7 @@ private: smt::CheckResult checkSatisfiable(); void initializeLocalVariables(FunctionDefinition const& _function); + void resetStateVariables(); void resetVariables(std::vector<Declaration const*> _variables); /// Given two different branches and the touched variables, /// merge the touched variables into after-branch ite variables @@ -163,6 +164,7 @@ private: 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; |