diff --git a/CVLByExample/Summarization/GhostSummary/SqrRoot/README.md b/CVLByExample/Summarization/GhostSummary/SqrRoot/README.md index c8c6e416..1fd69d71 100644 --- a/CVLByExample/Summarization/GhostSummary/SqrRoot/README.md +++ b/CVLByExample/Summarization/GhostSummary/SqrRoot/README.md @@ -10,7 +10,7 @@ Run the following spec: As you can see, the prover timed out trying to prove the rule. This is due to the nature of the complex math square root operation. In order to solve this timeout, we can try using a feature of the prover that will automatically use NONDET summarizations for difficult* internal functions. -To enable this option you can add the flag `--auto_nondet_difficult_internal_funcs`, it is already included in the following conf. +To enable this option you can add the flag `--nondet_difficult_funcs`, it is already included in the following conf. Run it using: ```certoraRun runAutoSummarizedSqrRoot.conf``` diff --git a/DEFI/ConstantProductPool/runBroken.conf b/DEFI/ConstantProductPool/runBroken.conf index 583d1217..8b04b667 100644 --- a/DEFI/ConstantProductPool/runBroken.conf +++ b/DEFI/ConstantProductPool/runBroken.conf @@ -14,4 +14,4 @@ // Check the rule is non-vacuous "rule_sanity": "basic" } -// alternatively, run `certoraRun contracts/broken/ConstantProductPoolBroken.sol:ConstantProductPool contracts/DummyERC20A.sol contracts/DummyERC20B.sol --verify ConstantProductPool:certora/spec/ConstantProductPool.spec --optimistic_loop --send_only --msg "CVLExmaple: ConstantProductPool with bugs"` \ No newline at end of file +// alternatively, run `certoraRun contracts/broken/ConstantProductPoolBroken.sol:ConstantProductPool contracts/DummyERC20A.sol contracts/DummyERC20B.sol --verify ConstantProductPool:certora/spec/ConstantProductPool.spec --optimistic_loop --msg "CVLExmaple: ConstantProductPool with bugs"` \ No newline at end of file diff --git a/DEFI/ConstantProductPool/runFixed.conf b/DEFI/ConstantProductPool/runFixed.conf index 975c0bc8..35bb6a07 100644 --- a/DEFI/ConstantProductPool/runFixed.conf +++ b/DEFI/ConstantProductPool/runFixed.conf @@ -15,4 +15,4 @@ "rule_sanity": "basic", "enforce_require_reason": true } -// alternatively, run `certoraRun contracts/broken/ConstantProductPoolBroken.sol:ConstantProductPool contracts/DummyERC20A.sol contracts/DummyERC20B.sol --verify ConstantProductPool:certora/spec/ConstantProductPool.spec --optimistic_loop --send_only --msg "CVLExmaple: ConstantProductPool fixed version"` \ No newline at end of file +// alternatively, run `certoraRun contracts/broken/ConstantProductPoolBroken.sol:ConstantProductPool contracts/DummyERC20A.sol contracts/DummyERC20B.sol --verify ConstantProductPool:certora/spec/ConstantProductPool.spec --optimistic_loop --msg "CVLExmaple: ConstantProductPool fixed version"` \ No newline at end of file