ActivePool_verified.conf

{
    "files": [
        "certora/harness/ActivePoolHarness.sol",
        "certora/harness/CollateralTokenTester.sol",
        "certora/harness/CollSurplusPoolHarness.sol",
        "certora/harness/DummyERC20A.sol",
        "certora/harness/DummyERC20B.sol",
    ],
    "link": [

        "ActivePoolHarness:collateral=CollateralTokenTester",
        "ActivePoolHarness:collSurplusPoolAddress=CollSurplusPoolHarness",

        "CollSurplusPoolHarness:activePoolAddress=ActivePoolHarness",
        "CollSurplusPoolHarness:collateral=CollateralTokenTester",
    ],
    "verify": "ActivePoolHarness:certora/specs/ActivePool.spec",
    "loop_iter": "3",
    "optimistic_loop": true,
    "rule_sanity": "basic",
    "msg": "ActivePoolHarness",
    "parametric_contracts": [ "ActivePoolHarness" ]
}