aboutsummaryrefslogtreecommitdiffstats
path: root/libsolidity/formal/SolverInterface.h
diff options
context:
space:
mode:
authorchriseth <chris@ethereum.org>2017-11-23 00:12:22 +0800
committerchriseth <chris@ethereum.org>2017-11-24 02:02:47 +0800
commit0e2a9658d231f75e5ac89fd58c5c880b46c4f4dc (patch)
tree6945f9521a33f3f3ed04299931bae5349b9936b7 /libsolidity/formal/SolverInterface.h
parent762d591a4755fbabfe8d2556bab10b77ec1d5bb5 (diff)
downloaddexon-solidity-0e2a9658d231f75e5ac89fd58c5c880b46c4f4dc.tar.gz
dexon-solidity-0e2a9658d231f75e5ac89fd58c5c880b46c4f4dc.tar.zst
dexon-solidity-0e2a9658d231f75e5ac89fd58c5c880b46c4f4dc.zip
Explain IntIntFun and merge assertion.
Diffstat (limited to 'libsolidity/formal/SolverInterface.h')
-rw-r--r--libsolidity/formal/SolverInterface.h10
1 files changed, 7 insertions, 3 deletions
diff --git a/libsolidity/formal/SolverInterface.h b/libsolidity/formal/SolverInterface.h
index ac722dad..c9adf863 100644
--- a/libsolidity/formal/SolverInterface.h
+++ b/libsolidity/formal/SolverInterface.h
@@ -44,7 +44,9 @@ enum class CheckResult
enum class Sort
{
- Int, Bool, IntIntFun
+ Int,
+ Bool,
+ IntIntFun // Function of one Int returning a single Int
};
/// C++ representation of an SMTLIB2 expression.
@@ -120,8 +122,10 @@ public:
}
Expression operator()(Expression _a) const
{
- solAssert(sort == Sort::IntIntFun, "Attempted function application to non-function.");
- solAssert(arguments.empty(), "Attempted function application to non-function.");
+ solAssert(
+ sort == Sort::IntIntFun && arguments.empty(),
+ "Attempted function application to non-function."
+ );
return Expression(name, _a, Sort::Int);
}