Merge pull request #7214 from ethereum/smt_relax_nonlinear_expecteation

[SMTChecker] Relax expectations for complex nonlinear tests
This commit is contained in:
Leonardo 2019-08-12 10:44:39 +02:00 committed by GitHub
commit b285e08635
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
2 changed files with 14 additions and 1 deletions

View File

@ -153,6 +153,19 @@ do \
} \
while(0)
#define CHECK_SUCCESS_OR_WARNING(text, substring) \
do \
{ \
auto sourceAndError = parseAnalyseAndReturnError((text), true); \
auto const& errors = sourceAndError.second; \
if (!errors.empty()) \
{ \
auto message = searchErrors(errors, {{(Error::Type::Warning), (substring)}}); \
BOOST_CHECK_MESSAGE(message.empty(), message); \
} \
} \
while(0)
}
}
}

View File

@ -109,7 +109,7 @@ BOOST_AUTO_TEST_CASE(division)
}
}
)";
CHECK_SUCCESS_NO_WARNINGS(text);
CHECK_SUCCESS_OR_WARNING(text, "might happen");
text = R"(
contract C {
function mul(uint256 a, uint256 b) internal pure returns (uint256) {