Merge pull request #4351 from ethereum/smt_portfolio

[SMTChecker] SMTPortfolio: use all SMT solvers available

1 files changed, 3 insertions, 6 deletions

diff --git a/libsolidity/formal/SMTLib2Interface.cpp b/libsolidity/formal/SMTLib2Interface.cpp
index 00ac523f..d9ea6df6 100644
--- a/libsolidity/formal/SMTLib2Interface.cpp
+++ b/libsolidity/formal/SMTLib2Interface.cpp
@@ -62,7 +62,7 @@ void SMTLib2Interface::pop()
 	m_accumulatedOutput.pop_back();
 }
 
-Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codomain)
+void SMTLib2Interface::declareFunction(string _name, Sort _domain, Sort _codomain)
 {
 	write(
 		"(declare-fun |" +
@@ -73,19 +73,16 @@ Expression SMTLib2Interface::newFunction(string _name, Sort _domain, Sort _codom
 		(_codomain == Sort::Int ? "Int" : "Bool") +
 		")"
 	);
-	return SolverInterface::newFunction(move(_name), _domain, _codomain);
 }
 
-Expression SMTLib2Interface::newInteger(string _name)
+void SMTLib2Interface::declareInteger(string _name)
 {
 	write("(declare-const |" + _name + "| Int)");
-	return SolverInterface::newInteger(move(_name));
 }
 
-Expression SMTLib2Interface::newBool(string _name)
+void SMTLib2Interface::declareBool(string _name)
 {
 	write("(declare-const |" + _name + "| Bool)");
-	return SolverInterface::newBool(std::move(_name));
 }
 
 void SMTLib2Interface::addAssertion(Expression const& _expr)