PSM3.conf

{
    "files": [
        "spark-psm/src/PSM3.sol",
        "spark-psm/test/mocks/MockRateProvider.sol",
        "harness/GemMock.sol", // Adding this one in order the prover also checks with an invalid asset
        "harness/GemMock.sol:USDCMock",
        "harness/GemMock.sol:USDSMock",
        "harness/GemMock.sol:SUSDSMock"
    ],
    "solc": "solc-0.8.20",
    "solc_optimize": "200",
    "packages": [
        "erc20-helpers=spark-psm/lib/erc20-helpers/src",
        "openzeppelin-contracts/=spark-psm/lib/openzeppelin-contracts",
        "src=spark-psm/src"
    ],
    "link": [
        "PSM3:rateProvider=MockRateProvider",
        "PSM3:usdc=USDCMock",
        "PSM3:usds=USDSMock",
        "PSM3:susds=SUSDSMock",
    ],
    "verify": "PSM3:PSM3.spec",
    "rule_sanity": "basic",
    "multi_assert_check": true,
    "parametric_contracts": ["PSM3"],
    "smt_timeout": "7200",
    "global_timeout": "7200",
    "prover_args": [
        " -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}]"
    ],
    "build_cache": true,
    "msg": "PSM3"
}