SMTChecker: Further test simplifications #15256
Conversation
| mapping (uint => uint8)[2] severalMaps8; | ||
| mapping (uint => uint)[2][2] severalMaps3d; | ||
| function f(mapping (uint => uint) storage map) internal { | ||
| // Accesses are safe but oob is reported because of aliasing. |
There was a problem hiding this comment.
It seems the problem with aliasing of maps had been fixed somewhere along the way, because no oob was reported here anymore.
| // ==== | ||
| // SMTEngine: all | ||
| // SMTIgnoreCex: yes | ||
| // SMTTargets: assert |
There was a problem hiding this comment.
In this test, we want to focus on assertions, not the accesses.
blishko
force-pushed
the
smt-more-test-simplification
branch
from
d7d7773 to
a8063fc
Compare
blishko
force-pushed
the
smt-more-test-simplification
branch
from
a8063fc to
f53bb02
Compare
There was a problem hiding this comment.
The only difference between this file and array_branches_3d.sol was that this has an option SMTShowUnproved: yes, but that is actually the default for that option, so this test was identical to the other one.
We can delete it without losing anything.
| // ==== | ||
| // SMTEngine: all | ||
| // SMTIgnoreOS: macos | ||
| // SMTTargets: assert |
There was a problem hiding this comment.
The out of bounds checks seem to be difficult for Z3, but there is no point to test them, they are safe.
The point of this test is to test the assertion.
This PR is a continuation of the effort (started in #15254 and #15251) to make the test suite more stable as a preparation for the change in the interaction with Z3 (#15252).