diff --git a/certora/confs/ConsistentState.conf b/certora/confs/ConsistentState.conf index 5da45284..4d064514 100644 --- a/certora/confs/ConsistentState.conf +++ b/certora/confs/ConsistentState.conf @@ -10,11 +10,7 @@ "verify": "MetaMorphoHarness:certora/specs/ConsistentState.spec", "loop_iter": "2", "optimistic_loop": true, - "prover_args": [ - "-depth 3", - "-mediumTimeout 20", - "-timeout 300", - ], + "smt_timeout": "600", "rule_sanity": "basic", "server": "production", "msg": "MetaMorpho Consistent State" diff --git a/certora/confs/Enabled.conf b/certora/confs/Enabled.conf index 650f7489..703bacd5 100644 --- a/certora/confs/Enabled.conf +++ b/certora/confs/Enabled.conf @@ -11,7 +11,9 @@ "-depth 3", "-mediumTimeout 20", "-timeout 1000", + "-smt_easy_LIA true", ], + "smt_timeout": "7000", "rule_sanity": "basic", "server": "production", "msg": "MetaMorpho Enabled" diff --git a/certora/confs/Liveness.conf b/certora/confs/Liveness.conf index ed583baf..f391344c 100644 --- a/certora/confs/Liveness.conf +++ b/certora/confs/Liveness.conf @@ -16,10 +16,9 @@ "loop_iter": "2", "optimistic_loop": true, "prover_args": [ - "-depth 3", - "-mediumTimeout 20", - "-timeout 120", + "-smt_easy_LIA true", ], + "smt_timeout": "7000", "rule_sanity": "basic", "server": "production", "msg": "MetaMorpho Liveness" diff --git a/certora/confs/Range.conf b/certora/confs/Range.conf index 383bcc8d..13b869d3 100644 --- a/certora/confs/Range.conf +++ b/certora/confs/Range.conf @@ -7,9 +7,11 @@ "loop_iter": "2", "optimistic_loop": true, "prover_args": [ - "-depth 3", - "-mediumTimeout 20", + "-depth 0", "-timeout 300", + "-smt_nonLinearArithmetic true", + "-adaptiveSolverConfig false", + "-solvers [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", "server": "production", diff --git a/certora/confs/Reverts.conf b/certora/confs/Reverts.conf index 15b75556..0960539b 100644 --- a/certora/confs/Reverts.conf +++ b/certora/confs/Reverts.conf @@ -20,7 +20,7 @@ "prover_args": [ "-depth 5", "-mediumTimeout 40", - "-newSplitParallel true", + "-splitParallel true", "-splitParallelInitialDepth 4", "-splitParallelTimelimit 7000", "-adaptiveSolverConfig false",