-
Notifications
You must be signed in to change notification settings - Fork 10
/
why3.conf
81 lines (71 loc) · 1.45 KB
/
why3.conf
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
[main]
magic = 14
memlimit = 16000
running_provers_max = 8
timelimit = 120
[strategy]
code = "start:
c Z3,4.8.12 1 1000
t split_vc start
c CVC4,1.8 10 2000
t introduce_premises afterintro
afterintro:
t inline_goal afterinline
g trylongertime
afterinline:
t split_all_full start
trylongertime:
c Alt-Ergo,2.4.1 30 4000
c CVC4,1.8 30 4000
c Z3,4.8.12 30 4000
"
desc = "Automatic@ run@ of@ provers@ and@ most@ useful@ transformations"
name = "PROVE_EVERYTHING"
shortcut = "4"
[strategy]
code = "start:
c Z3,4.8.12 1 1000
t split_vc start
c CVC4,1.8 10 2000
t introduce_premises afterintro
afterintro:
t inline_goal afterinline
g trylongertime
afterinline:
t split_all_full start
trylongertime:
c Alt-Ergo,2.4.1 30 4000
c CVC4,1.8 30 4000
c Z3,4.8.12 30 4000
"
desc = "Automatic@ run@ of@ provers@ and@ most@ useful@ transformations"
name = "EXPERIMENTAL"
shortcut = "7"
[strategy]
code = "start:
c Z3,4.8.12 1 1000
t split_vc start
c Alt-Ergo,2.4.1 1 1000
c CVC4,1.8 1 1000
t introduce_premises afterintro
afterintro:
t inline_goal afterinline
afterinline:
t split_all_full start
"
desc = "Automatic@ run@ of@ provers@ and@ most@ useful@ transformations"
name = "HARD_GOAL_IDENTIFIER"
shortcut = "8"
[strategy]
code = "start:
c Z3,4.8.12 1 1000
t split_vc start
t introduce_premises afterintro
afterintro:
t inline_goal afterinline
afterinline:
t split_all_full start
"
desc = "Automatic@ run@ of@ provers@ and@ most@ useful@ transformations"
name = "Z3_Split_tactic"
shortcut = "9"