diff options
| author | chriseth <chris@ethereum.org> | 2017-07-14 00:22:51 +0800 |
|---|---|---|
| committer | chriseth <chris@ethereum.org> | 2017-08-23 23:37:35 +0800 |
| commit | 4cea3d4aa44194e052520fea2f6d216675d3bd14 (patch) | |
| tree | 5c61271a42c2068a4387bdc2eefee3c27f04fe85 /libsolidity/formal/SMTChecker.h | |
| parent | c9cf24458baa77e2a2de1bedbad5040d0d83aab2 (diff) | |
| download | dexon-solidity-4cea3d4aa44194e052520fea2f6d216675d3bd14.tar.gz dexon-solidity-4cea3d4aa44194e052520fea2f6d216675d3bd14.tar.zst dexon-solidity-4cea3d4aa44194e052520fea2f6d216675d3bd14.zip | |
Insert abstraction layer.
Diffstat (limited to 'libsolidity/formal/SMTChecker.h')
| -rw-r--r-- | libsolidity/formal/SMTChecker.h | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/libsolidity/formal/SMTChecker.h b/libsolidity/formal/SMTChecker.h index 8c6a2327..afe5897d 100644 --- a/libsolidity/formal/SMTChecker.h +++ b/libsolidity/formal/SMTChecker.h @@ -18,7 +18,7 @@ #pragma once #include <libsolidity/ast/ASTVisitor.h> -#include <libsolidity/formal/SMTLib2Interface.h> +#include <libsolidity/formal/SolverInterface.h> #include <libsolidity/interface/ReadFile.h> #include <map> @@ -85,7 +85,7 @@ private: /// The function takes one argument which is the "sequence number". smt::Expression var(Declaration const& _decl); - smt::SMTLib2Interface m_interface; + std::shared_ptr<smt::SolverInterface> m_interface; std::map<Declaration const*, int> m_currentSequenceCounter; std::map<Expression const*, smt::Expression> m_z3Expressions; std::map<Declaration const*, smt::Expression> m_z3Variables; |