diff options
Diffstat (limited to 'libsolidity/formal/Z3Interface.cpp')
-rw-r--r-- | libsolidity/formal/Z3Interface.cpp | 9 |
1 files changed, 3 insertions, 6 deletions
diff --git a/libsolidity/formal/Z3Interface.cpp b/libsolidity/formal/Z3Interface.cpp index b57bcb94..784fbd28 100644 --- a/libsolidity/formal/Z3Interface.cpp +++ b/libsolidity/formal/Z3Interface.cpp @@ -51,22 +51,19 @@ void Z3Interface::pop() m_solver.pop(); } -Expression Z3Interface::newFunction(string _name, Sort _domain, Sort _codomain) +void Z3Interface::declareFunction(string _name, Sort _domain, Sort _codomain) { m_functions.insert({_name, m_context.function(_name.c_str(), z3Sort(_domain), z3Sort(_codomain))}); - return SolverInterface::newFunction(move(_name), _domain, _codomain); } -Expression Z3Interface::newInteger(string _name) +void Z3Interface::declareInteger(string _name) { m_constants.insert({_name, m_context.int_const(_name.c_str())}); - return SolverInterface::newInteger(move(_name)); } -Expression Z3Interface::newBool(string _name) +void Z3Interface::declareBool(string _name) { m_constants.insert({_name, m_context.bool_const(_name.c_str())}); - return SolverInterface::newBool(std::move(_name)); } void Z3Interface::addAssertion(Expression const& _expr) |