We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
There are a couple cases where this can happen:
function test_duplicata1(uint256 x) external pure { uint256 mul = x * 42; assertNotEq(mul, 0); assertNotEq(mul, 0); assertNotEq(mul, 0); }
results in
Counterexample: p_x_uint256_7e92c74_00 = 0x0000000000000000000000000000000000000000000000000000000000000000 Counterexample: p_x_uint256_7e92c74_00 = 0x0000000000000000000000000000000000000000000000000000000000000000 Counterexample: p_x_uint256_7e92c74_00 = 0x0000000000000000000000000000000000000000000000000000000000000000
function test_duplicata2(uint256 x) external pure { uint256 acc = 0; unchecked { // just introduce some extra paths acc += (x & (0xFF << 8) > 0) ? 2 : 3; acc += (x & (0xFF << 16) > 0) ? 5 : 3; assertNotEq((x & 0xff) * uint256(acc), 0); } }
function test_duplicata3(uint256 x) external pure { assertNotEq(x, 0); assertNotEq(x & 0xff, 0); assertNotEq(x & 0xff << 8, 0); }
It seems a little odd and spammy to see the same cex repeated verbatim in the output.
--early-exit
The text was updated successfully, but these errors were encountered:
No branches or pull requests
There are a couple cases where this can happen:
results in
It seems a little odd and spammy to see the same cex repeated verbatim in the output.
Suggested behavior
--early-exit
and making it the default)The text was updated successfully, but these errors were encountered: