cerc-io/solidity
16
0
Fork 0
mirror of https://github.com/ethereum/solidity synced 2023-10-03 13:03:40 +00:00
Code Issues Actions Packages Projects Releases Wiki Activity

[SMTChecker] Adapt division test for Z3 only

Browse Source
This commit is contained in:
Leonardo Alt 2019-08-23 17:33:29 +02:00
parent b5048bd6d7
commit c27235b2f5
1 changed files with 3 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

4
test/libsolidity/SMTChecker.cpp
View File

@ -116,13 +116,15 @@ BOOST_AUTO_TEST_CASE(division)
if (a == 0) {
return 0;
}
// TODO remove when SMTChecker sees that this code is the `else` of the `return`.
require(a != 0);
uint256 c = a * b;
require(c / a == b);
return c;
}
}
)";
CHECK_WARNING(text, "Division by zero");
CHECK_SUCCESS_OR_WARNING(text, "might happen");
text = R"(
contract C {
function div(uint256 a, uint256 b) internal pure returns (uint256) {