cerc-io/solidity
10
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

Extract SMTChecker mod test

Browse Source
This commit is contained in:
Leonardo Alt 2019-12-04 13:21:55 +01:00
parent 02343208ad
commit 77b9416d3e
2 changed files with 10 additions and 16 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

16
test/libsolidity/SMTChecker.cpp
View File

@ -59,22 +59,6 @@ protected:
BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework) BOOST_FIXTURE_TEST_SUITE(SMTChecker, SMTCheckerFramework)
BOOST_AUTO_TEST_CASE(mod)
{
string text = R"(
contract C {
function f(int x, int y) public pure {
require(y == -10);
require(x == 100);
int z1 = x % y;
int z2 = x % -y;
assert(z1 == z2);
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
}
BOOST_AUTO_TEST_CASE(import_base) BOOST_AUTO_TEST_CASE(import_base)
{ {
CompilerStack c; CompilerStack c;

10
test/libsolidity/smtCheckerTests/operators/mod.sol Normal file
View File

@ -0,0 +1,10 @@
pragma experimental SMTChecker;
contract C {
function f(int x, int y) public pure {
require(y == -10);
require(x == 100);
int z1 = x % y;
int z2 = x % -y;
assert(z1 == z2);
}
}