diff options
| author | chriseth <chris@ethereum.org> | 2018-10-18 04:54:00 +0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-10-18 04:54:00 +0800 |
| commit | c578b21e7c94dbb5ae1eec7bfb9e92e4ffea4ae9 (patch) | |
| tree | a0f9efc61b26fa18cc28138b9233ec008ea27fa1 /libsolidity/formal/SMTChecker.h | |
| parent | 1aca175d62b0b2ee3cf4bf2d2ad90fb1446b5058 (diff) | |
| parent | 070471d8d4921d0204b37aa3315b6737f58e7ad0 (diff) | |
| download | dexon-solidity-c578b21e7c94dbb5ae1eec7bfb9e92e4ffea4ae9.tar.gz dexon-solidity-c578b21e7c94dbb5ae1eec7bfb9e92e4ffea4ae9.tar.zst dexon-solidity-c578b21e7c94dbb5ae1eec7bfb9e92e4ffea4ae9.zip | |
Merge pull request #5251 from ethereum/smt_refactor_expr_types
[SMTChecker] Refactor expressions to use SymbolicVariable
Diffstat (limited to 'libsolidity/formal/SMTChecker.h')
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 3 |
1 files changed, 1 insertions, 2 deletions
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 0b078556..f66693d2 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -25,7 +25,6 @@ #include <libsolidity/interface/ReadFile.h> -#include <map> #include <unordered_map> #include <string> #include <vector> @@ -186,7 +185,7 @@ private: bool m_loopExecutionHappened = false; /// An Expression may have multiple smt::Expression due to /// repeated calls to the same function. - std::multimap<Expression const*, smt::Expression> m_expressions; + std::unordered_map<Expression const*, std::shared_ptr<SymbolicVariable>> m_expressions; std::unordered_map<VariableDeclaration const*, std::shared_ptr<SymbolicVariable>> m_variables; std::vector<smt::Expression> m_pathConditions; ErrorReporter& m_errorReporter; |