-
Notifications
You must be signed in to change notification settings - Fork 0
/
Copy pathkontrol.toml
100 lines (97 loc) · 3.92 KB
/
kontrol.toml
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
[build.default]
foundry-project-root = '.'
regen = false
rekompile = false
verbose = false
debug = false
require = 'src/test/kontrol/term-lemmas.k'
module-import = 'RepoTokenListInvariantsTest:TERM-LEMMAS'
ast = true
auxiliary-lemmas = true
[prove.setup]
foundry-project-root = '.'
verbose = false
debug = false
max-depth = 100000
max-iterations = 10000
reinit = false
cse = false
workers = 1
max-frontier-parallel = 6
maintenance-rate = 128
assume-defined = true
no-log-rewrites = true
no-stack-checks = true
kore-rpc-command = 'kore-rpc-booster --no-post-exec-simplify --equation-max-recursion 20 --equation-max-iterations 1000'
failure-information = true
counterexample-information = true
minimize-proofs = false
fail-fast = true
smt-timeout = 16000
smt-retry-limit = 0
break-every-step = false
break-on-jumpi = false
break-on-calls = false
break-on-storage = false
break-on-basic-blocks = false
break-on-cheatcodes = false
auto_abstract = true
run-constructor = false
bmc-depth = 2
match-test = [
"RepoTokenListInvariantsTest.setUp",
"TermAuctionListInvariantsTest.setUp",
]
ast = true
[prove.tests]
foundry-project-root = '.'
verbose = true
debug = false
max-depth = 100000
max-iterations = 10000
reinit = false
cse = false
workers = 1
max-frontier-parallel = 6
maintenance-rate = 128
assume-defined = true
no-log-rewrites = true
no-stack-checks = true
kore-rpc-command = 'kore-rpc-booster --no-post-exec-simplify --equation-max-recursion 20 --equation-max-iterations 1000'
failure-information = true
counterexample-information = true
minimize-proofs = false
fail-fast = true
smt-timeout = 16000
smt-retry-limit = 0
break-every-step = false
break-on-jumpi = false
break-on-calls = false
break-on-storage = false
break-on-basic-blocks = false
break-on-cheatcodes = false
auto_abstract = true
run-constructor = false
match-test = [
"RepoTokenListInvariantsTest.testInsertSortedNewToken",
"RepoTokenListInvariantsTest.testInsertSortedDuplicateToken",
"RepoTokenListInvariantsTest.testRemoveAndRedeemMaturedTokens",
"RepoTokenListInvariantsTest.testGetCumulativeDataEmpty",
"RepoTokenListInvariantsTest.testGetPresentValueEmpty",
"RepoTokenListInvariantsTest.testGetPresentTotalValue",
"RepoTokenListInvariantsTest.testGetCumulativeRepoTokenData",
"TermAuctionListInvariantsTest.testInsertPendingNewOffer",
"TermAuctionListInvariantsTest.testInsertPendingDuplicateOffer",
"TermAuctionListInvariantsTest.testRemoveCompleted",
"TermAuctionListInvariantsTest.testGetCumulativeDataEmpty",
"TermAuctionListInvariantsTest.testGetPresentValueEmpty",
"TermAuctionListInvariantsTest.testGetCumulativeDataNoCompletedAuctions",
"TermAuctionListInvariantsTest.testGetCumulativeDataCompletedAuctions",
"TermAuctionListInvariantsTest.testGetCumulativeOfferData",
"TermAuctionListInvariantsTest.testGetPresentTotalValue",
]
ast = true
[show.default]
foundry-project-root = '.'
verbose = true
debug = false