aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SMTLib2Interface.h
diff options
context:
space:
mode:
authorLeonardo Alt <leo@ethereum.org>2018-04-20 22:56:10 +0800
committerAlex Beregszaszi <alex@rtfs.hu>2018-07-27 23:15:34 +0800
commit87a38e1abe61547e66aedfa595a73fb78184d609 (patch)
treeba41f379fbf2713f2e885c0d641a5780a06d7fe4 /libsolidity/formal/SMTLib2Interface.h
parent5faa60e8834b5302f8d58f719c6962ed3affb50f (diff)
downloaddexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.tar
dexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.tar.gz
dexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.tar.bz2
dexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.tar.lz
dexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.tar.xz
dexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.tar.zst
dexon-solidity-87a38e1abe61547e66aedfa595a73fb78184d609.zip
[SMTChecker] SMTPortfolio: use all SMT solvers available
Diffstat (limited to 'libsolidity/formal/SMTLib2Interface.h')
-rw-r--r--libsolidity/formal/SMTLib2Interface.h6
1 files changed, 3 insertions, 3 deletions
diff --git a/libsolidity/formal/SMTLib2Interface.h b/libsolidity/formal/SMTLib2Interface.h
index 63188acd..61071fe5 100644
--- a/libsolidity/formal/SMTLib2Interface.h
+++ b/libsolidity/formal/SMTLib2Interface.h
@@ -48,9 +48,9 @@ public:
void push() override;
void pop() override;
- Expression newFunction(std::string _name, Sort _domain, Sort _codomain) override;
- Expression newInteger(std::string _name) override;
- Expression newBool(std::string _name) override;
+ void declareFunction(std::string _name, Sort _domain, Sort _codomain) override;
+ void declareInteger(std::string _name) override;
+ void declareBool(std::string _name) override;
void addAssertion(Expression const& _expr) override;
std::pair<CheckResult, std::vector<std::string>> check(std::vector<Expression> const& _expressionsToEvaluate) override;