623:         for (uint256 i; i < numOfStakers; ++i) {
624:             address staker = _priorityStakers[i];
625: 
626:             if (i > 0 && staker < _priorityStakers[i-1]) revert DuplicateArrayElements(); 
627: 
628:             isPriorityStaker[staker] = true; 
629: 
630:             emit PriorityStakerRegistered(staker);
631:         }
    function addrCompare(address a1, address a2) external pure returns (bool) {
        return a1 < a2;
    }
rule addingTwoDifferentPriorityStackers(address _priorityStaker1, address _priorityStaker2) {
    // Excluding address(0)
    require(_priorityStaker1 != 0 && _priorityStaker2 != 0);
    // Avoiding duplicates and making sure the address at index i - 1 is greater than the address at index i
    require(_priorityStaker1 > _priorityStaker2);
    // Making sure they aren't already Priority Stakers
    require(!isPriorityStaker(_priorityStaker1) && !isPriorityStaker(_priorityStaker2));
    env e;

    // Adding any 2 Priority stakers address
    addPriorityStakers(e, _priorityStaker1, _priorityStaker2);
    // The rule will fail due to this assertion being unreachable with the bug
    assert(true, "This is unreacheable");
}
File: Syndicate.sol
623:         for (uint256 i; i < numOfStakers; ++i) {
624:             address staker = _priorityStakers[i];
625: 
- 626:             if (i > 0 && staker < _priorityStakers[i-1]) revert DuplicateArrayElements(); 
627: 
628:             isPriorityStaker[staker] = true; 
629: 
630:             emit PriorityStakerRegistered(staker);
631:         }
