Conversation
| @@ -44,18 +44,18 @@ enum class CheckResult | |||
|
|
|||
| enum class Sort | |||
There was a problem hiding this comment.
What does sort means here? Is it kind but the lingo in SMT is sort?
There was a problem hiding this comment.
I'm not sure, but z3 calls this "sort"
There was a problem hiding this comment.
libsolidity/formal/SolverInterface.h
Outdated
| Expression operator()(Expression _a) const | ||
| { | ||
| solAssert(sort == Sort::IntIntFun, "Attempted function application to non-function."); | ||
| solAssert(arguments.empty(), "Attempted function application to non-function."); |
There was a problem hiding this comment.
Could merge these two? Does the second assert make any sense though? Wouldn't it be enough on its own?
There was a problem hiding this comment.
I would keep it for now, until we have proper function sort support. it might be removed in the future.
There was a problem hiding this comment.
You could merge it in that case sort == Sort::IntIntFun && arguments.empty(). But doesn't IntIntFun have a signle argument?
There was a problem hiding this comment.
No, arguments are empty because this is the plain function and we apply the argument _a by calling the operator.
libsolidity/formal/SolverInterface.h
Outdated
| enum class Sort | ||
| { | ||
| Int, Bool | ||
| Int, Bool, IntIntFun |
There was a problem hiding this comment.
Does IntIntFun means it is a function with a single Int input and single Int output? Would a comment here help?
|
Changed. |
chriseth
force-pushed
the
sortsForExpressions
branch
from
26f05d3 to
0e2a965
Compare
|
Test failures are due to the Zeppelin issue. |
2 participants
This will fix the assertion failures on MacOS. More specifically: It fixes assertion failures related to the smt solver when z3 is not found at build time.
It will not fix the tests themselves, because we do not have a way to invoke the smt solver on macos yet.