Skip to content

[SMTChecker] Using solUnimplementedAssert instead of solAssert#3922

Merged
axic merged 1 commit intodevelopfrom
smt_sol_unimplementedassert
Apr 18, 2018
Merged

[SMTChecker] Using solUnimplementedAssert instead of solAssert#3922
axic merged 1 commit intodevelopfrom
smt_sol_unimplementedassert

Conversation

@leonardoalt
Copy link

Fixes #3227

else
{
solAssert(false, "");
solUnimplementedAssert(false, "Type not supported");
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we have other possible types here?

Copy link
Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hopefully in the future :p

@axic
Copy link
Contributor

axic commented Apr 18, 2018

I think the assertions in SMTChecker.cpp are good to be changed, since they handle the translation from Solidity and show what feature is missing.

However in the internal parts it must only be using unimplmented if it is supported by certain parts of the code, while others don't support it yet and will be implemented. If it is for a future type (sort) which we don't even have yet it should remain a regular assertion.

@leonardoalt
Copy link
Author

Right, makes sense

@leonardoalt leonardoalt force-pushed the smt_sol_unimplementedassert branch from c6e3581 to 78ba346 Compare April 18, 2018 11:18
@axic axic merged commit 377254d into develop Apr 18, 2018
@axic axic deleted the smt_sol_unimplementedassert branch April 18, 2018 19:29
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

3 participants

Comments