runtimeverification / kontrol

BSD 3-Clause "New" or "Revised" License
55 stars 9 forks source link

Node bound (`bmc-depth`) in `setUp` not respected in test #845

Closed palinatolmach closed 1 month ago

palinatolmach commented 1 month ago

As identified by @PetarMax and @lisandrasilva, when a setUp function has a bounded node, that node stay bounded for the test, however, it does not remain bounded; which might mean that we’re running setUp with bmc-depth + 1 and the test with bmc-depth. The issue can be reproduced using the TermAuctionListInvariants.testInsertPendingNewOffer test or this one:

contract BoundTest is Test, KontrolCheats {
    uint x;

    function setUp() public {
        uint256 i = freshUInt256();
        for (uint j = 0; j < i; j++) {
            x += 1;
        }
    }

    function testBound() public {
        assertLe(x, 1);
    }
}