UsdcVaultL2.conf

{
    "files": [
        "spark-vaults/src/UsdcVaultL2.sol",
        "harness/SUsdsMock.sol",
        "harness/UsdsMock.sol",
        "harness/Psm3Mock.sol",
        "harness/UsdcMock.sol",
        "harness/RateProviderMock.sol",
        "harness/SignerMock.sol",
        "harness/Auxiliar.sol"
    ],
    "solc": "solc-0.8.21",
    "solc_optimize": "200",
    "packages": [
        "@openzeppelin/contracts-upgradeable/proxy/=spark-vaults/lib/openzeppelin-contracts-upgradeable/contracts/proxy",
        "@openzeppelin/contracts/=spark-vaults/lib/openzeppelin-contracts-upgradeable/lib/openzeppelin-contracts/contracts"
    ],
    "link": [
        "UsdcVaultL2:susds=SUsdsMock",
        "UsdcVaultL2:usdc=UsdcMock",
        "UsdcVaultL2:psm=Psm3Mock",
        "UsdcVaultL2:rateProvider=RateProviderMock",
        "Psm3Mock:usdc=UsdcMock",
        "Psm3Mock:usds=UsdsMock",
        "Psm3Mock:susds=SUsdsMock",
        "Psm3Mock:rateProvider=RateProviderMock"
    ],
    "verify": "UsdcVaultL2:UsdcVaultL2.spec",
    "smt_timeout": "7200",
    "global_timeout": "7200",
    "prover_args": [
        " -mediumTimeout 20 -lowTimeout 20 -tinyTimeout 20 -depth 20",
        " -s [z3:def{randomSeed=1},z3:def{randomSeed=2},z3:def{randomSeed=3},z3:def{randomSeed=4},z3:def{randomSeed=5},z3:def{randomSeed=6},z3:def{randomSeed=7},z3:def{randomSeed=8},z3:def{randomSeed=9},z3:def{randomSeed=10}]"
    ],
    "rule_sanity": "basic",
    "optimistic_loop": true,
    "multi_assert_check": true,
    "parametric_contracts": ["UsdcVaultL2"],
    "build_cache": true,
    "msg": "UsdcVaultL2"
}