Merge pull request #5571 from ethereum/develop

Version 0.5.1

1 files changed, 4 insertions, 21 deletions

diff --git a/libsolidity/formal/SMTPortfolio.cpp b/libsolidity/formal/SMTPortfolio.cpp
index 8b9fe9ce..2a109b89 100644
--- a/libsolidity/formal/SMTPortfolio.cpp
+++ b/libsolidity/formal/SMTPortfolio.cpp
@@ -23,27 +23,22 @@
 #ifdef HAVE_CVC4
 #include <libsolidity/formal/CVC4Interface.h>
 #endif
-#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
 #include <libsolidity/formal/SMTLib2Interface.h>
-#endif
 
 using namespace std;
 using namespace dev;
 using namespace dev::solidity;
 using namespace dev::solidity::smt;
 
-SMTPortfolio::SMTPortfolio(ReadCallback::Callback const& _readCallback)
+SMTPortfolio::SMTPortfolio(map<h256, string> const& _smtlib2Responses)
 {
+	m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_smtlib2Responses));
 #ifdef HAVE_Z3
 	m_solvers.emplace_back(make_shared<smt::Z3Interface>());
 #endif
 #ifdef HAVE_CVC4
 	m_solvers.emplace_back(make_shared<smt::CVC4Interface>());
 #endif
-#if !defined (HAVE_Z3) && !defined (HAVE_CVC4)
-	m_solvers.emplace_back(make_shared<smt::SMTLib2Interface>(_readCallback)),
-#endif
-	(void)_readCallback;
 }
 
 void SMTPortfolio::reset()
@@ -64,22 +59,10 @@ void SMTPortfolio::pop()
 		s->pop();
 }
 
-void SMTPortfolio::declareFunction(string _name, Sort _domain, Sort _codomain)
-{
-	for (auto s : m_solvers)
-		s->declareFunction(_name, _domain, _codomain);
-}
-
-void SMTPortfolio::declareInteger(string _name)
-{
-	for (auto s : m_solvers)
-		s->declareInteger(_name);
-}
-
-void SMTPortfolio::declareBool(string _name)
+void SMTPortfolio::declareVariable(string const& _name, Sort const& _sort)
 {
 	for (auto s : m_solvers)
-		s->declareBool(_name);
+		s->declareVariable(_name, _sort);
 }
 
 void SMTPortfolio::addAssertion(Expression const& _expr)