aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/CVC4Interface.h
diff options
context:
space:
mode:
Diffstat (limited to 'libsolidity/formal/CVC4Interface.h')
-rw-r--r--libsolidity/formal/CVC4Interface.h3
1 files changed, 2 insertions, 1 deletions
diff --git a/libsolidity/formal/CVC4Interface.h b/libsolidity/formal/CVC4Interface.h
index cd6d761d..273dce23 100644
--- a/libsolidity/formal/CVC4Interface.h
+++ b/libsolidity/formal/CVC4Interface.h
@@ -51,7 +51,7 @@ public:
void push() override;
void pop() override;
- void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+ void declareFunction(std::string _name, std::vector<Sort> const& _domain, Sort _codomain) override;
void declareInteger(std::string _name) override;
void declareBool(std::string _name) override;
@@ -61,6 +61,7 @@ public:
private:
CVC4::Expr toCVC4Expr(Expression const& _expr);
CVC4::Type cvc4Sort(smt::Sort _sort);
+ std::vector<CVC4::Type> cvc4Sort(std::vector<smt::Sort> const& _sort);
CVC4::ExprManager m_context;
CVC4::SmtEngine m_solver;