diff options
Diffstat (limited to 'libsolidity/formal/SMTPortfolio.h')
-rw-r--r-- | libsolidity/formal/SMTPortfolio.h | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/libsolidity/formal/SMTPortfolio.h b/libsolidity/formal/SMTPortfolio.h index 12e2be66..7f5ba37e 100644 --- a/libsolidity/formal/SMTPortfolio.h +++ b/libsolidity/formal/SMTPortfolio.h @@ -22,8 +22,11 @@ #include <libsolidity/interface/ReadFile.h> +#include <libdevcore/FixedHash.h> + #include <boost/noncopyable.hpp> +#include <map> #include <vector> namespace dev @@ -42,7 +45,7 @@ namespace smt class SMTPortfolio: public SolverInterface, public boost::noncopyable { public: - SMTPortfolio(ReadCallback::Callback const& _readCallback); + SMTPortfolio(std::map<h256, std::string> const& _smtlib2Responses); void reset() override; @@ -54,6 +57,7 @@ public: void addAssertion(Expression const& _expr) override; std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override; + std::vector<std::string> unhandledQueries() override { return m_solvers.at(0)->unhandledQueries(); } private: static bool solverAnswered(CheckResult result); |