Empirical Evaluation of: Lower Runtime Bounds for Integer Programs

Comparison of Prover Results

Compare two provers
Prover AProver B
LoAT
Best UB
KoAT
CoFloCo
Loopus
Rank
LoAT
Best UBΩ(1)Ω(n)Ω(n2)Ω(n3)Ω(n4)EXPINFno result
O(1)1320000000
O(n)45125000000
O(n2)9183300000
O(n3)20030000
O(n4)10002000
EXP00000500
INF00000000
no result503130001737

Detailed Result Tables

   (639 examples selected)
Only show examples that
LoAT
KoAT
CoFloCo
Loopus
Rank
Sort by
O(1)O(n)O(n2)O(n3)O(n4)O(n6)O(n8)EXPINFno resultany resultAvg. timeAvg. time (incl. no res.)
LoAT239174363200517376321761ms2399ms
Best UB13217060530050264375--
KoAT125154674211502803591002ms5513ms
CoFloCo11814151220000325314805ms8646ms
Loopus7710345650000403236115ms922ms
Rank90188100000522117485ms1557ms
ExampleLoATKoATCoFloCoLoopusRank
FGPSF09/Beerendonk/01
1 - B + A
83ms, Ω(n), #vars: 2, input, output
A + B + 1
57ms, O(n), #vars: 2, input, output
max(A + -1 * B + 1, 1)
236ms, O(n), #vars: 2, input, output
max(0, A - B)
55ms, O(n), #vars: 2, input, output

97ms, input, aspic, output, errors
FGPSF09/Beerendonk/02
1 + meter
63ms, Ω(n), #vars: 1, input, output
A + B + 1
75ms, O(n), #vars: 2, input, output
max(1 / 2 * A + -1 / 2...
224ms, O(n), #vars: 2, input, output
max(0, A - B)
55ms, O(n), #vars: 2, input, output

89ms, input, aspic, output, errors
FGPSF09/Beerendonk/03
1
81ms, Ω(1), #vars: 0, input, output
A + B + 1
106ms, O(n), #vars: 2, input, output
max(A + -1 * B + 1, 1)
220ms, O(n), #vars: 2, input, output
max(0, A - B)
51ms, O(n), #vars: 2, input, output

83ms, input, aspic
FGPSF09/Beerendonk/04
1
61ms, Ω(1), #vars: 0, input, output
2
23ms, O(1), #vars: 0, input, output
2
224ms, O(1), #vars: 0, input, output
max(0, A - B)
57ms, O(n), #vars: 2, input, output

97ms, input, aspic, output, errors
FGPSF09/Beerendonk/05
1
197ms, Ω(1), #vars: 0, input, output
2
24ms, O(1), #vars: 0, input, output
max(A + 1, 1)
182ms, O(n), #vars: 1, input, output
1
59ms, O(1), #vars: 0, input, output
4
87ms, O(1), #vars: 0, input, aspic, output
FGPSF09/Beerendonk/06
1
80ms, Ω(1), #vars: 0, input, output
2
25ms, O(1), #vars: 0, input, output
max(A + 1, 1)
240ms, O(n), #vars: 1, input, output
1
46ms, O(1), #vars: 0, input, output
4
102ms, O(1), #vars: 0, input, aspic, output
FGPSF09/Beerendonk/07
1
81ms, Ω(1), #vars: 0, input, output
2
22ms, O(1), #vars: 0, input, output
max(1 / 3 * A + 1, 1)
205ms, O(n), #vars: 1, input, output
1
46ms, O(1), #vars: 0, input, output
6
84ms, O(1), #vars: 0, input, aspic, output
FGPSF09/Beerendonk/08
1 + B
261ms, Ω(n), #vars: 1, input, output
B + 1
117ms, O(n), #vars: 1, input, output
max(1, max(0, min(B, A...
235ms, O(n), #vars: 2, input, output
max(B, 0)
61ms, O(n), #vars: 1, input, output

85ms, input, aspic, output, errors
FGPSF09/Beerendonk/09
1 - B + C
310ms, Ω(n), #vars: 2, input, output
A + B + 1
81ms, O(n), #vars: 2, input, output
max(1, max(0, min(A + ...
217ms, O(n), #vars: 3, input, output
max(0, C - B)
55ms, O(n), #vars: 2, input, output

84ms, input, aspic, output, errors
FGPSF09/Beerendonk/10
1
1903ms, Ω(1), #vars: 0, input, output
2 * A + 2
111ms, O(n), #vars: 1, input, output
max(A + 1, 2)
264ms, O(n), #vars: 1, input, output

777ms, input, output

143ms, input, aspic, output, errors
FGPSF09/Beerendonk/11
1 + B
376ms, Ω(n), #vars: 1, input, output
B + 4
149ms, O(n), #vars: 1, input, output
max(B + 1, 3, A + 2)
465ms, O(n), #vars: 2, input, output
max(0, B + max(0, min(...
88ms, O(n), #vars: 1, input, output

110ms, input, aspic, output, errors
FGPSF09/Beerendonk/13
1 + A
156ms, Ω(n), #vars: 1, input, output
A + 2
101ms, O(n), #vars: 1, input, output
max(B + 2, 2, A + 1)
254ms, O(n), #vars: 2, input, output
max(0, A + max(0, min(...
72ms, O(n), #vars: 1, input, output

99ms, input, aspic, output, errors
FGPSF09/Beerendonk/15
1
267ms, Ω(1), #vars: 0, input, output
2 * A + 2 * B + 1
160ms, O(n), #vars: 2, input, output
max(A + B + 1, 1, max(...
315ms, O(n), #vars: 2, input, output
1 + max(A, 0) + max(0,...
109ms, O(n), #vars: 2, input, output

76ms, input, aspic, aspic (errors)
FGPSF09/Beerendonk/16
1
418ms, Ω(1), #vars: 0, input, output
2 * A + 2 * B + 2 * C + 1
172ms, O(n), #vars: 3, input, output
max(A + B + -1 * C + 1...
326ms, O(n), #vars: 3, input, output
1 + max(A, 0) + max(0,...
62ms, O(n), #vars: 3, input, output

76ms, input, aspic, aspic (errors)
FGPSF09/Beerendonk/17
1
323ms, Ω(1), #vars: 0, input, output
3 * A + 3 * B + 1
231ms, O(n), #vars: 2, input, output
max(A + B + 1, 1, max(...
411ms, O(n), #vars: 2, input, output
max(0, A + B) + max(0,...
119ms, O(n2), #vars: 1, input, output

78ms, input, aspic, output, errors
FGPSF09/Beerendonk/18
1 + A
456ms, Ω(n), #vars: 1, input, output
2 * A + B + 2
309ms, O(n), #vars: 2, input, output
max(A + B + 1, A + 1, ...
308ms, O(n), #vars: 2, input, output
1 + max(B, 0) + max(A,...
91ms, O(n), #vars: 1, input, output

91ms, input, aspic, aspic (errors)
FGPSF09/Beerendonk/19
1 - B + A
500ms, Ω(n), #vars: 2, input, output
2 * A + 3 * B + C + 2
256ms, O(n), #vars: 3, input, output
max(A + -2 * B + C + 1...
359ms, O(n), #vars: 3, input, output
1 + max(0, A - B) + ma...
97ms, O(n), #vars: 2, input, output

71ms, input, aspic, aspic (errors)
FGPSF09/Beerendonk/20
3 + A
110ms, Ω(n), #vars: 1, input, output
A + 3
114ms, O(n), #vars: 1, input, output
max(A + 3, 1)
247ms, O(n), #vars: 1, input, output
max(A, 0) + max(A, 0) ...
65ms, O(n), #vars: 1, input, output

97ms, input, aspic, output, errors
FGPSF09/Beerendonk/21
3 - B + A
134ms, Ω(n), #vars: 2, input, output
A + B + 3
98ms, O(n), #vars: 2, input, output
max(-1 * B + C + 3, 1)
284ms, O(n), #vars: 2, input, output
max(0, A - B) + max(0,...
65ms, O(n), #vars: 2, input, output

85ms, input, aspic, output, errors
FGPSF09/Beerendonk/22
3 + B
138ms, Ω(n), #vars: 1, input, output
4 * A + B + 1
163ms, O(n), #vars: 2, input, output
max(2 * A + B + 1, 2 *...
301ms, O(n), #vars: 2, input, output
max(A, 0) + max(B, 0) ...
71ms, O(n), #vars: 1, input, output

92ms, input, aspic, output, errors
FGPSF09/Beerendonk/23
3 - B + C
211ms, Ω(n), #vars: 2, input, output
4 * A + 5 * B + C + 1
578ms, O(n), #vars: 3, input, output
max(2 * A + -3 * B + C...
491ms, O(n), #vars: 3, input, output
max(0, A - B) + max(0,...
71ms, O(n), #vars: 2, input, output

106ms, input, aspic, output, errors
FGPSF09/Beerendonk/24
3 + A
284ms, Ω(n), #vars: 1, input, output
2 * A + 2 * B + 7
189ms, O(n), #vars: 2, input, output
max(B + 3, 1, A + 3)
261ms, O(n), #vars: 2, input, output
max(A, 0) + max(A, 0) ...
86ms, O(n), #vars: 1, input, output

92ms, input, aspic, output, errors
FGPSF09/CAV02/practical1
1 + 1 / 2 * A^2 + 5 / ...
101ms, Ω(n2), #vars: 1, input, output
16 * A + 4 * A^2 + 13
383ms, O(n2), #vars: 1, input, output
max(3, (A + 2) * A + 1...
324ms, O(n2), #vars: 1, input, output
max(0, A + 1) + max(0,...
63ms, O(n2), #vars: 1, input, output

97ms, input, aspic, output, errors
FGPSF09/CAV02/practical2
2 + meter
97ms, Ω(n), #vars: 1, input, output
49927 * B + 5038821
1062ms, O(n), #vars: 1, input, output
max(56 / 11, -1 / 11 *...
829ms, O(n), #vars: 1, input, output
max(0, 9 * max(0, 101 ...
129ms, O(n), #vars: 1, input, output

144ms, input, aspic, output
FGPSF09/CAV05/c.05
1
462ms, Ω(1), #vars: 0, input, output
2 * A + 2 * B + 3
187ms, O(n), #vars: 2, input, output
max(A + B + -1, 1)
224ms, O(n), #vars: 2, input, output
max(A, 0) + max(A, 0) ...
125ms, O(n), #vars: 1, input, output

92ms, input, aspic
FGPSF09/ESOP08/abstractions
1 + B
131ms, Ω(n), #vars: 1, input, output

2394ms, input, output

257ms, input, output

72ms, input, output

89ms, input, aspic, output, errors
FGPSF09/LICS04/c.01
4
305ms, Ω(1), #vars: 0, input, output
10 * A + 2 * A^2 + 9
192ms, O(n2), #vars: 1, input, output
max(2 * A + 3, 4, A + ...
459ms, O(n2), #vars: 1, input, output
max(0, A + 1) + max(0,...
86ms, O(n2), #vars: 1, input, output

94ms, input, aspic
FGPSF09/LICS04/choice
1 + A
146ms, Ω(n), #vars: 1, input, output

3519ms, input, output

276ms, input, output
max(B, A, 0)
81ms, O(n), #vars: 2, input, output

99ms, input, aspic, output, errors
FGPSF09/PLDI06/c.03
2 + B - C
212ms, Ω(n), #vars: 2, input, output
5 * A + 2 * B + 3 * C + 4
121ms, O(n), #vars: 3, input, output
max(1, A + -1 * B + ma...
313ms, O(n), #vars: 2, input, output
max(0, max(0, B + 1 + ...
113ms, O(n2), #vars: 2, input, output

100ms, input, aspic, output, errors
FGPSF09/PLDI06/c.04
1
200ms, Ω(1), #vars: 0, input, output
A + B + 2
137ms, O(n), #vars: 2, input, output
max(A + -1 * B + 1, 2)
341ms, O(n), #vars: 2, input, output
max(0, A - B) + max(0,...
85ms, O(n), #vars: 2, input, output

84ms, input, aspic
FGPSF09/SAS05/c.02
9 / 2 - 1 / 2 * (1 + A...
173ms, Ω(n2), #vars: 1, input, output
149 * A + 6 * A^2 + 336
152ms, O(n2), #vars: 1, input, output
max(A + 3, 2, max(A + ...
365ms, O(n2), #vars: 1, input, output
max(0, A + 1) + max(0,...
80ms, O(n2), #vars: 1, input, output

90ms, input, aspic, output, errors
FGPSF09/TACAS01/terminate
1
84ms, Ω(1), #vars: 0, input, output
A + B + C + 102
99ms, O(n), #vars: 3, input, output
max(-1 / 2 * A + 1 / 2...
262ms, O(n), #vars: 3, input, output
max(0, B + 1 + 0 - C)
62ms, O(n), #vars: 2, input, output

73ms, input, aspic, output, errors
FGPSF09/VMCAI04/complete1
1 - B + A
153ms, Ω(n), #vars: 2, input, output
A + B + 1
104ms, O(n), #vars: 2, input, output
max(A + -1 * B + 1, 1)
301ms, O(n), #vars: 2, input, output
max(0, A - B)
208ms, O(n), #vars: 2, input, output

158ms, input, aspic
FGPSF09/VMCAI04/complete2
1
96ms, Ω(1), #vars: 0, input, output
5
261ms, O(1), #vars: 0, input, output

237ms, input, output
1
63ms, O(1), #vars: 0, input, output

143ms, input, aspic, output, errors
FGPSF09/VMCAI04/complete3
1 + 1 / 2 * A^2 + 5 / ...
97ms, Ω(n2), #vars: 1, input, output
16 * A + 4 * A^2 + 13
384ms, O(n2), #vars: 1, input, output
max(3, (A + 2) * A + 1...
333ms, O(n2), #vars: 1, input, output
max(0, A + 1) + max(0,...
68ms, O(n2), #vars: 1, input, output

88ms, input, aspic, output, errors
FGPSF09/VMCAI04/complete4
3 + (1 + A) * free + 2...
151ms, INF, #vars: 2, input, output

2373ms, input, output

257ms, input, output

66ms, input, output

108ms, input, aspic, output, errors
FGPSF09/VMCAI05/poly1
nonlinear
1
75ms, Ω(1), #vars: 0, input, output

5610ms, input, output

306ms, input, output

56ms, input, output
Non-linear example not handled by prover.
FGPSF09/VMCAI05/poly2
1
77ms, Ω(1), #vars: 0, input, output

6182ms, input, output

273ms, input, output

56ms, input, output

93ms, input, aspic
FGPSF09/VMCAI05/poly3
nonlinear
2 + A
125ms, Ω(n), #vars: 1, input, output

5749ms, input, output

216ms, input, output

102ms, input, output
Non-linear example not handled by prover.
FGPSF09/VMCAI05/poly4
1 - B + A
574ms, Ω(n), #vars: 2, input, output
2 * A + 2 * B + 2 * C ...
299ms, O(n), #vars: 4, input, output
max(A + -1 * B + C + -...
683ms, O(n), #vars: 4, input, output
max(0, C - D) + max(0,...
73ms, O(n), #vars: 2, input, output

100ms, input, aspic, output, errors
FGPSF09/new/unsatCond2
nonlinear
1
65ms, Ω(1), #vars: 0, input, output

100ms, input, output

232ms, input, output

44ms, input, output
Non-linear example not handled by prover.
FGPSF09/patrs/div
1
83ms, Ω(1), #vars: 0, input, output
A + B + 3
97ms, O(n), #vars: 2, input, output
2
211ms, O(1), #vars: 0, input, output
max(0, B - A)
82ms, O(n), #vars: 2, input, output

75ms, input, aspic
FGPSF09/patrs/increase1
1 - B + A
86ms, Ω(n), #vars: 2, input, output
A + B + 1
59ms, O(n), #vars: 2, input, output
max(A + -1 * B + 1, 1)
209ms, O(n), #vars: 2, input, output
max(0, A - B)
53ms, O(n), #vars: 2, input, output

81ms, input, aspic, output, errors
FGPSF09/patrs/increase2
1 - B - C + A
115ms, Ω(n), #vars: 3, input, output
2 * A + 2 * B + 2 * C + 1
107ms, O(n), #vars: 3, input, output
max(A + -1 * B + -1 * ...
283ms, O(n), #vars: 3, input, output
max(0, max(0, A - C - ...
84ms, O(n2), #vars: 3, input, output

79ms, input, aspic, output, errors
FGPSF09/patrs/increase3
1 - B + A
235ms, Ω(n), #vars: 2, input, output
4 * A + 2 * B + 2 * C + 3
106ms, O(n), #vars: 3, input, output
max(2 * A + -1 * B + -...
257ms, O(n), #vars: 3, input, output
max(0, A - C) + max(0,...
86ms, O(n), #vars: 2, input, output

85ms, input, aspic, output, errors
FGPSF09/patrs/increase4
1 - B + A
84ms, Ω(n), #vars: 2, input, output
A + B + 1
69ms, O(n), #vars: 2, input, output
max(A + -1 * B + 1, 1)
252ms, O(n), #vars: 2, input, output
max(0, A - B)
49ms, O(n), #vars: 2, input, output

88ms, input, aspic, output, errors
FGPSF09/patrs/pasta/a.01
1 + 1 / 2 * A^2 + 5 / ...
193ms, Ω(n2), #vars: 1, input, output
4 * A + 2 * A^2 + 1
169ms, O(n2), #vars: 1, input, output
max(A + 2, 2, max(A, (...
376ms, O(n2), #vars: 1, input, output
max(A, 0) + max(0, max...
78ms, O(n2), #vars: 1, input, output

91ms, input, aspic, output, errors
FGPSF09/patrs/pasta/a.02
1
1563ms, Ω(1), #vars: 0, input, output

3067ms, input, output

319ms, input, output

113ms, input, output

107ms, input, aspic, output, errors
FGPSF09/patrs/pasta/a.03
-7 + 4 * A
1797ms, Ω(n), #vars: 1, input, output
174 * A + 162 * B + 36...
664ms, O(n2), #vars: 2, input, output
max(-2 * A + B + 5, 17...
5224ms, O(n2), #vars: 2, input, output

141ms, input, output

82ms, input, aspic
FGPSF09/patrs/pasta/a.04
1 - B + A
86ms, Ω(n), #vars: 2, input, output
A + B + 1
57ms, O(n), #vars: 2, input, output
max(A + -1 * B + 1, 1)
248ms, O(n), #vars: 2, input, output
max(0, A - B)
48ms, O(n), #vars: 2, input, output

72ms, input, aspic, output, errors
FGPSF09/patrs/pasta/a.05
1 - B + A
88ms, Ω(n), #vars: 2, input, output
A + B + 1
56ms, O(n), #vars: 2, input, output
max(A + -1 * B + 1, 1)
253ms, O(n), #vars: 2, input, output
max(0, A - B)
56ms, O(n), #vars: 2, input, output

77ms, input, aspic, output, errors
FGPSF09/patrs/pasta/a.06
1 + meter
66ms, Ω(n), #vars: 1, input, output
A + B + C + 1
81ms, O(n), #vars: 3, input, output
max(1 / 2 * A + -1 / 2...
264ms, O(n), #vars: 3, input, output
max(0, A - C - B)
53ms, O(n), #vars: 3, input, output

93ms, input, aspic, output, errors
FGPSF09/patrs/pasta/a.07
1 - B + A
301ms, Ω(n), #vars: 2, input, output
A + B + 1
83ms, O(n), #vars: 2, input, output
max(1, max(0, min(A + ...
321ms, O(n), #vars: 3, input, output
max(0, A - C)
57ms, O(n), #vars: 2, input, output

75ms, input, aspic, output, errors
FGPSF09/patrs/pasta/a.08
1 - B + A
93ms, Ω(n), #vars: 2, input, output
A + B + 1
74ms, O(n), #vars: 2, input, output
max(A + -1 * B + 1, 1)
215ms, O(n), #vars: 2, input, output
max(0, A - B)
52ms, O(n), #vars: 2, input, output

83ms, input, aspic, output, errors
FGPSF09/patrs/pasta/a.09
1
85ms, Ω(1), #vars: 0, input, output
A + B + 2
117ms, O(n), #vars: 2, input, output
max(A + -1 * B + 2, 1)
267ms, O(n), #vars: 2, input, output
max(0, A + 1 + 0 - B)
53ms, O(n), #vars: 2, input, output

84ms, input, aspic
FGPSF09/patrs/pasta/a.10
1 - B + A
195ms, Ω(n), #vars: 2, input, output
2 * A + 2 * B + 2
162ms, O(n), #vars: 2, input, output
max(A + -1 * B + 1, 1,...
274ms, O(n), #vars: 2, input, output

139ms, input, output

85ms, input, aspic, output, errors
FGPSF09/patrs/pasta/a.11
1 - 2 * B + 2 * A
316ms, Ω(n), #vars: 2, input, output
16 * A + 6 * B + 10 * ...
311ms, O(n), #vars: 3, input, output
max(6 * A + -4 * B + -...
549ms, O(n), #vars: 3, input, output
max(0, max(0, A - C) *...
138ms, O(n3), #vars: 2, input, output

86ms, input, aspic, output, errors
FGPSF09/patrs/sqrt
1
83ms, Ω(1), #vars: 0, input, output
D + 2
151ms, O(n), #vars: 1, input, output
max(1 / 2 * D + 2, 2)
306ms, O(n), #vars: 1, input, output
max(D, 0)
50ms, O(n), #vars: 1, input, output

90ms, input, aspic
FGPSF09/patrs/sumto_no_if
2 + B - A
83ms, Ω(n), #vars: 2, input, output
A + B + 3
66ms, O(n), #vars: 2, input, output
max(-1 * A + B + 3, 2)
201ms, O(n), #vars: 2, input, output
max(0, B + 1 + 0 - A)
60ms, O(n), #vars: 2, input, output

100ms, input, aspic, output, errors
KoAT-2013/sect1-lin
2 + B + 2 * A
76ms, Ω(n), #vars: 2, input, output
2 * A + B + 2
183ms, O(n), #vars: 2, input, output

216ms, input, output
max(A, 0) + max(0, max...
59ms, O(n), #vars: 1, input, output

91ms, input, aspic, output, errors
KoAT-2013/sect1-quad
3 + 1 / 2 * A^2 + B + ...
79ms, Ω(n2), #vars: 2, input, output
2 * A + B + A^2 + 2
232ms, O(n2), #vars: 2, input, output

221ms, input, output
max(A, 0) + max(0, max...
58ms, O(n2), #vars: 1, input, output

66ms, input, aspic
KoAT-2013/sect2
2 + 7 / 2 * B + 1 / 2 ...
133ms, Ω(n2), #vars: 1, input, output
5 * B + 2 * B^2 + 2
312ms, O(n2), #vars: 1, input, output
max(2 * B + 3, 2, B + ...
379ms, O(n2), #vars: 1, input, output
max(B, 0) + max(B, 0) ...
90ms, O(n2), #vars: 1, input, output

95ms, input, aspic, output, errors
KoAT-2013/sect5-len
1 + B
56ms, Ω(n), #vars: 1, input, output
B + 2
96ms, O(n), #vars: 1, input, output
max(B + 2, 2)
187ms, O(n), #vars: 1, input, output
max(B, 0)
42ms, O(n), #vars: 1, input, output

79ms, input, aspic, output, errors
KoAT-2013/sect5-sumSum
1 + 5 / 2 * B + 1 / 2 ...
92ms, Ω(n2), #vars: 1, input, output
11 * B + 4 * B^2 + 7
825ms, O(n2), #vars: 1, input, output
max(1, (B + 2) * B + 1)
254ms, O(n2), #vars: 1, input, output
max(B, 0) + max(0, max...
61ms, O(n2), #vars: 1, input, output

77ms, input, aspic
KoAT-2014/adding-exp-growth1
2 + pow(2, A) + A
95ms, EXP, #vars: 1, input, output
pow(2, A) + A + 2
251ms, EXP, #vars: 1, input, output

264ms, input, output

65ms, input, output

19ms, input
KoAT-2014/adding-exp-growth2
2 + C + pow(2, C)
97ms, EXP, #vars: 1, input, output
pow(2, 2 * C) + C + 3
302ms, EXP, #vars: 1, input, output

286ms, input, output

69ms, input, output

21ms, input
KoAT-2014/adding-exp-growth3
2 + pow(2, A) + 2 * A
96ms, EXP, #vars: 1, input, output
pow(2, 2 * A + 1) + 4 ...
258ms, EXP, #vars: 1, input, output

252ms, input, output

69ms, input, output

13ms, input
KoAT-2014/nesting-ex1
3 + 4 / 3 * B + 1 / 2 ...
114ms, Ω(n3), #vars: 1, input, output
15 * B + 12 * B^2 + 4 ...
927ms, O(n3), #vars: 1, input, output

506ms, input, output
max(B, 0) + max(0, max...
104ms, O(n3), #vars: 1, input, output

16ms, input
KoAT-2014/scaling-doubly-exp-growth
3 + pow(2, A) + pow(2,...
122ms, EXP, #vars: 1, input, output
2 * pow(2, A) * 2 + po...
452ms, EXP, #vars: 1, input, output

444ms, input, output

113ms, input, output

19ms, input
KoAT-2014/scaling-exp-growth
2 + B + pow(2, B) * A
100ms, EXP, #vars: 2, input, output
pow(2, B) * A + B + A + 2
247ms, EXP, #vars: 2, input, output

248ms, input, output

73ms, input, output

21ms, input
SAS10/aaron2
1
1049ms, Ω(1), #vars: 0, input, output
4 * A + 4 * C + 4 * E + 7
841ms, O(n), #vars: 3, input, output

169ms, input, output, errors

42ms, input, output

88ms, input, aspic
SAS10/ackermann
1
693ms, Ω(1), #vars: 0, input, output
16 * A + 4
217ms, O(n), #vars: 1, input, output
max(4 * A + 2, 5)
286ms, O(n), #vars: 1, input, output
max(A, 0)
76ms, O(n), #vars: 1, input, output
max(1 + A__o' + 1 + A_...
112ms, O(n), #vars: 1, input, aspic, output
SAS10/ax
1 + A
671ms, Ω(n), #vars: 1, input, output
2 * A^2 + 10 * A + 14
297ms, O(n2), #vars: 1, input, output
max(3, 2 * A + -6 + ma...
469ms, O(n2), #vars: 1, input, output

81ms, input, output
max(1 + 1 + -2 * A__o'...
138ms, O(n2), #vars: 1, input, aspic, output
SAS10/complex
6
5354ms, Ω(1), #vars: 0, input, output
248 * A + 45 * C + 8960
1211ms, O(n), #vars: 2, input, output

164ms, input, output, errors

42ms, input, output

60002ms, input, aspic, output, errors
SAS10/counterex1
2 + A
1220ms, Ω(n), #vars: 1, input, output

29234ms, input, output

169ms, input, output, errors

40ms, input, output
1 + 1 + A__o' + -1 + 1...
285ms, O(n), #vars: 1, input, aspic, output, errors
SAS10/cousot9
2 + C
704ms, Ω(n), #vars: 1, input, output
2 * A^2 + 8 * A + C + 12
419ms, O(n2), #vars: 2, input, output

161ms, input, output, errors

40ms, input, output
max(4, 1 + A__o' + 1 + 1)
148ms, O(n), #vars: 1, input, aspic, output, errors
SAS10/determinant
11 / 6 - (-1 + A)^2 * ...
1276ms, Ω(n3), #vars: 1, input, output
28 * A + 44 * A^2 + 16...
495ms, O(n3), #vars: 1, input, output
max(A + 4, 5, max((A +...
1674ms, O(n3), #vars: 1, input, output
max(0, -1 + min(A, A +...
124ms, O(n3), #vars: 1, input, output
max(2 + A__o' + -1 + 1...
173ms, O(n3), #vars: 1, input, aspic, output
SAS10/easy1
1
1042ms, Ω(1), #vars: 0, input, output
126
634ms, O(1), #vars: 0, input, output

159ms, input, output, errors

120ms, input, output
max(44, 84)
137ms, O(1), #vars: 0, input, aspic, output
SAS10/easy2
1 + A
241ms, Ω(n), #vars: 1, input, output
A + 4
293ms, O(n), #vars: 1, input, output
max(A + 2, 3)
293ms, O(n), #vars: 1, input, output
max(0, D + -1 + max(mi...
56ms, O(n), #vars: 2, input, output
max(2 + A__o' + 1 + 1, 4)
97ms, O(n), #vars: 1, input, aspic, output
SAS10/exmini
1
842ms, Ω(1), #vars: 0, input, output
A + E + G + 107
285ms, O(n), #vars: 3, input, output
max(3, max(0, min(-1 /...
858ms, O(n), #vars: 3, input, output

178ms, input, output

99ms, input, aspic
SAS10/gcd
1
683ms, Ω(1), #vars: 0, input, output
4 * A + 4 * C + 18
463ms, O(n), #vars: 2, input, output

163ms, input, output, errors

38ms, input, output

115ms, input, aspic
SAS10/insertsort
-2 + 2 * A
890ms, Ω(n), #vars: 1, input, output
3 * A^2 + 22 * A + 28
553ms, O(n2), #vars: 1, input, output
max(4, max(3 * A + -6,...
1555ms, O(n2), #vars: 1, input, output
max(0, -1 + min(A, A +...
302ms, O(n2), #vars: 1, input, output
max(2 + -1 + A__o' + -...
252ms, O(n2), #vars: 1, input, aspic, output
SAS10/loops
3
953ms, Ω(1), #vars: 0, input, output
13 * A + 2 * A^2 + 17
516ms, O(n2), #vars: 1, input, output

163ms, input, output, errors

38ms, input, output

85ms, input, aspic
SAS10/maccarthy91
2 + meter
2504ms, Ω(n), #vars: 1, input, output
8 * A + 813
906ms, O(n), #vars: 1, input, output

172ms, input, output, errors

187ms, input, output

154ms, input, aspic, output
SAS10/nd_loop
1
362ms, Ω(1), #vars: 0, input, output
43
210ms, O(1), #vars: 0, input, output
21
285ms, O(1), #vars: 0, input, output
10
70ms, O(1), #vars: 0, input, output
23
125ms, O(1), #vars: 0, input, aspic, output
SAS10/ndecr
A
168ms, Ω(n), #vars: 1, input, output
A + 4
168ms, O(n), #vars: 1, input, output
max(A + 1, 3)
225ms, O(n), #vars: 1, input, output
max(0, A + -2)
44ms, O(n), #vars: 1, input, output
max(2 + -1 + A__o' + 1...
75ms, O(n), #vars: 1, input, aspic, output
SAS10/nestedLoop
1 + C
5310ms, Ω(n), #vars: 1, input, output
12 * A + 12 * C + 6 * ...
1140ms, O(n2), #vars: 3, input, output

186ms, input, output, errors

45ms, input, output

256ms, input, aspic, output
SAS10/perfect
1
2651ms, Ω(1), #vars: 0, input, output
2 * A^2 + 10 * A + 15
665ms, O(n2), #vars: 1, input, output
2
377ms, O(1), #vars: 0, input, output

947ms, input, output

109ms, input, aspic
SAS10/random1d
1 + A
609ms, Ω(n), #vars: 1, input, output
2 * A + 7
304ms, O(n), #vars: 1, input, output
max(A + 2, 3)
336ms, O(n), #vars: 1, input, output

136ms, input, output
max(2 + A__o' + 1 + 1, 4)
125ms, O(n), #vars: 1, input, aspic, output
SAS10/random2d
1
6484ms, Ω(1), #vars: 0, input, output
22 * A + 19
1251ms, O(n), #vars: 1, input, output
max(2 * A + 2, 4)
1409ms, O(n), #vars: 1, input, output

680ms, input, output

218ms, input, aspic, output
SAS10/realbubble
4
2768ms, Ω(1), #vars: 0, input, output
24 * A^2 + 60 * A + 27
875ms, O(n2), #vars: 1, input, output
max(5, max(max(0, min(...
927ms, O(n2), #vars: 1, input, output

45ms, input, output

223ms, input, aspic, output
SAS10/realheapsort
1
14632ms, Ω(1), #vars: 0, input, output
1288422 * A + 714 * A^...
4644ms, O(n2), #vars: 1, input, output

242ms, input, output, errors

63ms, input, output

1243ms, input, aspic
SAS10/realselect
1
3719ms, Ω(1), #vars: 0, input, output
12 * A + 19
727ms, O(n), #vars: 1, input, output
5
400ms, O(1), #vars: 0, input, output

254ms, input, output

220ms, input, aspic, output
SAS10/realshellsort
5
12763ms, Ω(1), #vars: 0, input, output
264 * L + 105 * L^2 + ...
1069ms, O(n3), #vars: 1, input, output

60001ms, input, output

274ms, input, output

351ms, input, aspic
SAS10/relation1
1
16ms, Ω(1), #vars: 0, input, output
3
24ms, O(1), #vars: 0, input, output
3
167ms, O(1), #vars: 0, input, output

43ms, input
5
90ms, O(1), #vars: 0, input, aspic, output
SAS10/rsd
2 + A
864ms, Ω(n), #vars: 1, input, output
6 * A^2 + 43 * A + 9
1152ms, O(n2), #vars: 1, input, output

161ms, input, output, errors

39ms, input, output

107ms, input, aspic
SAS10/sipmabubble
1 + A
885ms, Ω(n), #vars: 1, input, output
72 * A + 36 * A^2 + 40
541ms, O(n2), #vars: 1, input, output

172ms, input, output, errors

40ms, input, output
max(2 + 1 + A__o' + 1 ...
304ms, O(n2), #vars: 1, input, aspic, output
SAS10/speedFails4
2 - B + C
1791ms, Ω(n), #vars: 2, input, output
2 * B + 2 * C + 7
575ms, O(n), #vars: 2, input, output

166ms, input, output, errors

40ms, input, output

112ms, input, aspic
SAS10/speedpldi2
1
1210ms, Ω(1), #vars: 0, input, output
6 * G + 9
435ms, O(n), #vars: 1, input, output
max(2 * G + 1, 3)
467ms, O(n), #vars: 1, input, output

230ms, input, output
max(4, 2 + G__o' + G__...
217ms, O(n), #vars: 2, input, aspic, output
SAS10/speedpldi3
2 + A
1745ms, Ω(n), #vars: 1, input, output
2 * A * C + 8 * C + A + 9
396ms, O(n2), #vars: 2, input, output
max(3, 2 * C + -2 + ma...
1018ms, O(n2), #vars: 2, input, output

393ms, input, output
max(5, 2 + C__o' * A__...
351ms, O(n2), #vars: 2, input, aspic, output
SAS10/speedpldi4
2
1115ms, Ω(1), #vars: 0, input, output
2 * A + 2 * C + 17
382ms, O(n), #vars: 2, input, output
max(-1 * A + C + 5, 6,...
3237ms, O(n), #vars: 2, input, output

256ms, input, output

93ms, input, aspic
SAS10/terminate
1
835ms, Ω(1), #vars: 0, input, output
A + E + 207
285ms, O(n), #vars: 2, input, output
max(3, max(0, min(-1 /...
755ms, O(n), #vars: 3, input, output

155ms, input, output

85ms, input, aspic
SAS10/wcet1
A
2158ms, Ω(n), #vars: 1, input, output
3 * A + 13
658ms, O(n), #vars: 1, input, output
max(A + 1, 3)
645ms, O(n), #vars: 1, input, output

169ms, input, output

111ms, input, aspic
SAS10/wcet2
4
1254ms, Ω(1), #vars: 0, input, output
44 * A + 221
728ms, O(n), #vars: 1, input, output

168ms, input, output, errors

38ms, input, output

60003ms, input, aspic, output
SAS10/while2
2 + A
655ms, Ω(n), #vars: 1, input, output
10 * A + 2 * A^2 + 14
390ms, O(n2), #vars: 1, input, output
max(4, max(0, min(A + ...
424ms, O(n2), #vars: 1, input, output

155ms, input, output
max(4, 2 + A__o' * A__...
125ms, O(n2), #vars: 1, input, aspic, output
SAS10/wise
-1 + C - A
621ms, Ω(n), #vars: 2, input, output
2 * A + 2 * C + 12
364ms, O(n), #vars: 2, input, output

162ms, input, output, errors

40ms, input, output
max(2 + -2 + -1 * C__o...
126ms, O(n), #vars: 2, input, aspic, output
T2/1
F
235ms, Ω(n), #vars: 1, input, output

4389ms, input, output

737ms, input, output

73ms, input, output

302ms, input, aspic
T2/1394-fail
INF
1973ms, INF, #vars: 1, input, output

5560ms, input, output

60001ms, input, output

457ms, input, output

70ms, input, aspic, aspic (errors)
T2/1394-succeed
INF
1822ms, INF, #vars: 1, input, output

5497ms, input, output

51174ms, input, output

523ms, input, output

73ms, input, aspic, aspic (errors)
T2/1394complete-fail
INF
1634ms, INF, #vars: 1, input, output

4993ms, input, output

57747ms, input, output

436ms, input, output

67ms, input, aspic, aspic (errors)
T2/1394complete-succeed
INF
1798ms, INF, #vars: 1, input, output

5584ms, input, output

60004ms, input, output

847ms, input, output

73ms, input, aspic, aspic (errors)
T2/2
F
199ms, Ω(n), #vars: 1, input, output

4024ms, input, output

709ms, input, output

83ms, input, output

326ms, input, aspic
T2/232
-1 / 2 + (-1 + A) * A ...
299ms, Ω(n2), #vars: 1, input, output
A^2 + 3 * A + 2
204ms, O(n2), #vars: 1, input, output
max(1, max(0, (A + -1)...
250ms, O(n2), #vars: 1, input, output
max(0, A + -1) + max(0...
56ms, O(n2), #vars: 1, input, output
max(2, 1 + 3 / 2 * A__...
71ms, O(n2), #vars: 1, input, aspic, output
T2/241
-1 / 2 + (-1 + A) * A ...
312ms, Ω(n2), #vars: 1, input, output
A^2 + 3 * A + 2
202ms, O(n2), #vars: 1, input, output
max(1, max(0, (A + -1)...
198ms, O(n2), #vars: 1, input, output
max(0, A + -1) + max(0...
57ms, O(n2), #vars: 1, input, output
max(2, 1 + 3 / 2 * A__...
15216ms, O(n2), #vars: 1, input, aspic, output
T2/3
INF
31ms, INF, #vars: 1, input, output

119ms, input, output

176ms, input, output

40ms, input, output

71ms, input, aspic, output, errors
T2/5
INF
3876ms, INF, #vars: 1, input, output

23448ms, input, output

2047ms, input, output

488ms, input, output

1011ms, input, aspic, output, errors
T2/6
INF
34ms, INF, #vars: 1, input, output

123ms, input, output

164ms, input, output

42ms, input, output

69ms, input, aspic, output, errors
T2/7
INF
25ms, INF, #vars: 1, input, output

683ms, input, output

211ms, input, output

50ms, input, output

81ms, input, aspic
T2/Loop
1
10774ms, Ω(1), #vars: 0, input, output
111 * C + 111 * E + 11...
1453ms, O(n), #vars: 4, input, output

60002ms, input, output

220ms, input, output

723ms, input, aspic, output
T2/a.10.c
1
49ms, Ω(1), #vars: 0, input, output
42136 * A + 42076 * B ...
345ms, O(n2), #vars: 4, input, output
max(2 * D + -2 * F + 2...
320ms, O(n), #vars: 4, input, output

45ms, input

377ms, input, aspic, output, errors
T2/acqrel-fail
INF
106ms, INF, #vars: 1, input, output

822ms, input, output

454ms, input, output

73ms, input, output

77ms, input, aspic, output, errors
T2/afagp-fail
INF
2129ms, INF, #vars: 1, input, output

60019ms, input

12584ms, input, output, errors

765ms, input, output

72ms, input, aspic, aspic (errors)
T2/afagx1
INF
92ms, INF, #vars: 1, input, output

410ms, input, output

315ms, input, output

70ms, input, output

82ms, input, aspic, output, errors
T2/agafp
INF
5300ms, INF, #vars: 1, input, output

60016ms, input

60001ms, input, output

2029ms, input, output

75ms, input, aspic, aspic (errors)
T2/apchild-accepted
3 + free_30
2499ms, INF, #vars: 1, input, output

23476ms, input, output

60001ms, input, output

1080ms, input, output

71ms, input, aspic, aspic (errors)
T2/apchild-accepted-fail
3 + free_30
2715ms, INF, #vars: 1, input, output

22900ms, input, output

60001ms, input, output

1023ms, input, output

65ms, input, aspic, aspic (errors)
T2/apchild-live
INF
2961ms, INF, #vars: 1, input, output

26782ms, input, output

60001ms, input, output

561ms, input, output

99ms, input, aspic, aspic (errors)
T2/apchildlive-succeed
2 + free_59
3422ms, INF, #vars: 1, input, output

13024ms, input, output

60003ms, input, output

407ms, input, output

64ms, input, aspic, aspic (errors)
T2/array
1
17ms, Ω(1), #vars: 0, input, output
1
16ms, O(1), #vars: 0, input, output
1
217ms, O(1), #vars: 0, input, output

41ms, input
3
76ms, O(1), #vars: 0, input, aspic, output
T2/array1
1
16ms, Ω(1), #vars: 0, input, output
1
17ms, O(1), #vars: 0, input, output
1
144ms, O(1), #vars: 0, input, output

40ms, input
3
81ms, O(1), #vars: 0, input, aspic, output
T2/array2
51
61ms, Ω(1), #vars: 0, input, output
52
90ms, O(1), #vars: 0, input, output
52
168ms, O(1), #vars: 0, input, output
50
56ms, O(1), #vars: 0, input, output
54
102ms, O(1), #vars: 0, input, aspic, output
T2/array3
102
79ms, Ω(1), #vars: 0, input, output
103
183ms, O(1), #vars: 0, input, output
103
389ms, O(1), #vars: 0, input, output
100
70ms, O(1), #vars: 0, input, output
105
87ms, O(1), #vars: 0, input, aspic, output
T2/array_free
43
66ms, Ω(1), #vars: 0, input, output
86
136ms, O(1), #vars: 0, input, output
44
166ms, O(1), #vars: 0, input, output
42
71ms, O(1), #vars: 0, input, output
46
81ms, O(1), #vars: 0, input, aspic, output
T2/array_init
11
66ms, Ω(1), #vars: 0, input, output
13
91ms, O(1), #vars: 0, input, output
12
173ms, O(1), #vars: 0, input, output
10
41ms, O(1), #vars: 0, input, output
14
76ms, O(1), #vars: 0, input, aspic, output
T2/array_init_assign
6
76ms, Ω(1), #vars: 0, input, output
8
182ms, O(1), #vars: 0, input, output
7
206ms, O(1), #vars: 0, input, output
4
62ms, O(1), #vars: 0, input, output
9
92ms, O(1), #vars: 0, input, aspic, output
T2/ase_example
33
100ms, Ω(1), #vars: 0, input, output
85
189ms, O(1), #vars: 0, input, output
34
344ms, O(1), #vars: 0, input, output
30
101ms, O(1), #vars: 0, input, output
36
120ms, O(1), #vars: 0, input, aspic, output
T2/bf10
1
327ms, Ω(1), #vars: 0, input, output
658
3093ms, O(1), #vars: 0, input, output
85
1079ms, O(1), #vars: 0, input, output
80
138ms, O(1), #vars: 0, input, output
91
213ms, O(1), #vars: 0, input, aspic, output
T2/bf11
1
324ms, Ω(1), #vars: 0, input, output
736
3214ms, O(1), #vars: 0, input, output
91
827ms, O(1), #vars: 0, input, output
87
133ms, O(1), #vars: 0, input, output
97
172ms, O(1), #vars: 0, input, aspic, output
T2/bf12
1
311ms, Ω(1), #vars: 0, input, output
814
3063ms, O(1), #vars: 0, input, output
97
785ms, O(1), #vars: 0, input, output
94
126ms, O(1), #vars: 0, input, output
103
202ms, O(1), #vars: 0, input, aspic, output
T2/bf13
1
321ms, Ω(1), #vars: 0, input, output
898
2931ms, O(1), #vars: 0, input, output
103
822ms, O(1), #vars: 0, input, output
101
129ms, O(1), #vars: 0, input, output
109
221ms, O(1), #vars: 0, input, aspic, output
T2/bf14
1
308ms, Ω(1), #vars: 0, input, output
986
3111ms, O(1), #vars: 0, input, output
109
818ms, O(1), #vars: 0, input, output
108
130ms, O(1), #vars: 0, input, output
115
221ms, O(1), #vars: 0, input, aspic, output
T2/bf15
1
315ms, Ω(1), #vars: 0, input, output
1078
3100ms, O(1), #vars: 0, input, output
115
765ms, O(1), #vars: 0, input, output
115
164ms, O(1), #vars: 0, input, output
121
224ms, O(1), #vars: 0, input, aspic, output
T2/bf16
1
318ms, Ω(1), #vars: 0, input, output
1195
3452ms, O(1), #vars: 0, input, output
121
778ms, O(1), #vars: 0, input, output
122
131ms, O(1), #vars: 0, input, output
127
190ms, O(1), #vars: 0, input, aspic, output
T2/bf17
1
307ms, Ω(1), #vars: 0, input, output
1274
3333ms, O(1), #vars: 0, input, output
127
842ms, O(1), #vars: 0, input, output
129
127ms, O(1), #vars: 0, input, output
133
261ms, O(1), #vars: 0, input, aspic, output
T2/bf18
1
317ms, Ω(1), #vars: 0, input, output
1378
3096ms, O(1), #vars: 0, input, output
133
803ms, O(1), #vars: 0, input, output
136
130ms, O(1), #vars: 0, input, output
139
226ms, O(1), #vars: 0, input, aspic, output
T2/bf19
1
325ms, Ω(1), #vars: 0, input, output
1486
3017ms, O(1), #vars: 0, input, output
139
807ms, O(1), #vars: 0, input, output
143
130ms, O(1), #vars: 0, input, output
145
233ms, O(1), #vars: 0, input, aspic, output
T2/bf20
1
331ms, Ω(1), #vars: 0, input, output
1598
3161ms, O(1), #vars: 0, input, output
145
1068ms, O(1), #vars: 0, input, output
150
137ms, O(1), #vars: 0, input, output
151
230ms, O(1), #vars: 0, input, aspic, output
T2/bf5
1
325ms, Ω(1), #vars: 0, input, output
342
3029ms, O(1), #vars: 0, input, output
55
780ms, O(1), #vars: 0, input, output
45
126ms, O(1), #vars: 0, input, output
61
162ms, O(1), #vars: 0, input, aspic, output
T2/bf6
1
325ms, Ω(1), #vars: 0, input, output
394
3135ms, O(1), #vars: 0, input, output
61
851ms, O(1), #vars: 0, input, output
52
142ms, O(1), #vars: 0, input, output
67
235ms, O(1), #vars: 0, input, aspic, output
T2/bf7
1
331ms, Ω(1), #vars: 0, input, output
454
3271ms, O(1), #vars: 0, input, output
67
803ms, O(1), #vars: 0, input, output
59
134ms, O(1), #vars: 0, input, output
73
235ms, O(1), #vars: 0, input, aspic, output
T2/bf8
1
318ms, Ω(1), #vars: 0, input, output
518
3127ms, O(1), #vars: 0, input, output
73
790ms, O(1), #vars: 0, input, output
66
167ms, O(1), #vars: 0, input, output
79
222ms, O(1), #vars: 0, input, aspic, output
T2/bf9
1
333ms, Ω(1), #vars: 0, input, output
589
3103ms, O(1), #vars: 0, input, output
79
1041ms, O(1), #vars: 0, input, output
73
141ms, O(1), #vars: 0, input, output
85
325ms, O(1), #vars: 0, input, aspic, output
T2/bio
1
31531ms, Ω(1), #vars: 0, input, output

60013ms, input

60001ms, input

2029ms, input, output

69ms, input, aspic, aspic (errors)
T2/bitcount16
1
104ms, Ω(1), #vars: 0, input, output
34
141ms, O(1), #vars: 0, input, output
18
318ms, O(1), #vars: 0, input, output
48
53ms, O(1), #vars: 0, input, output
20
121ms, O(1), #vars: 0, input, aspic, output
T2/bitcount32
1
116ms, Ω(1), #vars: 0, input, output
66
133ms, O(1), #vars: 0, input, output
34
308ms, O(1), #vars: 0, input, output
96
58ms, O(1), #vars: 0, input, output
36
117ms, O(1), #vars: 0, input, aspic, output
T2/broydn
2 - B + A
1450ms, Ω(n), #vars: 2, input, output

11682ms, input, output

60001ms, input, output

336ms, input, output

4711ms, input, aspic
T2/broydn.c.i.broydn.pl.t2.fixed
nonlinear
2 - B + A
1998ms, Ω(n), #vars: 2, input, output

14084ms, input, output

60001ms, input, output

372ms, input, output
Non-linear example not handled by prover.
T2/broydn.c.i.broydn.pl.t2.nor.t2.rlgfixed
2 - B + A
1418ms, Ω(n), #vars: 2, input, output

11672ms, input, output

60012ms, input, output

388ms, input, output

5172ms, input, aspic
T2/brp
1
11112ms, Ω(1), #vars: 0, input, output

60013ms, input

60001ms, input, output

1168ms, input, output

60003ms, input, aspic
T2/brp_withassume
1
12079ms, Ω(1), #vars: 0, input, output

60013ms, input

60001ms, input, output

1317ms, input, output

30996ms, input, aspic, aspic (errors)
T2/bs
1
153ms, Ω(1), #vars: 0, input, output

2036ms, input, output

393ms, input, output

226ms, input, output

140ms, input, aspic, output, errors
T2/bsort100
1
218ms, Ω(1), #vars: 0, input, output
1413880
413ms, O(1), #vars: 0, input, output
10201
2741ms, O(1), #vars: 0, input, output
29899
127ms, O(1), #vars: 0, input, output

212ms, input, aspic, output, errors
T2/bubbleSort
1 / 2 - 1 / 2 * (-1 + ...
245ms, Ω(n2), #vars: 1, input, output
422 * C + 20 * C^2 + 591
396ms, O(n2), #vars: 1, input, output
max(5, (C + 1) * (C + ...
546ms, O(n2), #vars: 1, input, output
max(C, 0) + max(0, C +...
81ms, O(n2), #vars: 1, input, output

134ms, input, aspic, output, errors
T2/bubblesort_inner_loop
1
111ms, Ω(1), #vars: 0, input, output
11
227ms, O(1), #vars: 0, input, output
6
210ms, O(1), #vars: 0, input, output
4
48ms, O(1), #vars: 0, input, output
8
84ms, O(1), #vars: 0, input, aspic, output
T2/buggyNonTermLoop
INF
10520ms, INF, #vars: 1, input, output

2903ms, input, output

60008ms, input, output

226ms, input, output

798ms, input, aspic, output
T2/byron-1
1
61ms, Ω(1), #vars: 0, input, output
A + 3
253ms, O(n), #vars: 1, input, output
max(A + 2, 2)
186ms, O(n), #vars: 1, input, output

43ms, input, output

90ms, input, aspic
T2/byron-2
-1 + C
645ms, Ω(n), #vars: 1, input, output

347ms, input, output

239ms, input, output

104ms, input, output

133ms, input, aspic, output, errors
T2/byron-3
1
58ms, Ω(1), #vars: 0, input, output

2780ms, input, output

182ms, input, output

68ms, input, output

75ms, input, aspic
T2/byron-4
1 + 2 * meter
213ms, Ω(n), #vars: 1, input, output
2 * A + 3
280ms, O(n), #vars: 1, input, output
max(A + 2, 4)
221ms, O(n), #vars: 1, input, output

208ms, input, output

76ms, input, aspic, output, errors
T2/cfg
INF
65ms, INF, #vars: 1, input, output

1495ms, input, output

190ms, input, output

49ms, input, output

82ms, input, aspic, output, errors
T2/cnt
1
248ms, Ω(1), #vars: 0, input, output
1773
411ms, O(1), #vars: 0, input, output
243
1396ms, O(1), #vars: 0, input, output
450
87ms, O(1), #vars: 0, input, output

431ms, input, aspic
T2/collatz
1
1784ms, Ω(1), #vars: 0, input, output

2321ms, input, output

218ms, input, output

10722ms, input, output

105ms, input, aspic
T2/complex_guard
7
61ms, Ω(1), #vars: 0, input, output
25
130ms, O(1), #vars: 0, input, output
10
235ms, O(1), #vars: 0, input, output
3
80ms, O(1), #vars: 0, input, output
12
86ms, O(1), #vars: 0, input, aspic, output
T2/constants
1
84ms, Ω(1), #vars: 0, input, output
404
126ms, O(1), #vars: 0, input, output
402
252ms, O(1), #vars: 0, input, output
400
72ms, O(1), #vars: 0, input, output

98ms, input, aspic, output
T2/consts1
1
61ms, Ω(1), #vars: 0, input, output
301
87ms, O(1), #vars: 0, input, output
200
164ms, O(1), #vars: 0, input, output

67ms, input, output
202
79ms, O(1), #vars: 0, input, aspic, output
T2/consts1nt
INF
70ms, INF, #vars: 1, input, output

594ms, input, output

170ms, input, output

81ms, input, output

71ms, input, aspic, output, errors
T2/consts2
1 + meter
61ms, Ω(n), #vars: 1, input, output
A + 1000
87ms, O(n), #vars: 1, input, output
max(1 / 1000 * A, 1)
164ms, O(n), #vars: 1, input, output
max(0, A + -1000)
71ms, O(n), #vars: 1, input, output

75ms, input, aspic, output, errors
T2/consts2nt
INF
60ms, INF, #vars: 1, input, output

1354ms, input, output

163ms, input, output

61ms, input, output

80ms, input, aspic, output, errors
T2/consts3
-200 + A
64ms, Ω(n), #vars: 1, input, output
A + 1
77ms, O(n), #vars: 1, input, output
max(A + -200, 1)
218ms, O(n), #vars: 1, input, output
max(0, A + -201)
47ms, O(n), #vars: 1, input, output

97ms, input, aspic, output, errors
T2/consts3nt
INF
52ms, INF, #vars: 1, input, output

784ms, input, output

166ms, input, output

42ms, input, output

83ms, input, aspic, output, errors
T2/consts4
1 + meter
57ms, Ω(n), #vars: 1, input, output
A + 1200
81ms, O(n), #vars: 1, input, output
max(1 / 1000 * A + -1 ...
161ms, O(n), #vars: 1, input, output
max(0, A + -1200)
42ms, O(n), #vars: 1, input, output

71ms, input, aspic, output, errors
T2/consts4nt
INF
57ms, INF, #vars: 1, input, output

1294ms, input, output

162ms, input, output

54ms, input, output

78ms, input, aspic, output, errors
T2/consts5
1
79ms, Ω(1), #vars: 0, input, output
1
28ms, O(1), #vars: 0, input, output
1
172ms, O(1), #vars: 0, input, output

46ms, input
3
81ms, O(1), #vars: 0, input, aspic, output
T2/consts5nt
INF
74ms, INF, #vars: 1, input, output

1404ms, input, output

218ms, input, output

52ms, input, output

86ms, input, aspic, output, errors
T2/cover
1
800ms, Ω(1), #vars: 0, input, output

60012ms, input

60001ms, input, output

762ms, input, output

60003ms, input, aspic, output
T2/crc
1
606ms, Ω(1), #vars: 0, input, output
1008 * L + 346135
2678ms, O(n), #vars: 1, input, output
2649
6922ms, O(1), #vars: 0, input, output
4194
292ms, O(1), #vars: 0, input, output

2266ms, input, aspic, output
T2/create
-1 + free_26
119ms, INF, #vars: 1, input, output

873ms, input, output

312ms, input, output

63ms, input, output

511ms, input, aspic
T2/create_seg
-1 + free_26
88ms, INF, #vars: 1, input, output

884ms, input, output

352ms, input, output

67ms, input, output

668ms, input, aspic
T2/create_via_tmps
1 + U + A
2014ms, Ω(n), #vars: 2, input, output
4 * U + A + 15
893ms, O(n), #vars: 2, input, output
max(A + -1, 1)
1604ms, O(n), #vars: 1, input, output

231ms, input, output

2677ms, input, aspic
T2/ctl
INF
74ms, INF, #vars: 1, input, output

271ms, input, output

369ms, input, output

48ms, input, output

132ms, input, aspic, output, errors
T2/curious
INF
52ms, INF, #vars: 1, input, output

126ms, input, output

167ms, input, output

40ms, input, output

78ms, input, aspic, output, errors
T2/curious4
INF
3687ms, INF, #vars: 1, input, output

60013ms, input

11500ms, input, output, errors

772ms, input, output

85ms, input, aspic, aspic (errors)
T2/d
1
96ms, Ω(1), #vars: 0, input, output

1227ms, input, output

222ms, input, output

53ms, input, output

117ms, input, aspic
T2/db2
34 + free_1
23118ms, INF, #vars: 1, input, output

60015ms, input

60001ms, input

4030ms, input, output

60ms, input, aspic, aspic (errors)
T2/db3
34 + free_1
25052ms, INF, #vars: 1, input, output

60022ms, input

60001ms, input

3839ms, input, output

80ms, input, aspic, aspic (errors)
T2/dead.neg-st88b-succeed
INF
425ms, INF, #vars: 1, input, output

1886ms, input, output

310ms, input, output

162ms, input, output

105ms, input, aspic, output, errors
T2/destroy
1 + R + free_74
2274ms, INF, #vars: 2, input, output

1516ms, input, output

1607ms, input, output

203ms, input, output

5834ms, input, aspic
T2/destroy_seg
1 + free_75 + T
2594ms, INF, #vars: 2, input, output

1421ms, input, output

2538ms, input, output

185ms, input, output

8552ms, input, aspic
T2/destroy_seg_leak

60016ms, input, output

60014ms, input

35180ms, input, output

26547ms, input, output, errors

155ms, input, aspic, aspic (errors)
T2/disj_nightmare_abi
1
109ms, Ω(1), #vars: 0, input, output
3
53ms, O(1), #vars: 0, input, output
2
173ms, O(1), #vars: 0, input, output
1
103ms, O(1), #vars: 0, input, output

80ms, input, aspic, output, errors
T2/dropbuf
INF
1200ms, INF, #vars: 1, input, output

1877ms, input, output

5141ms, input, output

434ms, input, output

1234ms, input, aspic, output
T2/dropbuf-live
1
17ms, Ω(1), #vars: 0, input, output
1
26ms, O(1), #vars: 0, input, output
1
144ms, O(1), #vars: 0, input, output

41ms, input
3
97ms, O(1), #vars: 0, input, aspic, output
T2/dsa_test
1
16ms, Ω(1), #vars: 0, input, output
1
18ms, O(1), #vars: 0, input, output
1
195ms, O(1), #vars: 0, input, output

44ms, input
3
82ms, O(1), #vars: 0, input, aspic, output
T2/dsa_test1
1
16ms, Ω(1), #vars: 0, input, output
1
22ms, O(1), #vars: 0, input, output
1
143ms, O(1), #vars: 0, input, output

35ms, input
3
81ms, O(1), #vars: 0, input, aspic, output
T2/dsa_test10
22
81ms, Ω(1), #vars: 0, input, output
31
211ms, O(1), #vars: 0, input, output
23
244ms, O(1), #vars: 0, input, output
20
66ms, O(1), #vars: 0, input, output
25
106ms, O(1), #vars: 0, input, aspic, output
T2/dsa_test11
1
18ms, Ω(1), #vars: 0, input, output
1
17ms, O(1), #vars: 0, input, output
1
185ms, O(1), #vars: 0, input, output

66ms, input
3
90ms, O(1), #vars: 0, input, aspic, output
T2/dsa_test12
1
18ms, Ω(1), #vars: 0, input, output
1
18ms, O(1), #vars: 0, input, output
1
143ms, O(1), #vars: 0, input, output

49ms, input
3
76ms, O(1), #vars: 0, input, aspic, output
T2/dsa_test13
1
17ms, Ω(1), #vars: 0, input, output
1
16ms, O(1), #vars: 0, input, output
1
144ms, O(1), #vars: 0, input, output

53ms, input
3
83ms, O(1), #vars: 0, input, aspic, output
T2/dsa_test15
22
79ms, Ω(1), #vars: 0, input, output
23
171ms, O(1), #vars: 0, input, output
23
217ms, O(1), #vars: 0, input, output
20
64ms, O(1), #vars: 0, input, output
25
82ms, O(1), #vars: 0, input, aspic, output
T2/dsa_test4
1
17ms, Ω(1), #vars: 0, input, output
1
18ms, O(1), #vars: 0, input, output
1
143ms, O(1), #vars: 0, input, output

66ms, input
3
76ms, O(1), #vars: 0, input, aspic, output
T2/dsa_test5
1
17ms, Ω(1), #vars: 0, input, output
1
20ms, O(1), #vars: 0, input, output
1
145ms, O(1), #vars: 0, input, output

102ms, input
3
74ms, O(1), #vars: 0, input, aspic, output
T2/dsa_test6
11
56ms, Ω(1), #vars: 0, input, output
12
82ms, O(1), #vars: 0, input, output
12
169ms, O(1), #vars: 0, input, output
10
47ms, O(1), #vars: 0, input, output
14
77ms, O(1), #vars: 0, input, aspic, output
T2/dsa_test8
1
23ms, Ω(1), #vars: 0, input, output
1
19ms, O(1), #vars: 0, input, output
1
144ms, O(1), #vars: 0, input, output

52ms, input
3
79ms, O(1), #vars: 0, input, aspic, output
T2/dsa_test9
1
17ms, Ω(1), #vars: 0, input, output
1
20ms, O(1), #vars: 0, input, output
1
148ms, O(1), #vars: 0, input, output

36ms, input
3
103ms, O(1), #vars: 0, input, aspic, output
T2/dummy
INF
81ms, INF, #vars: 1, input, output

2515ms, input, output

187ms, input, output

44ms, input, output

68ms, input, aspic
T2/e-1394complete-succeed
INF
1661ms, INF, #vars: 1, input, output

5135ms, input, output

50045ms, input, output

353ms, input, output

57ms, input, aspic, aspic (errors)
T2/e-acqrel-fail
INF
93ms, INF, #vars: 1, input, output

652ms, input, output

248ms, input, output

54ms, input, output

94ms, input, aspic, output, errors
T2/e-acqrel-succeed
INF
80ms, INF, #vars: 1, input, output

803ms, input, output

485ms, input, output

61ms, input, output

97ms, input, aspic, output, errors
T2/e-pgarch-fail
INF
174ms, INF, #vars: 1, input, output

368ms, input, output

550ms, input, output

48ms, input, output

233ms, input, aspic, output, errors
T2/e-pgarch-succeed
INF
169ms, INF, #vars: 1, input, output

397ms, input, output

785ms, input, output

59ms, input, output

282ms, input, aspic, output, errors
T2/e-popl07-fail
INF
268ms, INF, #vars: 1, input, output

975ms, input, output

3041ms, input, output

562ms, input, output

693ms, input, aspic, output
T2/edn
1
363ms, Ω(1), #vars: 0, input, output
1291579
2353ms, O(1), #vars: 0, input, output
27161 / 7
10535ms, O(1), #vars: 0, input, output
6297
210ms, O(1), #vars: 0, input, output

6398ms, input, aspic, output
T2/efegp
3 - 2 * free_2
1632ms, INF, #vars: 1, input, output

31773ms, input, output

4258ms, input, output, errors

677ms, input, output

62ms, input, aspic, aspic (errors)
T2/elmhes
3 - E + A
876ms, Ω(n), #vars: 2, input, output
13577382562501012 * A ...
1500ms, O(n2), #vars: 3, input, output

6294ms, input, output

464ms, input, output

782ms, input, aspic, output, errors
T2/elmhes.c.i.elmhes.pl.t2.fixed
nonlinear
3 - E + A
1525ms, Ω(n), #vars: 2, input, output
2318416846246180 * A +...
1515ms, O(n2), #vars: 3, input, output

7053ms, input, output

475ms, input, output
Non-linear example not handled by prover.
T2/elmhes.c.i.elmhes.pl.t2.nor.t2.rlgfixed
3 - E + A
894ms, Ω(n), #vars: 2, input, output
2318416846246180 * A +...
1488ms, O(n2), #vars: 3, input, output

6583ms, input, output

403ms, input, output

754ms, input, aspic, output, errors
T2/eric
1 - 2 * B + 2 * A
561ms, Ω(n), #vars: 2, input, output

1496ms, input, output
max(2 * A + -2 * B + 3...
470ms, O(n), #vars: 2, input, output

80ms, input, output

83ms, input, aspic, output, errors
T2/eric1
1 + 2 * B
151ms, Ω(n), #vars: 1, input, output

8490ms, input, output
max(2, max(0, min(B + ...
354ms, O(n2), #vars: 1, input, output

109ms, input, output
max(3 / 2 * B__o' + 1 ...
87ms, O(n2), #vars: 1, input, aspic, output
T2/eric2
3 + H
4545ms, Ω(n), #vars: 1, input, output

60018ms, input

5820ms, input, output

251ms, input, output

846ms, input, aspic, output
T2/eric3
INF
117ms, INF, #vars: 1, input, output

1322ms, input, output

205ms, input, output

252ms, input, output

91ms, input, aspic, output, errors
T2/ex1
INF
27ms, INF, #vars: 1, input, output

736ms, input, output

184ms, input, output

38ms, input, output

93ms, input, aspic, output, errors
T2/ex10
INF
85ms, INF, #vars: 1, input, output

819ms, input, output

373ms, input, output

87ms, input, output

158ms, input, aspic, output, errors
T2/ex11
1
5783ms, Ω(1), #vars: 0, input, output

2029ms, input, output

241ms, input, output

168ms, input, output

76ms, input, aspic, output, errors
T2/ex12
1
65ms, Ω(1), #vars: 0, input, output
20
137ms, O(1), #vars: 0, input, output
11
201ms, O(1), #vars: 0, input, output
18
42ms, O(1), #vars: 0, input, output
23
106ms, O(1), #vars: 0, input, aspic, output
T2/ex13
1
16ms, Ω(1), #vars: 0, input, output
1
18ms, O(1), #vars: 0, input, output
1
202ms, O(1), #vars: 0, input, output

48ms, input
3
81ms, O(1), #vars: 0, input, aspic, output
T2/ex14
11
58ms, Ω(1), #vars: 0, input, output
12
128ms, O(1), #vars: 0, input, output
12
178ms, O(1), #vars: 0, input, output
10
46ms, O(1), #vars: 0, input, output
14
78ms, O(1), #vars: 0, input, aspic, output
T2/ex15
1
17ms, Ω(1), #vars: 0, input, output
1
26ms, O(1), #vars: 0, input, output
1
146ms, O(1), #vars: 0, input, output

34ms, input
3
107ms, O(1), #vars: 0, input, aspic, output
T2/ex16
1
153ms, Ω(1), #vars: 0, input, output

4115ms, input, output

614ms, input, output

66ms, input, output

204ms, input, aspic
T2/ex17
1
95ms, Ω(1), #vars: 0, input, output
104
247ms, O(1), #vars: 0, input, output
102
520ms, O(1), #vars: 0, input, output

70ms, input, output

133ms, input, aspic, output
T2/ex18
1
153ms, Ω(1), #vars: 0, input, output

2932ms, input, output
302
396ms, O(1), #vars: 0, input, output

195ms, input, output

162ms, input, aspic, output, errors
T2/ex19
INF
69ms, INF, #vars: 1, input, output

1738ms, input, output

293ms, input, output

55ms, input, output

63ms, input, aspic, output, errors
T2/ex2
INF
77ms, INF, #vars: 1, input, output

2256ms, input, output

216ms, input, output

112ms, input, output

83ms, input, aspic, output, errors
T2/ex20
1
71ms, Ω(1), #vars: 0, input, output
1030
174ms, O(1), #vars: 0, input, output
1026
293ms, O(1), #vars: 0, input, output
1024
86ms, O(1), #vars: 0, input, output
1028
103ms, O(1), #vars: 0, input, aspic, output
T2/ex21
202
79ms, Ω(1), #vars: 0, input, output
499
209ms, O(1), #vars: 0, input, output
203
247ms, O(1), #vars: 0, input, output
200
65ms, O(1), #vars: 0, input, output
205
88ms, O(1), #vars: 0, input, aspic, output
T2/ex22
1
361ms, Ω(1), #vars: 0, input, output
11928
4268ms, O(1), #vars: 0, input, output
390
3481ms, O(1), #vars: 0, input, output
370
190ms, O(1), #vars: 0, input, output

1570ms, input, aspic, output
T2/ex23
37
66ms, Ω(1), #vars: 0, input, output
39
115ms, O(1), #vars: 0, input, output
38
247ms, O(1), #vars: 0, input, output
36
56ms, O(1), #vars: 0, input, output
max(40, 3)
96ms, O(1), #vars: 0, input, aspic, output
T2/ex26
202
78ms, Ω(1), #vars: 0, input, output
499
219ms, O(1), #vars: 0, input, output
203
327ms, O(1), #vars: 0, input, output
200
58ms, O(1), #vars: 0, input, output
205
99ms, O(1), #vars: 0, input, aspic, output
T2/ex27
1
479ms, Ω(1), #vars: 0, input, output
22853
10128ms, O(1), #vars: 0, input, output
595
10627ms, O(1), #vars: 0, input, output
570
400ms, O(1), #vars: 0, input, output

4101ms, input, aspic, output
T2/ex29
1
31ms, Ω(1), #vars: 0, input, output
15
131ms, O(1), #vars: 0, input, output
4
234ms, O(1), #vars: 0, input, output

50ms, input

255ms, input, aspic, output
T2/ex3
11
68ms, Ω(1), #vars: 0, input, output
13
86ms, O(1), #vars: 0, input, output
23 / 2
188ms, O(1), #vars: 0, input, output
10
48ms, O(1), #vars: 0, input, output
25
82ms, O(1), #vars: 0, input, aspic, output
T2/ex30
2 + free + free_2
76ms, INF, #vars: 2, input, output

2348ms, input, output

402ms, input, output

61ms, input, output

121ms, input, aspic, output, errors
T2/ex31
1
95ms, Ω(1), #vars: 0, input, output

1099ms, input, output

257ms, input, output

72ms, input, output

88ms, input, aspic, output, errors
T2/ex32
2002
76ms, Ω(1), #vars: 0, input, output
2003
226ms, O(1), #vars: 0, input, output
2003
234ms, O(1), #vars: 0, input, output
2000
61ms, O(1), #vars: 0, input, output

95ms, input, aspic, output
T2/ex33
1
50ms, Ω(1), #vars: 0, input, output
3
66ms, O(1), #vars: 0, input, output
1
155ms, O(1), #vars: 0, input, output

36ms, input
3
86ms, O(1), #vars: 0, input, aspic, output
T2/ex34
1
19ms, Ω(1), #vars: 0, input, output
1
13ms, O(1), #vars: 0, input, output
1
169ms, O(1), #vars: 0, input, output

48ms, input

65ms, input, aspic, aspic (errors)
T2/ex36
12 + free_82 + free_64...
14866ms, INF, #vars: 5, input, output

60018ms, input

60001ms, input, output

1088ms, input, output

69ms, input, aspic, aspic (errors)
T2/ex37
1
16ms, Ω(1), #vars: 0, input, output
1
14ms, O(1), #vars: 0, input, output
1
197ms, O(1), #vars: 0, input, output

49ms, input
3
78ms, O(1), #vars: 0, input, aspic, output
T2/ex4
1
228ms, Ω(1), #vars: 0, input, output
87
325ms, O(1), #vars: 0, input, output
34
516ms, O(1), #vars: 0, input, output
20
95ms, O(1), #vars: 0, input, output
36
146ms, O(1), #vars: 0, input, aspic, output
T2/ex40
INF
33ms, INF, #vars: 1, input, output

1438ms, input, output

200ms, input, output

50ms, input, output

83ms, input, aspic, output, errors
T2/ex6
1
48ms, Ω(1), #vars: 0, input, output
3
19ms, O(1), #vars: 0, input, output
1
147ms, O(1), #vars: 0, input, output

35ms, input
3
82ms, O(1), #vars: 0, input, aspic, output
T2/ex7
11
56ms, Ω(1), #vars: 0, input, output
12
92ms, O(1), #vars: 0, input, output
12
197ms, O(1), #vars: 0, input, output
10
48ms, O(1), #vars: 0, input, output
14
83ms, O(1), #vars: 0, input, aspic, output
T2/ex8
INF
77ms, INF, #vars: 1, input, output

2835ms, input, output

417ms, input, output

78ms, input, output

82ms, input, aspic, aspic (errors)
T2/ex9
INF
88ms, INF, #vars: 1, input, output

2693ms, input, output

586ms, input, output

88ms, input, output

78ms, input, aspic, aspic (errors)
T2/example
A
189ms, Ω(n), #vars: 1, input, output
2 * A + 2 * B + 5
138ms, O(n), #vars: 2, input, output
max(A + B + -1, 1)
246ms, O(n), #vars: 2, input, output
max(0, B + -1) + max(0...
80ms, O(n), #vars: 1, input, output
max(2, 2, 1 + -1 + B__...
102ms, O(n), #vars: 2, input, aspic, output
T2/fake-succeed
INF
7722ms, INF, #vars: 1, input, output

60015ms, input

60001ms, input, output

486ms, input, output

61ms, input, aspic, aspic (errors)
T2/fast_poll
INF
2204ms, INF, #vars: 1, input, output

10432ms, input, output

60001ms, input, output

185ms, input, output

5872ms, input, aspic, output
T2/fdct
18
81ms, Ω(1), #vars: 0, input, output
31
171ms, O(1), #vars: 0, input, output
19
707ms, O(1), #vars: 0, input, output
16
70ms, O(1), #vars: 0, input, output
21
924ms, O(1), #vars: 0, input, aspic, output
T2/fermat
12
103ms, Ω(1), #vars: 0, input, output
17
297ms, O(1), #vars: 0, input, output
13
857ms, O(1), #vars: 0, input, output
9
122ms, O(1), #vars: 0, input, output
15
349ms, O(1), #vars: 0, input, aspic, output
T2/fibcall
1
60ms, Ω(1), #vars: 0, input, output
31
191ms, O(1), #vars: 0, input, output
31
247ms, O(1), #vars: 0, input, output
29
43ms, O(1), #vars: 0, input, output

87ms, input, aspic
T2/fir
21 + 10 * free
866ms, INF, #vars: 1, input, output

3774ms, input, output

1452ms, input, output

125ms, input, output

233ms, input, aspic, output, errors
T2/firewire
1
1823ms, Ω(1), #vars: 0, input, output

4162ms, input, output

4089ms, input, output

388ms, input, output

561ms, input, aspic, output, errors
T2/flipflop
INF
72ms, INF, #vars: 1, input, output

1030ms, input, output

211ms, input, output

49ms, input, output

76ms, input, aspic, output, errors
T2/fourn
8 + 2 * meter - B + A
7661ms, Ω(n), #vars: 3, input, output

22123ms, input, output

60001ms, input, output

565ms, input, output

2604ms, input, aspic
T2/fourn.c.i.fourn.pl.t2.fixed
nonlinear
3 - B + A
40190ms, Ω(n), #vars: 2, input, output
A + B + 4
436ms, O(n), #vars: 2, input, output

60001ms, input, output

1526ms, input, output
Non-linear example not handled by prover.
T2/fourn.c.i.fourn.pl.t2.nor.t2.rlgfixed
8 + 2 * meter - B + A
7287ms, Ω(n), #vars: 3, input, output

21568ms, input, output

60001ms, input, output

647ms, input, output

3151ms, input, aspic
T2/fuhs-inflasso
-1 / 2 + 1 / 2 * (-1 +...
231ms, Ω(n2), #vars: 1, input, output
C^2 + 5 * C + 7
122ms, O(n2), #vars: 1, input, output
max(1, max(0, min(C + ...
351ms, O(n2), #vars: 1, input, output
max(0, C + -1) + max(0...
71ms, O(n2), #vars: 1, input, output

82ms, input, aspic
T2/fun1
INF
9709ms, INF, #vars: 1, input, output

2943ms, input, output

60001ms, input, output

239ms, input, output

623ms, input, aspic, output
T2/fun10
INF
3387ms, INF, #vars: 1, input, output

60017ms, input

60001ms, input, output

334ms, input, output

61ms, input, aspic, aspic (errors)
T2/fun10b
INF
3236ms, INF, #vars: 1, input, output

60016ms, input

60001ms, input, output

287ms, input, output

73ms, input, aspic, aspic (errors)
T2/fun11
INF
133ms, INF, #vars: 1, input, output

1343ms, input, output

257ms, input, output

47ms, input, output

113ms, input, aspic, output, errors
T2/fun1b
INF
10131ms, INF, #vars: 1, input, output

3303ms, input, output

60001ms, input, output

241ms, input, output

757ms, input, aspic, output
T2/fun2
1
11986ms, Ω(1), #vars: 0, input, output
111 * C + 111 * E + 11...
1448ms, O(n), #vars: 4, input, output

60001ms, input, output

209ms, input, output

801ms, input, aspic, output
T2/fun2b
1
10013ms, Ω(1), #vars: 0, input, output

2857ms, input, output

60001ms, input, output

222ms, input, output

968ms, input, aspic, output
T2/fun3
1
10929ms, Ω(1), #vars: 0, input, output
111 * C + 111 * E + 11...
1554ms, O(n), #vars: 4, input, output

60001ms, input, output

214ms, input, output

766ms, input, aspic, output
T2/fun4
2
245ms, Ω(1), #vars: 0, input, output
24
351ms, O(1), #vars: 0, input, output
max(1 / 2 * A + -1 * B...
304ms, O(n), #vars: 2, input, output

100ms, input, output

97ms, input, aspic, output, errors
T2/fun4-alt
2
178ms, Ω(1), #vars: 0, input, output
24
203ms, O(1), #vars: 0, input, output
max(1 / 2 * A + -1 * B...
254ms, O(n), #vars: 2, input, output

95ms, input, output

101ms, input, aspic, output, errors
T2/fun5
1
1098ms, Ω(1), #vars: 0, input, output

13901ms, input, output

46627ms, input, output

979ms, input, output

60001ms, input, aspic
T2/fun6
4 + free
369ms, INF, #vars: 1, input, output

19559ms, input, output

262ms, input, output, errors

85ms, input, output

7937ms, input, aspic, output
T2/fun7
1
1065ms, Ω(1), #vars: 0, input, output

762ms, input, output

3221ms, input, output

309ms, input, output

3645ms, input, aspic, output
T2/fun8
1
2390ms, Ω(1), #vars: 0, input, output
1068
1970ms, O(1), #vars: 0, input, output
32
3571ms, O(1), #vars: 0, input, output

247ms, input, output

3557ms, input, aspic
T2/fun9
1
5493ms, Ω(1), #vars: 0, input, output

6356ms, input, output

60006ms, input, output

273ms, input, output

1583ms, input, aspic, output, errors
T2/graycode
1
276ms, Ω(1), #vars: 0, input, output
583643
9159ms, O(1), #vars: 0, input, output

60005ms, input, output
178
743ms, O(1), #vars: 0, input, output

676ms, input, aspic, output
T2/heidy1
INF
32ms, INF, #vars: 1, input, output

638ms, input, output

180ms, input, output

40ms, input, output

68ms, input, aspic, output, errors
T2/heidy10
1 + free
175ms, INF, #vars: 1, input, output

2609ms, input, output

249ms, input, output

68ms, input, output

182ms, input, aspic, output, errors
T2/heidy2
INF
56ms, INF, #vars: 1, input, output

1142ms, input, output

174ms, input, output

48ms, input, output

107ms, input, aspic, output, errors
T2/heidy3
INF
76ms, INF, #vars: 1, input, output

354ms, input, output

252ms, input, output

52ms, input, output

75ms, input, aspic, output, errors
T2/heidy5
1 + B
62ms, Ω(n), #vars: 1, input, output
B + 3
104ms, O(n), #vars: 1, input, output
max(B + 2, 2)
180ms, O(n), #vars: 1, input, output
max(B, 0)
77ms, O(n), #vars: 1, input, output

73ms, input, aspic, output, errors
T2/heidy6
INF
77ms, INF, #vars: 1, input, output

528ms, input, output

279ms, input, output

83ms, input, output

87ms, input, aspic, output, errors
T2/heidy7
1 + B
192ms, Ω(n), #vars: 1, input, output

2406ms, input, output

262ms, input, output

111ms, input, output

103ms, input, aspic, output, errors
T2/heidy7-simple
INF
66ms, INF, #vars: 1, input, output

1227ms, input, output

251ms, input, output

55ms, input, output

82ms, input, aspic, output, errors
T2/heidy8
1 + C
194ms, Ω(n), #vars: 1, input, output

4632ms, input, output

358ms, input, output

85ms, input, output

96ms, input, aspic, output, errors
T2/heidy9
1 + A
61ms, Ω(n), #vars: 1, input, output
A + 2
101ms, O(n), #vars: 1, input, output
max(A + 2, 2)
170ms, O(n), #vars: 1, input, output
max(A, 0)
57ms, O(n), #vars: 1, input, output

88ms, input, aspic, output, errors
T2/hongyi1
3 + 2 * C
9809ms, Ω(n), #vars: 1, input, output
188 * C + 627 * D + 23...
23166ms, O(n), #vars: 3, input, output

60001ms, input, output

1282ms, input, output

30706ms, input, aspic, aspic (errors)
T2/hqr
5 + 2 * B - Q
30737ms, Ω(n), #vars: 2, input, output

60012ms, input

60001ms, input, output

362ms, input, output

72ms, input, aspic, aspic (errors)
T2/hqr.c.i.hqr.pl.t2.fixed
nonlinear
6 - Q
52954ms, Ω(n), #vars: 1, input, output

60013ms, input

60001ms, input, output

694ms, input, output
Non-linear example not handled by prover.
T2/hqr.c.i.hqr.pl.t2.nor.t2.rlgfixed
5 + 2 * B - Q
27704ms, Ω(n), #vars: 2, input, output

60013ms, input

60001ms, input, output

413ms, input, output

74ms, input, aspic, aspic (errors)
T2/huh
32 + free_24
206ms, INF, #vars: 1, input, output

3908ms, input, output

738ms, input, output

56ms, input, output

695ms, input, aspic
T2/iecs
1
57ms, Ω(1), #vars: 0, input, output
B + 1
231ms, O(n), #vars: 1, input, output
max(B + 1, 1)
173ms, O(n), #vars: 1, input, output

67ms, input, output

76ms, input, aspic
T2/insertsort
INF
54ms, INF, #vars: 1, input, output

4212ms, input, output

266ms, input, output

55ms, input, output

109ms, input, aspic, output, errors
T2/intSqRoot
nonlinear
1
118ms, Ω(1), #vars: 0, input, output

1561ms, input, output

224ms, input, output

87ms, input, output
Non-linear example not handled by prover.
T2/invgen
1
75ms, Ω(1), #vars: 0, input, output
B + 2
100ms, O(n), #vars: 1, input, output
max(B + 2, 1)
200ms, O(n), #vars: 1, input, output
max(0, B + 1)
46ms, O(n), #vars: 1, input, output

63ms, input, aspic
T2/jacobi
4 - C + A
614ms, Ω(n), #vars: 2, input, output
225 * A + 218 * B + 7 ...
4389ms, O(n), #vars: 3, input, output

60001ms, input, output

928ms, input, output

2373ms, input, aspic, output
T2/jacobi.c.i.jacobi.pl.t2.fixed
nonlinear
4 - C + A
8557ms, Ω(n), #vars: 2, input, output
225 * A + 218 * B + 7 ...
5433ms, O(n), #vars: 3, input, output

60001ms, input, output

873ms, input, output
Non-linear example not handled by prover.
T2/jacobi.c.i.jacobi.pl.t2.nor.t2.rlgfixed
4 - C + A
637ms, Ω(n), #vars: 2, input, output
225 * A + 218 * B + 7 ...
4391ms, O(n), #vars: 3, input, output

60001ms, input, output

924ms, input, output

2027ms, input, aspic, output
T2/janne_complex
1
1132ms, Ω(1), #vars: 0, input, output

1550ms, input, output

581ms, input, output

465ms, input, output

106ms, input, aspic, output, errors
T2/jfdctint
83
104ms, Ω(1), #vars: 0, input, output
94
282ms, O(1), #vars: 0, input, output
84
827ms, O(1), #vars: 0, input, output
80
109ms, O(1), #vars: 0, input, output
86
1119ms, O(1), #vars: 0, input, aspic, output
T2/loop3
1
2671ms, Ω(1), #vars: 0, input, output
1873991
47348ms, O(1), #vars: 0, input, output

53078ms, input, output

494ms, input, output

999ms, input, aspic
T2/loop_on_input
1
124ms, Ω(1), #vars: 0, input, output
10
308ms, O(1), #vars: 0, input, output
6
178ms, O(1), #vars: 0, input, output

54ms, input, output

54ms, input, aspic
T2/ludcmp
3 - D + A
4625ms, Ω(n), #vars: 2, input, output
932 * A + 926 * D + 4 ...
2544ms, O(n), #vars: 4, input, output

60004ms, input, output
max(0, max(0, max(0, A...
691ms, O(n4), #vars: 2, input, output

403ms, input, aspic, output
T2/ludcmp.c.i.ludcmp.pl.t2.fixed
nonlinear
3 - D + A
4613ms, Ω(n), #vars: 2, input, output
602 * A + 596 * D + 4 ...
2619ms, O(n), #vars: 4, input, output

60002ms, input, output
max(0, max(0, max(0, A...
736ms, O(n4), #vars: 2, input, output
Non-linear example not handled by prover.
T2/ludcmp.c.i.ludcmp.pl.t2.nor.t2.rlgfixed
3 - D + A
4418ms, Ω(n), #vars: 2, input, output
568 * A + 562 * D + 4 ...
2793ms, O(n), #vars: 4, input, output

60004ms, input, output
max(0, max(0, max(0, A...
693ms, O(n4), #vars: 2, input, output

436ms, input, aspic, output
T2/magic
2 + free_2
581ms, INF, #vars: 1, input, output

60013ms, input

60001ms, input, output

372ms, input, output

9946ms, input, aspic
T2/matmul
222
136ms, Ω(1), #vars: 0, input, output
6567
388ms, O(1), #vars: 0, input, output
223
338ms, O(1), #vars: 0, input, output
190
83ms, O(1), #vars: 0, input, output

91ms, input, aspic, output, errors
T2/matmult
9723
178ms, Ω(1), #vars: 0, input, output
163873
790ms, O(1), #vars: 0, input, output
9724
829ms, O(1), #vars: 0, input, output
9280
140ms, O(1), #vars: 0, input, output

298ms, input, aspic, output, errors
T2/matrixsqrt
30
177ms, Ω(1), #vars: 0, input, output
524
2996ms, O(1), #vars: 0, input, output
31
913ms, O(1), #vars: 0, input, output
22
88ms, O(1), #vars: 0, input, output

275ms, input, aspic, output, errors
T2/mc91
1 + meter
308ms, INF, #vars: 1, input, output

1870ms, input, output

230ms, input, output

93ms, input, output

83ms, input, aspic, output, errors
T2/mc91test
1 + meter
699ms, INF, #vars: 1, input, output

3935ms, input, output

281ms, input, output

336ms, input, output

117ms, input, aspic, output, errors
T2/minmax
1
19ms, Ω(1), #vars: 0, input, output
5
44ms, O(1), #vars: 0, input, output
3
188ms, O(1), #vars: 0, input, output

36ms, input
5
139ms, O(1), #vars: 0, input, aspic, output
T2/n-1
INF
58ms, INF, #vars: 1, input, output

1408ms, input, output

244ms, input, output

45ms, input, output

144ms, input, aspic, output, errors
T2/n-10
INF
104ms, INF, #vars: 1, input, output

158ms, input, output

349ms, input, output

56ms, input, output

225ms, input, aspic, output, errors
T2/n-12
INF
160ms, INF, #vars: 1, input, output

278ms, input, output

224ms, input, output

90ms, input, output

89ms, input, aspic, output, errors
T2/n-12a
INF
53ms, INF, #vars: 1, input, output

128ms, input, output

169ms, input, output

39ms, input, output

82ms, input, aspic, output, errors
T2/n-13
INF
57ms, INF, #vars: 1, input, output

935ms, input, output

173ms, input, output

40ms, input, output

83ms, input, aspic, output, errors
T2/n-14
INF
159ms, INF, #vars: 1, input, output

281ms, input, output

224ms, input, output

290ms, input, output

119ms, input, aspic, output, errors
T2/n-15
INF
76ms, INF, #vars: 1, input, output

895ms, input, output

212ms, input, output

50ms, input, output

54ms, input, aspic, output, errors
T2/n-15a
INF
400ms, INF, #vars: 1, input, output

288ms, input, output

247ms, input, output

154ms, input, output

100ms, input, aspic, output, errors
T2/n-16
INF
80ms, INF, #vars: 1, input, output

991ms, input, output

208ms, input, output

48ms, input, output

64ms, input, aspic, output, errors
T2/n-16a
1
65ms, Ω(1), #vars: 0, input, output

2428ms, input, output

228ms, input, output

56ms, input, output

83ms, input, aspic
T2/n-17
INF
73ms, INF, #vars: 1, input, output

937ms, input, output

201ms, input, output

63ms, input, output

79ms, input, aspic, output, errors
T2/n-18
INF
52ms, INF, #vars: 1, input, output

889ms, input, output

170ms, input, output

55ms, input, output

73ms, input, aspic, output, errors
T2/n-18a
1
58ms, Ω(1), #vars: 0, input, output

2472ms, input, output

191ms, input, output

63ms, input, output

133ms, input, aspic
T2/n-1c
INF
110ms, INF, #vars: 1, input, output

158ms, input, output

277ms, input, output

67ms, input, output

183ms, input, aspic, output, errors
T2/n-1d
INF
192ms, INF, #vars: 1, input, output

215ms, input, output

234ms, input, output

86ms, input, output

102ms, input, aspic, output, errors
T2/n-20
INF
73ms, INF, #vars: 1, input, output

184ms, input, output

269ms, input, output

43ms, input, output

191ms, input, aspic, output, errors
T2/n-21
INF
70ms, INF, #vars: 1, input, output

1441ms, input, output

208ms, input, output

53ms, input, output

88ms, input, aspic, output, errors
T2/n-3
INF
96ms, INF, #vars: 1, input, output

1277ms, input, output

211ms, input, output

64ms, input, output

79ms, input, aspic, output, errors
T2/n-32
1
72ms, Ω(1), #vars: 0, input, output

1143ms, input, output

171ms, input, output

50ms, input, output

83ms, input, aspic, output, errors
T2/n-33
1
307ms, Ω(1), #vars: 0, input, output

366ms, input, output

312ms, input, output

559ms, input, output

136ms, input, aspic, output, errors
T2/n-36
INF
250ms, INF, #vars: 1, input, output

349ms, input, output

1002ms, input, output

348ms, input, output

1386ms, input, aspic, output, errors
T2/n-37
INF
28ms, INF, #vars: 1, input, output

1001ms, input, output

210ms, input, output

42ms, input, output

68ms, input, aspic, output, errors
T2/n-3a
INF
540ms, INF, #vars: 1, input, output

404ms, input, output

465ms, input, output

332ms, input, output

136ms, input, aspic, output, errors
T2/n-4
1 - C + A
351ms, Ω(n), #vars: 2, input, output

6727ms, input, output

147ms, input, output, errors

39ms, input, output

212ms, input, aspic, output, errors
T2/n-40
INF
2017ms, INF, #vars: 1, input, output

2323ms, input, output

586ms, input, output

169ms, input, output

178ms, input, aspic, output, errors
T2/n-46
INF
101ms, INF, #vars: 1, input, output

2191ms, input, output

206ms, input, output

61ms, input, output

88ms, input, aspic, output, errors
T2/n-48
1
65ms, Ω(1), #vars: 0, input, output

3052ms, input, output

220ms, input, output

53ms, input, output

111ms, input, aspic
T2/n-5
1 + B - A
208ms, Ω(n), #vars: 2, input, output

2711ms, input, output

989ms, input, output

149ms, input, output

366ms, input, aspic, output, errors
T2/n-6
INF
179ms, INF, #vars: 1, input, output

236ms, input, output

233ms, input, output

141ms, input, output

89ms, input, aspic, output, errors
T2/n-6a
INF
112ms, INF, #vars: 1, input, output

281ms, input, output

224ms, input, output

55ms, input, output

91ms, input, aspic, output, errors
T2/n-7
INF
76ms, INF, #vars: 1, input, output

1537ms, input, output

193ms, input, output

151ms, input, output

81ms, input, aspic, output, errors
T2/n-8
INF
111ms, INF, #vars: 1, input, output

148ms, input, output

368ms, input, output

67ms, input, output

166ms, input, aspic, output, errors
T2/n-8a
INF
54ms, INF, #vars: 1, input, output

1005ms, input, output

196ms, input, output

50ms, input, output

83ms, input, aspic, output, errors
T2/n-9
1
119ms, Ω(1), #vars: 0, input, output

269ms, input, output

277ms, input, output

76ms, input, output

137ms, input, aspic, output, errors
T2/n_firewire_instrumented-PP
1
4091ms, Ω(1), #vars: 0, input, output

14958ms, input, output

2347ms, input, output

487ms, input, output

16895ms, input, aspic, output, errors
T2/nakata
1 + 2 * free_1
5463ms, INF, #vars: 1, input, output

23182ms, input, output

60001ms, input, output

622ms, input, output

39863ms, input, aspic, aspic (errors)
T2/nakata_withassume
1 + 2 * free_1
7463ms, INF, #vars: 1, input, output

50053ms, input, output

60001ms, input, output

228ms, input, output

60002ms, input, aspic
T2/ndes
1
9087ms, Ω(1), #vars: 0, input, output
59 * W1 + 59 * E2 + 73...
13535ms, O(n), #vars: 2, input, output

60001ms, input, output

1373ms, input, output

77ms, input, aspic, aspic (errors)
T2/neg-1394complete-fail
INF
1702ms, INF, #vars: 1, input, output

5965ms, input, output

55476ms, input, output

1110ms, input, output

67ms, input, aspic, aspic (errors)
T2/neg-1394complete-succeed
INF
1689ms, INF, #vars: 1, input, output

4954ms, input, output

59316ms, input, output

358ms, input, output

72ms, input, aspic, aspic (errors)
T2/neg-e-1394complete-fail
INF
1690ms, INF, #vars: 1, input, output

5019ms, input, output

50994ms, input, output

333ms, input, output

71ms, input, aspic, aspic (errors)
T2/neg-e-1394complete-succeed
INF
1694ms, INF, #vars: 1, input, output

4958ms, input, output

55037ms, input, output

339ms, input, output

83ms, input, aspic, aspic (errors)
T2/neg-e-acqrel-fail
INF
80ms, INF, #vars: 1, input, output

300ms, input, output

504ms, input, output

55ms, input, output

102ms, input, aspic, output, errors
T2/neg-e-acqrel-succeed
INF
83ms, INF, #vars: 1, input, output

678ms, input, output

287ms, input, output

67ms, input, output

96ms, input, aspic, output, errors
T2/neg-e-pgarch-fail
INF
168ms, INF, #vars: 1, input, output

361ms, input, output

386ms, input, output

47ms, input, output

212ms, input, aspic, output, errors
T2/neg-e-pgarch-succeed
INF
165ms, INF, #vars: 1, input, output

424ms, input, output

418ms, input, output

40ms, input, output

129ms, input, aspic, output, errors
T2/neg-e-popl07-succeed
INF
263ms, INF, #vars: 1, input, output

1026ms, input, output

2890ms, input, output

487ms, input, output

624ms, input, aspic, output, errors
T2/neg-pgarch-succeed
INF
181ms, INF, #vars: 1, input, output

360ms, input, output

492ms, input, output

43ms, input, output

170ms, input, aspic, output, errors
T2/neg-popl07-fail
INF
168ms, INF, #vars: 1, input, output

474ms, input, output

2498ms, input, output

464ms, input, output

607ms, input, aspic, output, errors
T2/neg-popl07-succeed
INF
206ms, INF, #vars: 1, input, output

742ms, input, output

2717ms, input, output

455ms, input, output

622ms, input, aspic, output, errors
T2/neg-smagilla-fail
INF
188ms, INF, #vars: 1, input, output

977ms, input, output

427ms, input, output

224ms, input, output

113ms, input, aspic, output, errors
T2/neg-smagilla-succeed
INF
189ms, INF, #vars: 1, input, output

970ms, input, output

513ms, input, output

212ms, input, output

105ms, input, aspic, output, errors
T2/nested
1 + 3 * free_3
108ms, INF, #vars: 1, input, output

1381ms, input, output

278ms, input, output

101ms, input, output

123ms, input, aspic, output, errors
T2/nested2
5001 + 5001 * meter_1
163ms, INF, #vars: 1, input, output

1394ms, input, output

253ms, input, output

89ms, input, output

92ms, input, aspic, output, errors
T2/new_ex
2 + free
562ms, INF, #vars: 1, input, output

2714ms, input, output

572ms, input, output

147ms, input, output

105ms, input, aspic, output, errors
T2/non_term
1
72ms, Ω(1), #vars: 0, input, output

2712ms, input, output

177ms, input, output

45ms, input, output

68ms, input, aspic
T2/ns
936
131ms, Ω(1), #vars: 0, input, output
15265
459ms, O(1), #vars: 0, input, output
937
617ms, O(1), #vars: 0, input, output
810
179ms, O(1), #vars: 0, input, output

155ms, input, aspic, output, errors
T2/oct_vs_subpoly
INF
32ms, INF, #vars: 1, input, output

719ms, input, output

216ms, input, output

55ms, input, output

83ms, input, aspic, output, errors
T2/p-1
INF
57ms, INF, #vars: 1, input, output

1249ms, input, output

199ms, input, output

39ms, input, output

105ms, input, aspic, output, errors
T2/p-10
INF
52ms, INF, #vars: 1, input, output

1342ms, input, output

301ms, input, output

47ms, input, output

117ms, input, aspic, output, errors
T2/p-12
2 + A
61ms, Ω(n), #vars: 1, input, output
A + 3
93ms, O(n), #vars: 1, input, output
max(A + 3, 2)
244ms, O(n), #vars: 1, input, output
max(0, A + 1)
56ms, O(n), #vars: 1, input, output

90ms, input, aspic, output, errors
T2/p-13
1
48ms, Ω(1), #vars: 0, input, output
2
58ms, O(1), #vars: 0, input, output
1
147ms, O(1), #vars: 0, input, output

34ms, input
3
66ms, O(1), #vars: 0, input, aspic, output
T2/p-14
A
60ms, Ω(n), #vars: 1, input, output
A + 2
91ms, O(n), #vars: 1, input, output
max(A + 1, 2)
166ms, O(n), #vars: 1, input, output
max(0, A + -1)
42ms, O(n), #vars: 1, input, output

8156ms, input, aspic, output, errors
T2/p-15
1 + A
58ms, Ω(n), #vars: 1, input, output
A + 2
89ms, O(n), #vars: 1, input, output
max(A + 2, 2)
348ms, O(n), #vars: 1, input, output
max(A, 0)
62ms, O(n), #vars: 1, input, output

72ms, input, aspic, output, errors
T2/p-16
1 + A
61ms, Ω(n), #vars: 1, input, output
A + 2
104ms, O(n), #vars: 1, input, output
max(A + 2, 2)
167ms, O(n), #vars: 1, input, output
max(A, 0)
49ms, O(n), #vars: 1, input, output

60ms, input, aspic, output, errors
T2/p-18
1 + A
56ms, Ω(n), #vars: 1, input, output
A + 2
96ms, O(n), #vars: 1, input, output
max(A + 2, 2)
183ms, O(n), #vars: 1, input, output
max(A, 0)
48ms, O(n), #vars: 1, input, output

64ms, input, aspic, output, errors
T2/p-19
INF
53ms, INF, #vars: 1, input, output

1098ms, input, output

250ms, input, output

46ms, input, output

107ms, input, aspic, output, errors
T2/p-19a
INF
55ms, INF, #vars: 1, input, output

1251ms, input, output

239ms, input, output

49ms, input, output

135ms, input, aspic, output, errors
T2/p-1a
INF
53ms, INF, #vars: 1, input, output

1350ms, input, output

231ms, input, output

54ms, input, output

112ms, input, aspic, output, errors
T2/p-1b
1 + B - A
78ms, Ω(n), #vars: 2, input, output
A + B + 2
74ms, O(n), #vars: 2, input, output
max(-1 * A + B + 2, 2)
184ms, O(n), #vars: 2, input, output
max(0, B - A)
42ms, O(n), #vars: 2, input, output

92ms, input, aspic, output, errors
T2/p-1c
INF
64ms, INF, #vars: 1, input, output

1304ms, input, output

323ms, input, output

49ms, input, output

133ms, input, aspic, output, errors
T2/p-1d
1 + B - A
257ms, Ω(n), #vars: 2, input, output
3 * A + 3 * B + 2
171ms, O(n), #vars: 2, input, output
max(-1 * A + B + 2, 2)
215ms, O(n), #vars: 2, input, output
max(0, max(0, B - A) *...
124ms, O(n2), #vars: 2, input, output

76ms, input, aspic, output, errors
T2/p-20
INF
73ms, INF, #vars: 1, input, output

146ms, input, output

234ms, input, output

50ms, input, output

200ms, input, aspic, output, errors
T2/p-21
-27 + A
91ms, Ω(n), #vars: 1, input, output
A + 64 * B + 1314
172ms, O(n), #vars: 2, input, output
max(A + 2 * B + -68, A...
249ms, O(n), #vars: 2, input, output
max(0, B + -20) + max(...
94ms, O(n), #vars: 1, input, output

84ms, input, aspic, output, errors
T2/p-22
A
62ms, Ω(n), #vars: 1, input, output
A + 3
131ms, O(n), #vars: 1, input, output
max(A + 1, 2)
168ms, O(n), #vars: 1, input, output
max(0, A + -1)
47ms, O(n), #vars: 1, input, output
max(3, A__o' + 1 + 1 + 1)
67ms, O(n), #vars: 1, input, aspic, output
T2/p-3
1 + B - A
142ms, Ω(n), #vars: 2, input, output
A + B + 3
120ms, O(n), #vars: 2, input, output
max(-1 * A + B + 3, 3)
206ms, O(n), #vars: 2, input, output

94ms, input, output

93ms, input, aspic, output, errors
T2/p-32
1
67ms, Ω(1), #vars: 0, input, output

1149ms, input, output

183ms, input, output

50ms, input, output

76ms, input, aspic, output, errors
T2/p-33
1
141ms, Ω(1), #vars: 0, input, output

248ms, input, output

204ms, input, output

112ms, input, output

109ms, input, aspic, output, errors
T2/p-34
INF
155ms, INF, #vars: 1, input, output

225ms, input, output

1251ms, input, output

204ms, input, output

1870ms, input, aspic, output, errors
T2/p-36
INF
128ms, INF, #vars: 1, input, output

1011ms, input, output

526ms, input, output

53ms, input, output

568ms, input, aspic, output, errors
T2/p-37
1
81ms, Ω(1), #vars: 0, input, output
8
153ms, O(1), #vars: 0, input, output
6
249ms, O(1), #vars: 0, input, output
4
57ms, O(1), #vars: 0, input, output

86ms, input, aspic, output
T2/p-4
1 - B + A
171ms, Ω(n), #vars: 2, input, output
107 * A + 108 * B + 3 ...
133ms, O(n2), #vars: 3, input, output
max(2 * A + -1 * B + -...
302ms, O(n), #vars: 3, input, output
max(0, max(0, B + -1 +...
82ms, O(n2), #vars: 2, input, output

105ms, input, aspic, output, errors
T2/p-40
500 - free_3
68ms, INF, #vars: 1, input, output

918ms, input, output

275ms, input, output

66ms, input, output

88ms, input, aspic, output, errors
T2/p-41
1
17ms, Ω(1), #vars: 0, input, output
1
14ms, O(1), #vars: 0, input, output
1
149ms, O(1), #vars: 0, input, output

35ms, input
3
76ms, O(1), #vars: 0, input, aspic, output
T2/p-42
3 - A
129ms, Ω(n), #vars: 1, input, output
A + B + 7
208ms, O(n), #vars: 2, input, output
max(-1 * A + -1 * B + ...
242ms, O(n), #vars: 2, input, output
max(0, 2 - A) + max(0,...
61ms, O(n), #vars: 1, input, output

83ms, input, aspic, output, errors
T2/p-43
1
351ms, Ω(1), #vars: 0, input, output

536ms, input, output

252ms, input, output

72ms, input, output

145ms, input, aspic, output, errors
T2/p-43-terminate
1
4431ms, Ω(1), #vars: 0, input, output

6310ms, input, output

201ms, input, output, errors

73ms, input, output

559ms, input, aspic, output
T2/p-44
1
113ms, Ω(1), #vars: 0, input, output
A + 3
155ms, O(n), #vars: 1, input, output
max(A + 2, 2)
377ms, O(n), #vars: 1, input, output
max(A, 0)
55ms, O(n), #vars: 1, input, output

88ms, input, aspic, output, errors
T2/p-45
1 + B
274ms, Ω(n), #vars: 1, input, output
B + 3
201ms, O(n), #vars: 1, input, output
max(B + 2, 2, A + 2)
303ms, O(n), #vars: 2, input, output
max(B, 0)
54ms, O(n), #vars: 1, input, output

109ms, input, aspic, output, errors
T2/p-46
1
1459ms, Ω(1), #vars: 0, input, output

451ms, input, output

306ms, input, output

174ms, input, output

119ms, input, aspic
T2/p-49
2 + A
56ms, Ω(n), #vars: 1, input, output
A + 3
92ms, O(n), #vars: 1, input, output
max(A + 3, 2)
170ms, O(n), #vars: 1, input, output
max(0, A + 1)
60ms, O(n), #vars: 1, input, output

110ms, input, aspic, output, errors
T2/p-5
1 + B - A
199ms, Ω(n), #vars: 2, input, output

2602ms, input, output

837ms, input, output

170ms, input, output

381ms, input, aspic, output, errors
T2/p-52
INF
52ms, INF, #vars: 1, input, output

1387ms, input, output

220ms, input, output

53ms, input, output

98ms, input, aspic, output, errors
T2/p-53
1
43ms, Ω(1), #vars: 0, input, output
2
32ms, O(1), #vars: 0, input, output
1
149ms, O(1), #vars: 0, input, output

53ms, input
3
67ms, O(1), #vars: 0, input, aspic, output
T2/p-55
1 - A
470ms, Ω(n), #vars: 1, input, output
202 * B + 2 * A + 2 * ...
314ms, O(n2), #vars: 2, input, output
max(-1 * A + 102, 2, m...
297ms, O(n), #vars: 2, input, output
max(0, 1 + max(0, -1 -...
160ms, O(n), #vars: 1, input, output

83ms, input, aspic
T2/p-56
0 - D
329ms, Ω(n), #vars: 1, input, output
2 * D + 5
239ms, O(n), #vars: 1, input, output
max(-1 * D + 1, 2)
404ms, O(n), #vars: 1, input, output
max(0, -1 - D)
87ms, O(n), #vars: 1, input, output

97ms, input, aspic, output, errors
T2/p-58
1
53ms, Ω(1), #vars: 0, input, output
3
71ms, O(1), #vars: 0, input, output
1
155ms, O(1), #vars: 0, input, output

40ms, input, output

86ms, input, aspic, output
T2/p-6
1 + B - A
259ms, Ω(n), #vars: 2, input, output
3 * A + 3 * B + 2
171ms, O(n), #vars: 2, input, output
max(-1 * A + B + 2, 2)
259ms, O(n), #vars: 2, input, output
max(0, max(0, B - A) *...
147ms, O(n2), #vars: 2, input, output

87ms, input, aspic, output, errors
T2/p-60
101
86ms, Ω(1), #vars: 0, input, output
103
115ms, O(1), #vars: 0, input, output
102
194ms, O(1), #vars: 0, input, output
100
47ms, O(1), #vars: 0, input, output
max(104, 3)
92ms, O(1), #vars: 0, input, aspic, output
T2/p-61
901
73ms, Ω(1), #vars: 0, input, output
1003
122ms, O(1), #vars: 0, input, output
902
200ms, O(1), #vars: 0, input, output
900
44ms, O(1), #vars: 0, input, output
904
100ms, O(1), #vars: 0, input, aspic, output
T2/p-63
1
64ms, Ω(1), #vars: 0, input, output
A + 4
313ms, O(n), #vars: 1, input, output
max(A + 3, 2)
231ms, O(n), #vars: 1, input, output

45ms, input, output

78ms, input, aspic
T2/p-7
1 + meter
83ms, Ω(n), #vars: 1, input, output
B + C + 3
111ms, O(n), #vars: 2, input, output
max(-1 / 2 * B + 1 / 2...
212ms, O(n), #vars: 2, input, output
max(0, C + -1 + 0 - B)
130ms, O(n), #vars: 2, input, output

86ms, input, aspic, output, errors
T2/p-7b
1 + meter
97ms, Ω(n), #vars: 1, input, output
B + C + 4
107ms, O(n), #vars: 2, input, output
max(-1 / 2 * B + 1 / 2...
270ms, O(n), #vars: 2, input, output
max(0, C + -1 + 0 - B)
105ms, O(n), #vars: 2, input, output

77ms, input, aspic, output, errors
T2/p-8
INF
51ms, INF, #vars: 1, input, output

1069ms, input, output

200ms, input, output

39ms, input, output

72ms, input, aspic, output, errors
T2/p-9
INF
52ms, INF, #vars: 1, input, output

1063ms, input, output

201ms, input, output

50ms, input, output

108ms, input, aspic, output, errors
T2/pearl-necklace
4 - B + 4 * A
154ms, Ω(n), #vars: 2, input, output
157 * A + 145 * B + 29...
363ms, O(n), #vars: 2, input, output
max(4 * A + -1 * B + 4...
509ms, O(n), #vars: 2, input, output
max(0, max(B, 0) + max...
65ms, O(n), #vars: 2, input, output

102ms, input, aspic, output, errors
T2/pentagon
1
117ms, Ω(1), #vars: 0, input, output

1040ms, input, output

392ms, input, output

553ms, input, output

242ms, input, aspic, output, errors
T2/pgarch

60013ms, input, output

41916ms, input, output

60001ms, input

11949ms, input, output

161ms, input, aspic, aspic (errors)
T2/pldi
-1 / 2 - 1 / 2 * (-1 +...
392ms, Ω(n2), #vars: 1, input, output
12 * B + 8 * B^2 + 5
630ms, O(n2), #vars: 1, input, output
max(4, (B + 1) * (B + ...
323ms, O(n2), #vars: 1, input, output
max(B, 0) + max(0, max...
208ms, O(n3), #vars: 1, input, output

82ms, input, aspic, output, errors
T2/polling
INF
636ms, INF, #vars: 1, input, output

14470ms, input, output

60001ms, input, output

395ms, input, output

5081ms, input, aspic
T2/polling.bug
INF
1032ms, INF, #vars: 1, input, output

15900ms, input, output

60001ms, input, output

551ms, input, output

5888ms, input, aspic
T2/polyrank1
1
59ms, Ω(1), #vars: 0, input, output

2609ms, input, output

179ms, input, output

52ms, input, output

81ms, input, aspic
T2/polyrank2
1
57ms, Ω(1), #vars: 0, input, output

5291ms, input, output

259ms, input, output

46ms, input, output

75ms, input, aspic
T2/polyrank3
1
78ms, Ω(1), #vars: 0, input, output

5884ms, input, output

198ms, input, output

60ms, input, output

92ms, input, aspic
T2/polyrank4
1
73ms, Ω(1), #vars: 0, input, output

10955ms, input, output

198ms, input, output

50ms, input, output

65ms, input, aspic
T2/polyrank5
1 + A
95ms, Ω(n), #vars: 1, input, output

6397ms, input, output

209ms, input, output

60ms, input, output

81ms, input, aspic
T2/polyrank6
1 + A
175ms, Ω(n), #vars: 1, input, output

5327ms, input, output

215ms, input, output

133ms, input, output

67ms, input, aspic
T2/polyrank7
INF
47ms, INF, #vars: 1, input, output

5887ms, input, output

190ms, input, output

54ms, input, output

85ms, input, aspic
T2/popl07-fail
INF
168ms, INF, #vars: 1, input, output

466ms, input, output

1712ms, input, output

498ms, input, output

538ms, input, aspic, output, errors
T2/popl07-succeed
INF
181ms, INF, #vars: 1, input, output

488ms, input, output

2135ms, input, output

470ms, input, output

531ms, input, aspic, output, errors
T2/print
1 + Q + free_199
10296ms, INF, #vars: 2, input, output

13373ms, input, output

13921ms, input, output

1442ms, input, output

74ms, input, aspic, aspic (errors)
T2/qrdcmp
4 - D + A
607ms, Ω(n), #vars: 2, input, output
162 * A + 12 * K + 5 *...
669ms, O(n), #vars: 4, input, output

11707ms, input, output
max(0, A + 1 + 0 - K) ...
785ms, O(n), #vars: 2, input, output

565ms, input, aspic
T2/qrdcmp.c.i.qrdcmp.pl.t2.fixed
nonlinear
4 - D + A
914ms, Ω(n), #vars: 2, input, output
162 * A + 12 * K + 5 *...
867ms, O(n), #vars: 4, input, output

10193ms, input, output
max(0, A + 1 + 0 - K) ...
717ms, O(n), #vars: 2, input, output
Non-linear example not handled by prover.
T2/qrdcmp.c.i.qrdcmp.pl.t2.nor.t2.rlgfixed
4 - D + A
587ms, Ω(n), #vars: 2, input, output
162 * A + 12 * K + 5 *...
692ms, O(n), #vars: 4, input, output

11309ms, input, output
max(0, A + 1 + 0 - K) ...
716ms, O(n), #vars: 2, input, output

692ms, input, aspic
T2/queens
1
2308ms, Ω(1), #vars: 0, input, output
1157351968
5350ms, O(1), #vars: 0, input, output

60001ms, input, output
288
924ms, O(1), #vars: 0, input, output

731ms, input, aspic, output
T2/queue_1
1
120ms, Ω(1), #vars: 0, input, output
17
424ms, O(1), #vars: 0, input, output
7
227ms, O(1), #vars: 0, input, output
2
72ms, O(1), #vars: 0, input, output
9
124ms, O(1), #vars: 0, input, aspic, output
T2/queue_10
1
116ms, Ω(1), #vars: 0, input, output
276
453ms, O(1), #vars: 0, input, output
43
236ms, O(1), #vars: 0, input, output
20
66ms, O(1), #vars: 0, input, output
45
155ms, O(1), #vars: 0, input, aspic, output
T2/queue_100
1
122ms, Ω(1), #vars: 0, input, output
2886
463ms, O(1), #vars: 0, input, output
403
244ms, O(1), #vars: 0, input, output
200
68ms, O(1), #vars: 0, input, output
405
122ms, O(1), #vars: 0, input, aspic, output
T2/queue_1000
1
119ms, Ω(1), #vars: 0, input, output
28986
417ms, O(1), #vars: 0, input, output
4003
232ms, O(1), #vars: 0, input, output
2000
70ms, O(1), #vars: 0, input, output
4005
129ms, O(1), #vars: 0, input, aspic, output
T2/randomwalk
1
2374ms, Ω(1), #vars: 0, input, output

4892ms, input, output

548ms, input, output

228ms, input, output

130ms, input, aspic, output, errors
T2/randomwalk_withassume
1
2937ms, Ω(1), #vars: 0, input, output

5188ms, input, output

1117ms, input, output

134ms, input, output
1
177ms, O(1), #vars: 0, input, aspic, output, errors
T2/refine_disj_problem
INF
109ms, INF, #vars: 1, input, output

1644ms, input, output

196ms, input, output

74ms, input, output

82ms, input, aspic
T2/rev_nt2
INF
499ms, INF, #vars: 1, input, output

1311ms, input, output

4039ms, input, output

167ms, input, output

2288ms, input, aspic, output
T2/rev_nt3
INF
525ms, INF, #vars: 1, input, output

1410ms, input, output

3185ms, input, output

197ms, input, output

2348ms, input, aspic, output
T2/rev_nt4
1
38ms, Ω(1), #vars: 0, input, output
2
18ms, O(1), #vars: 0, input, output
1
159ms, O(1), #vars: 0, input, output

33ms, input

79ms, input, aspic, output
T2/reverse
1 + free_347 + S
15315ms, INF, #vars: 2, input, output

9800ms, input, output

31045ms, input, output

60001ms, input, output

104ms, input, aspic, aspic (errors)
T2/reverse_div4
INF
890ms, INF, #vars: 1, input, output

738ms, input, output

3764ms, input, output

112ms, input, output

64ms, input, aspic, aspic (errors)
T2/reverse_seg_cyclic
1 + N + E1
11072ms, Ω(n), #vars: 2, input, output
16 * J + 16 * K + 16 *...
6952ms, O(n), #vars: 6, input, output
max(N, 2)
19807ms, O(n), #vars: 1, input, output

42934ms, input, output

71ms, input, aspic, aspic (errors)
T2/rewrite
INF
27ms, INF, #vars: 1, input, output

533ms, input, output

251ms, input, output

43ms, input, output

79ms, input, aspic, output, errors
T2/rlft3
6 - 2 * K + 2 * J
5650ms, Ω(n), #vars: 2, input, output
24 * H + 24 * I + 4 * ...
3119ms, O(n), #vars: 7, input, output

60001ms, input, output

1267ms, input, output

2316ms, input, aspic, output
T2/rlft3.c.i.rlft3.pl.t2.fixed
nonlinear
5 - K + J
3994ms, Ω(n), #vars: 2, input, output
52 * H + 52 * I + 3 * ...
3073ms, O(n), #vars: 7, input, output

60001ms, input, output

1482ms, input, output
Non-linear example not handled by prover.
T2/s1-saved
1 + H + free_212
8377ms, INF, #vars: 2, input, output

10711ms, input, output

7666ms, input, output

1335ms, input, output

69ms, input, aspic, aspic (errors)
T2/s3-work
2 + B
52146ms, Ω(n), #vars: 1, input, output

60025ms, input

60001ms, input, output

60001ms, input, output

109ms, input, aspic, aspic (errors)
T2/sas1
1 + B
386ms, Ω(n), #vars: 1, input, output
19 * B + 7
819ms, O(n), #vars: 1, input, output
max(4 * B + 4, B + 7, 5)
513ms, O(n), #vars: 1, input, output
max(0, -2 + max(B, 0))...
154ms, O(n), #vars: 1, input, output

118ms, input, aspic, output, errors
T2/sas2
1
1183ms, Ω(1), #vars: 0, input, output

6264ms, input, output
max(C + 11, -1 * C + 2...
3240ms, O(n), #vars: 1, input, output

142ms, input, output

390ms, input, aspic, output, errors
T2/select
1
333ms, Ω(1), #vars: 0, input, output

16811ms, input, output

19915ms, input, output

1275ms, input, output

790ms, input, aspic, output, errors
T2/selectSort
1 / 2 - 1 / 2 * (-1 + ...
265ms, Ω(n2), #vars: 1, input, output
23 * C + 12 * C^2 + 4
1293ms, O(n2), #vars: 1, input, output
max(5, (C + 1) * (C + ...
756ms, O(n2), #vars: 1, input, output
max(C, 0) + max(0, C +...
71ms, O(n2), #vars: 1, input, output

184ms, input, aspic, output, errors
T2/send-more-money
1
125ms, Ω(1), #vars: 0, input, output
129
2142ms, O(1), #vars: 0, input, output

60001ms, input, output

103ms, input

60001ms, input, aspic
T2/seq
2 + A
59ms, Ω(n), #vars: 1, input, output
A + 2
77ms, O(n), #vars: 1, input, output
max(A + 2, 1)
313ms, O(n), #vars: 1, input, output
max(0, A + 1)
52ms, O(n), #vars: 1, input, output

87ms, input, aspic, output, errors
T2/seq2
1 + A
59ms, Ω(n), #vars: 1, input, output
A + 1
78ms, O(n), #vars: 1, input, output
max(A + 1, 1)
168ms, O(n), #vars: 1, input, output
max(A, 0)
44ms, O(n), #vars: 1, input, output
1 + 1 + A__o' + 1
79ms, O(n), #vars: 1, input, aspic, output
T2/sequential_swap
1
43ms, Ω(1), #vars: 0, input, output
2
42ms, O(1), #vars: 0, input, output
1
177ms, O(1), #vars: 0, input, output

43ms, input
3
98ms, O(1), #vars: 0, input, aspic, output
T2/simple
INF
67ms, INF, #vars: 1, input, output

1821ms, input, output

171ms, input, output

55ms, input, output

72ms, input, aspic, output, errors
T2/simpleWhile
1 + C
113ms, Ω(n), #vars: 1, input, output
2 * C + 7
190ms, O(n), #vars: 1, input, output
max(C + 3, 3)
376ms, O(n), #vars: 1, input, output
max(C, 0) + max(C, 0) ...
55ms, O(n), #vars: 1, input, output

107ms, input, aspic, output, errors
T2/simple_array_inversion
3
56ms, Ω(1), #vars: 0, input, output
5
84ms, O(1), #vars: 0, input, output
4
214ms, O(1), #vars: 0, input, output
2
48ms, O(1), #vars: 0, input, output
6
92ms, O(1), #vars: 0, input, aspic, output
T2/simple_control_on_input
1
64ms, Ω(1), #vars: 0, input, output
22
91ms, O(1), #vars: 0, input, output
21
161ms, O(1), #vars: 0, input, output

55ms, input, output
max(23, 3)
92ms, O(1), #vars: 0, input, aspic, output
T2/simple_double_free
1
16ms, Ω(1), #vars: 0, input, output
1
21ms, O(1), #vars: 0, input, output
1
140ms, O(1), #vars: 0, input, output

42ms, input
3
57ms, O(1), #vars: 0, input, aspic, output
T2/simple_fail
1
19ms, Ω(1), #vars: 0, input, output
1
16ms, O(1), #vars: 0, input, output
1
221ms, O(1), #vars: 0, input, output

46ms, input
3
81ms, O(1), #vars: 0, input, aspic, output
T2/simple_pre
1
19ms, Ω(1), #vars: 0, input, output
1
16ms, O(1), #vars: 0, input, output
1
162ms, O(1), #vars: 0, input, output

46ms, input
3
85ms, O(1), #vars: 0, input, aspic, output
T2/simple_pre1
1
21ms, Ω(1), #vars: 0, input, output
1
20ms, O(1), #vars: 0, input, output
1
174ms, O(1), #vars: 0, input, output

42ms, input
3
85ms, O(1), #vars: 0, input, aspic, output
T2/simple_pre2
1
17ms, Ω(1), #vars: 0, input, output
1
20ms, O(1), #vars: 0, input, output
1
142ms, O(1), #vars: 0, input, output

35ms, input
3
78ms, O(1), #vars: 0, input, aspic, output
T2/simple_pre3
1
18ms, Ω(1), #vars: 0, input, output
4
25ms, O(1), #vars: 0, input, output
1
144ms, O(1), #vars: 0, input, output

35ms, input

90ms, input, aspic, output
T2/simple_swap_call
1
43ms, Ω(1), #vars: 0, input, output
2
32ms, O(1), #vars: 0, input, output
1
153ms, O(1), #vars: 0, input, output

36ms, input
3
78ms, O(1), #vars: 0, input, aspic, output
T2/slayer-1-filtered
1 + free_53 + G
615ms, INF, #vars: 2, input, output

4930ms, input, output

3220ms, input, output

74ms, input, output

73ms, input, aspic, aspic (errors)
T2/slayer-1-rf
3
1082ms, Ω(1), #vars: 0, input, output

10662ms, input, output

4652ms, input, output

130ms, input, output

64ms, input, aspic, aspic (errors)
T2/slayer-2-filtered
11
56ms, Ω(1), #vars: 0, input, output
12
144ms, O(1), #vars: 0, input, output
12
193ms, O(1), #vars: 0, input, output
10
51ms, O(1), #vars: 0, input, output

86ms, input, aspic, output
T2/slayer-3

60014ms, input, output

60021ms, input

60001ms, input

60001ms, input, output

187ms, input, aspic, aspic (errors)
T2/slayer-3-filtered
1 + B
5633ms, Ω(n), #vars: 1, input, output

49081ms, input, output

60004ms, input, output

686ms, input, output

77ms, input, aspic, aspic (errors)
T2/slayer-3-new

60013ms, input, output

60026ms, input

60001ms, input

60002ms, input, output, errors

194ms, input, aspic, aspic (errors)
T2/slayer-4-filtered

60011ms, input, output

60021ms, input

60001ms, input

21555ms, input, output

108ms, input, aspic, aspic (errors)
T2/slayer-n1
INF
2860ms, INF, #vars: 1, input, output

1649ms, input, output

2834ms, input, output

416ms, input, output

9049ms, input, aspic
T2/slayer-n1-filtered
INF
339ms, INF, #vars: 1, input, output

1905ms, input, output

1316ms, input, output

66ms, input, output

3467ms, input, aspic
T2/slayer-n2
INF
31ms, INF, #vars: 1, input, output

936ms, input, output

195ms, input, output

48ms, input, output

86ms, input, aspic, output, errors
T2/slayer-n2-filtered
INF
31ms, INF, #vars: 1, input, output

867ms, input, output

177ms, input, output

52ms, input, output

80ms, input, aspic, output, errors
T2/slayer-n3-filtered
1
89ms, Ω(1), #vars: 0, input, output
7
192ms, O(1), #vars: 0, input, output

239ms, input, output, errors

67ms, input

1972ms, input, aspic, output
T2/slayer-n5-filtered
5 + free_53 - V + J1
2467ms, Ω(n), #vars: 3, input, output

11792ms, input, output

20548ms, input, output

305ms, input, output

73ms, input, aspic, aspic (errors)
T2/smagilla-succeed
INF
196ms, INF, #vars: 1, input, output

921ms, input, output

404ms, input, output

268ms, input, output

97ms, input, aspic, output, errors
T2/smagillb-succeed
INF
209ms, INF, #vars: 1, input, output

459ms, input, output

808ms, input, output

250ms, input, output

132ms, input, aspic, output, errors
T2/smagillc-fail
INF
196ms, INF, #vars: 1, input, output

879ms, input, output

590ms, input, output

239ms, input, output

118ms, input, aspic, output, errors
T2/smagillc-succeed
INF
189ms, INF, #vars: 1, input, output

1027ms, input, output

512ms, input, output

221ms, input, output

113ms, input, aspic, output, errors
T2/sort
1
1152ms, Ω(1), #vars: 0, input, output
3977
1170ms, O(1), #vars: 0, input, output

60003ms, input, output

410ms, input, output

748ms, input, aspic, output
T2/spctrm
4 - J + D
9855ms, Ω(n), #vars: 2, input, output
186 * N + 186 * O + 16...
4268ms, O(n), #vars: 6, input, output

60001ms, input, output

903ms, input, output

2343ms, input, aspic
T2/spctrm.c.i.spctrm.pl.t2.fixed
nonlinear
4 - J
1212ms, Ω(n), #vars: 1, input, output
186 * N + 186 * O + 16...
4289ms, O(n), #vars: 6, input, output

60001ms, input, output

724ms, input, output
Non-linear example not handled by prover.
T2/spctrm.c.i.spctrm.pl.t2.nor.t2.rlgfixed
4 - J + D
9829ms, Ω(n), #vars: 2, input, output
186 * N + 186 * O + 16...
4354ms, O(n), #vars: 6, input, output

60001ms, input, output

783ms, input, output

2596ms, input, aspic
T2/spiral
B
3032ms, Ω(n), #vars: 1, input, output
9 * A * B + B^2 + 25 *...
1587ms, O(n2), #vars: 2, input, output
max(2 * A + B + -1, -1...
672ms, O(n), #vars: 2, input, output

34437ms, input, output

96ms, input, aspic, output, errors
T2/st88
19 - 2 * free_2
556ms, INF, #vars: 1, input, output

2853ms, input, output

223ms, input, output

269ms, input, output

87ms, input, aspic, output, errors
T2/st88.bug
13 - 2 * free_2
1235ms, INF, #vars: 1, input, output

3398ms, input, output

244ms, input, output

119ms, input, output

84ms, input, aspic, output, errors
T2/statemate
1
49097ms, Ω(1), #vars: 0, input, output

60015ms, input

60001ms, input

4336ms, input, output

98ms, input, aspic, aspic (errors)
T2/stored
1
149ms, Ω(1), #vars: 0, input, output

1618ms, input, output

288ms, input, output

125ms, input, output

83ms, input, aspic, output, errors
T2/streamserver-succeed
INF
796ms, INF, #vars: 1, input, output

14421ms, input, output

60001ms, input, output

791ms, input, output

2413ms, input, aspic, output
T2/streamserver.bug
INF
1077ms, INF, #vars: 1, input, output

16418ms, input, output

60001ms, input, output

379ms, input, output

2551ms, input, aspic, output
T2/subpoly_crash
INF
50ms, INF, #vars: 1, input, output

1223ms, input, output

364ms, input, output

46ms, input, output

80ms, input, aspic, output, errors
T2/sudoku
nonlinear
2 + free^2 + 2 * free
1088ms, INF, #vars: 1, input, output

60013ms, input

60001ms, input, output

8725ms, input, output
Non-linear example not handled by prover.
T2/sumit
1 - 3 * B + 3 * C
605ms, Ω(n), #vars: 2, input, output

2334ms, input, output
max(-3 * B + 3 * C + 6...
1455ms, O(n), #vars: 2, input, output

255ms, input, output

132ms, input, aspic, output, errors
T2/svdcmp
4 + H - A
24411ms, Ω(n), #vars: 2, input, output

60013ms, input

4966ms, input, output, errors

535ms, input, output

38511ms, input, aspic
T2/svdcmp.c.i.svdcmp.pl.t2.fixed
nonlinear

60025ms, input, output

60014ms, input

5196ms, input, output, errors

536ms, input, output
Non-linear example not handled by prover.
T2/svdcmp.c.i.svdcmp.pl.t2.nor.t2.rlgfixed
4 + H - A
21851ms, Ω(n), #vars: 2, input, output

60012ms, input

5242ms, input, output, errors

489ms, input, output

32830ms, input, aspic
T2/toeplz
-14 + 3 / 2 * (-2 + A)...
1283ms, Ω(n2), #vars: 1, input, output

5709ms, input, output

13199ms, input, output

262ms, input, output

1131ms, input, aspic, output, errors
T2/toeplz.c.i.toeplz.pl.t2.fixed
nonlinear
10
4356ms, Ω(1), #vars: 0, input, output
522470403373181 * A + ...
1975ms, O(n2), #vars: 1, input, output
max(3, (7 / 2 * A + -3...
9803ms, O(n2), #vars: 1, input, output

298ms, input, output
Non-linear example not handled by prover.
T2/toeplz.c.i.toeplz.pl.t2.nor.t2.rlgfixed
-14 + 3 / 2 * (-2 + A)...
1303ms, Ω(n2), #vars: 1, input, output

5988ms, input, output

12993ms, input, output

261ms, input, output

1107ms, input, aspic, output, errors
T2/tqli
4 - B - D + 2 * A
9859ms, Ω(n), #vars: 3, input, output

13352ms, input, output

60001ms, input, output

1240ms, input, output

2752ms, input, aspic, output
T2/tqli.c.i.tqli.pl.t2.fixed
nonlinear

60016ms, input, output

17890ms, input, output

60002ms, input, output

1050ms, input, output
Non-linear example not handled by prover.
T2/tqli.c.i.tqli.pl.t2.nor.t2.rlgfixed
4 - B - D + 2 * A
9481ms, Ω(n), #vars: 3, input, output

13698ms, input, output

60001ms, input, output

1290ms, input, output

2640ms, input, aspic, output
T2/traverse
1 + free_195 + D
8405ms, INF, #vars: 2, input, output

10061ms, input, output

9326ms, input, output

1715ms, input, output

68ms, input, aspic, aspic (errors)
T2/traverse2
-1 + free_938
52182ms, INF, #vars: 1, input, output

60016ms, input

22970ms, input, output

49052ms, input, output, errors

96ms, input, aspic, aspic (errors)
T2/traverse_seg
1 + E + free_221
7957ms, INF, #vars: 2, input, output

14218ms, input, output

17553ms, input, output

3432ms, input, output

83ms, input, aspic, aspic (errors)
T2/traverse_seg2
1 + R + free_207
8312ms, INF, #vars: 2, input, output

15538ms, input, output

11977ms, input, output

2567ms, input, output

83ms, input, aspic, aspic (errors)
T2/traverse_twice
1 + free_270 + D
11160ms, INF, #vars: 2, input, output

27630ms, input, output

16526ms, input, output

2139ms, input, output

87ms, input, aspic, aspic (errors)
T2/two_arrays
306
150ms, Ω(1), #vars: 0, input, output
3043
669ms, O(1), #vars: 0, input, output
307
575ms, O(1), #vars: 0, input, output
300
89ms, O(1), #vars: 0, input, output
309
208ms, O(1), #vars: 0, input, aspic, output
T2/two_arrays1
408
195ms, Ω(1), #vars: 0, input, output
3289
1027ms, O(1), #vars: 0, input, output
409
872ms, O(1), #vars: 0, input, output
400
130ms, O(1), #vars: 0, input, output

244ms, input, aspic, output
T2/two_arrays2
8 + 8 * E
192ms, Ω(n), #vars: 1, input, output
18 * E + 55
1135ms, O(n), #vars: 1, input, output
max(8 * E + 9, 9)
1157ms, O(n), #vars: 1, input, output
max(E, 0) + max(E, 0) ...
131ms, O(n), #vars: 1, input, output

281ms, input, aspic, output
T2/two_arrays6
8 + 8 * E
199ms, Ω(n), #vars: 1, input, output
20 * E + 51
1131ms, O(n), #vars: 1, input, output
max(8 * E + 9, 9)
1088ms, O(n), #vars: 1, input, output
max(E, 0) + max(E, 0) ...
176ms, O(n), #vars: 1, input, output

282ms, input, aspic, output
T2/ud
1
752ms, Ω(1), #vars: 0, input, output
76604 * F + 76604 * G ...
6770ms, O(n), #vars: 4, input, output
381
5001ms, O(1), #vars: 0, input, output
770
746ms, O(1), #vars: 0, input, output

451ms, input, aspic
T2/vmcai_bytes
1
17ms, Ω(1), #vars: 0, input, output
1
15ms, O(1), #vars: 0, input, output
1
148ms, O(1), #vars: 0, input, output

39ms, input
3
84ms, O(1), #vars: 0, input, aspic, output
T2/vmcai_struct
1
19ms, Ω(1), #vars: 0, input, output
1
14ms, O(1), #vars: 0, input, output
1
143ms, O(1), #vars: 0, input, output

35ms, input
3
70ms, O(1), #vars: 0, input, aspic, output
T2/w1
INF
95ms, INF, #vars: 1, input, output

1142ms, input, output

163ms, input, output

40ms, input, output

92ms, input, aspic, output, errors
T2/w2_nt
INF
478ms, INF, #vars: 1, input, output

1285ms, input, output

2289ms, input, output

156ms, input, output

1209ms, input, aspic, output
T2/walk
1
236ms, Ω(1), #vars: 0, input, output

2957ms, input, output

512ms, input, output

65ms, input, output

292ms, input, aspic, output, errors
T2/wrong_loop
INF
434ms, INF, #vars: 1, input, output

516ms, input, output

303ms, input, output

119ms, input, output

85ms, input, aspic, output, errors
T2/wtf
1
10628ms, Ω(1), #vars: 0, input, output
111 * C + 111 * E + 11...
1481ms, O(n), #vars: 4, input, output

60001ms, input, output

215ms, input, output

758ms, input, aspic, output
T2/zeroconf
1
8128ms, Ω(1), #vars: 0, input, output

53695ms, input, output

4343ms, input, output

220ms, input, output

52192ms, input, aspic, aspic (errors)
T2/zeroconf_withassume
1
8929ms, Ω(1), #vars: 0, input, output

55691ms, input, output

5649ms, input, output

285ms, input, output

55314ms, input, aspic, aspic (errors)
c-examples/ABC/ex01
4 + 2 * B - 2 * A
88ms, Ω(n), #vars: 2, input, output
4 * A + 4 * B + 6
95ms, O(n), #vars: 2, input, output
max(-2 * A + 2 * B + 6...
192ms, O(n), #vars: 2, input, output
max(0, B + 1 + 0 - A)
44ms, O(n), #vars: 2, input, output

102ms, input, aspic, output, errors
c-examples/ABC/ex02
2 + 4 * B + B^2
104ms, Ω(n2), #vars: 1, input, output
906 * B + 72 * B^2 + 298
204ms, O(n2), #vars: 1, input, output
max(4, (2 * B + 3) * B...
288ms, O(n2), #vars: 1, input, output
max(B, 0) + max(0, 1 +...
76ms, O(n2), #vars: 1, input, output

91ms, input, aspic, output, errors
c-examples/ABC/ex03
-5 / 6 - 3 / 4 * (-1 +...
219ms, Ω(n4), #vars: 1, input, output
159238928 * B + 242186...
494ms, O(n6), #vars: 1, input, output
max(9, (B + -1) * max(...
1179ms, O(n4), #vars: 1, input, output
max(B, 0) + max(0, 1 +...
141ms, O(n4), #vars: 1, input, output

155ms, input, aspic, output, errors
c-examples/ABC/ex04
nonlinear
1
433ms, Ω(1), #vars: 0, input, output

6191ms, input, output

830ms, input, output

206ms, input, output
Non-linear example not handled by prover.
c-examples/ABC/ex05
2 + 4 * B + B^2
104ms, Ω(n2), #vars: 1, input, output
2238 * B + 72 * B^2 + ...
206ms, O(n2), #vars: 1, input, output
max(4, (2 * B + 3) * B...
287ms, O(n2), #vars: 1, input, output
max(B, 0) + max(0, 1 +...
74ms, O(n2), #vars: 1, input, output

103ms, input, aspic, output, errors
c-examples/ABC/ex06
2 + 4 * B + B^2
98ms, Ω(n2), #vars: 1, input, output
13106 * B + 84 * B^2 +...
206ms, O(n2), #vars: 1, input, output
max(4, (2 * B + 3) * B...
273ms, O(n2), #vars: 1, input, output
max(B, 0) + max(0, max...
68ms, O(n2), #vars: 1, input, output

101ms, input, aspic, output, errors
c-examples/ABC/ex07
2 + 3 * B + 2 * B * D
101ms, Ω(n2), #vars: 2, input, output
30 * B + 12 * B * D + ...
232ms, O(n2), #vars: 2, input, output
max(3 * B + 4, 4, (2 *...
308ms, O(n2), #vars: 2, input, output
max(B, 0) + max(0, max...
67ms, O(n2), #vars: 1, input, output

107ms, input, aspic, output, errors
c-examples/ABC/ex08
2 + 2 * B * A + 3 * A
103ms, Ω(n2), #vars: 2, input, output
15 * A + 12 * A * B + ...
196ms, O(n2), #vars: 2, input, output
max(3 * A + 4, 4, (2 *...
268ms, O(n2), #vars: 2, input, output
max(A, 0) + max(0, max...
67ms, O(n2), #vars: 1, input, output

103ms, input, aspic, output, errors
c-examples/ABC/ex09
2 + 3 * B + 2 * B * D
105ms, Ω(n2), #vars: 2, input, output
30 * B + 12 * B * D + ...
226ms, O(n2), #vars: 2, input, output
max(3 * B + 4, 4, (2 *...
305ms, O(n2), #vars: 2, input, output
max(B, 0) + max(0, max...
69ms, O(n2), #vars: 1, input, output

93ms, input, aspic, output, errors
c-examples/ABC/ex10
2 + 2 * B * A + 3 * A
97ms, Ω(n2), #vars: 2, input, output
30 * A + 12 * A * B + ...
204ms, O(n2), #vars: 2, input, output
max(3 * A + 4, 4, (2 *...
276ms, O(n2), #vars: 2, input, output
max(A, 0) + max(0, max...
66ms, O(n2), #vars: 1, input, output

91ms, input, aspic, output, errors
c-examples/ABC/ex11
2 + 2 * B * A + 3 * A
100ms, Ω(n2), #vars: 2, input, output
15 * A + 12 * A * B + ...
196ms, O(n2), #vars: 2, input, output
max(3 * A + 4, 4, (2 *...
274ms, O(n2), #vars: 2, input, output
max(A, 0) + max(0, max...
66ms, O(n2), #vars: 1, input, output

101ms, input, aspic, output, errors
c-examples/ABC/ex12
2 + 5 * A
91ms, Ω(n), #vars: 1, input, output
18 * A + 24 * A * B + ...
203ms, O(n2), #vars: 2, input, output
max(5 * A + 4, 4)
224ms, O(n), #vars: 1, input, output
1 + max(A, 0)
68ms, O(n), #vars: 1, input, output

90ms, input, aspic, output, errors
c-examples/ABC/ex13
-5 - 7 * B + 2 * (1 + ...
1147ms, Ω(n3), #vars: 3, input, output
2537 * A + 2537 * B + ...
527ms, O(n4), #vars: 4, input, output
max(-3 * A + 3 * B + 7...
1279ms, O(n3), #vars: 4, input, output
max(0, max(0, max(0, D...
127ms, O(n3), #vars: 2, input, output

195ms, input, aspic, output, errors
c-examples/ABC/ex14
2 + 1 / 3 * B^3 * A + ...
200ms, Ω(n4), #vars: 2, input, output
7871239044 * A + 11971...
521ms, O(n8), #vars: 2, input, output
max(3 * A + 4, 4, A * ...
1089ms, O(n4), #vars: 2, input, output
max(A, 0) + max(0, max...
174ms, O(n4), #vars: 1, input, output

199ms, input, aspic, output, errors
c-examples/ABC/ex15
6 + 6 * B
193ms, Ω(n), #vars: 1, input, output

4045ms, input, output

1198ms, input, output

218ms, input, output

269ms, input, aspic, output, errors
c-examples/Loopus/Example1
1 + 3 * B
157ms, Ω(n), #vars: 1, input, output
80 * B + 34
870ms, O(n), #vars: 1, input, output
max(8 * B + 1, 3 * B +...
768ms, O(n), #vars: 1, input, output
max(0, -2 + max(B, 0))...
147ms, O(n), #vars: 1, input, output

150ms, input, aspic, output, errors
c-examples/Loopus/Example2
1
2062ms, Ω(1), #vars: 0, input, output

13381ms, input, output
max(3 / 2 * A + 25 / 2...
7854ms, O(n), #vars: 1, input, output

302ms, input, output

1226ms, input, aspic, output, errors
c-examples/Loopus/Example3
677
156ms, Ω(1), #vars: 0, input, output
18 * A * B + 4590 * B ...
770ms, O(n2), #vars: 2, input, output
max(3 * A + 4, 4, -3 *...
343ms, O(n), #vars: 1, input, output
max(0, max(A, 0) + max...
179ms, O(n), #vars: 1, input, output

86ms, input, aspic, output, errors
c-examples/Rank/ex1
10 + 8 * B
227ms, Ω(n), #vars: 1, input, output
70944 * B + 36720 * B^...
4054ms, O(n2), #vars: 1, input, output
max(4, 6 * B + max(max...
730ms, O(n2), #vars: 1, input, output

686ms, input, output

184ms, input, aspic, output, errors
c-examples/Rank/ex2
2 + 7 * meter
137ms, Ω(n), #vars: 1, input, output
36 * B + 16
967ms, O(n), #vars: 1, input, output
max(4, 9 / 2 * B + 3 /...
435ms, O(n2), #vars: 1, input, output
max(0, B + -1) + max(0...
90ms, O(n), #vars: 1, input, output

138ms, input, aspic, output, errors
c-examples/Rank/ex3
4 + 5 * meter
186ms, Ω(n), #vars: 1, input, output
52 * B + 30
1351ms, O(n), #vars: 1, input, output
max(25 / 4 * B + 11 / ...
520ms, O(n), #vars: 1, input, output
max(0, B + -1) + max(0...
92ms, O(n), #vars: 1, input, output

248ms, input, aspic, output, errors
c-examples/SPEED/CAV09/ex1
2 + 3 * C
160ms, Ω(n), #vars: 1, input, output
6 * C + 602
514ms, O(n), #vars: 1, input, output
max(3 * C + 304, 304)
266ms, O(n), #vars: 1, input, output
100 + max(C, 0) + max(...
74ms, O(n), #vars: 1, input, output

101ms, input, aspic, output, errors
c-examples/SPEED/CAV09/ex2
-1 + 3 * C + 3 * (-1 +...
276ms, Ω(n2), #vars: 2, input, output
12 * C + 18 * D + 18 *...
474ms, O(n2), #vars: 2, input, output
max(4, max(0, D * C + ...
263ms, O(n2), #vars: 2, input, output
max(C, 0) + max(0, max...
70ms, O(n2), #vars: 1, input, output

101ms, input, aspic, output, errors
c-examples/SPEED/CAV09/ex3
4 + 3 * B
124ms, Ω(n), #vars: 1, input, output
90 * B + 5
3922ms, O(n), #vars: 1, input, output
max(8 * B + 5, 5, 3 * ...
644ms, O(n), #vars: 1, input, output
max(B, 0) + max(B, 0) ...
268ms, O(n), #vars: 1, input, output

148ms, input, aspic, output, errors
c-examples/SPEED/PLDI09/Example2
1
200ms, Ω(1), #vars: 0, input, output
42 * A + 23
428ms, O(n), #vars: 1, input, output
max(8 * A, 5)
290ms, O(n), #vars: 1, input, output

281ms, input, output

110ms, input, aspic, output, errors
c-examples/SPEED/PLDI09/Example3
-2 + 4 * (-1 + B) * A ...
287ms, Ω(n2), #vars: 2, input, output
500 * A + 300 * B + 50...
574ms, O(n2), #vars: 2, input, output
max(5, max(0, min(B * ...
503ms, O(n2), #vars: 2, input, output
max(B, 0) + max(0, max...
73ms, O(n2), #vars: 1, input, output

163ms, input, aspic, output, errors
c-examples/SPEED/PLDI09/Example4
1
155ms, Ω(1), #vars: 0, input, output
32 * B^2 + 32 * A * B ...
1274ms, O(n2), #vars: 2, input, output

247ms, input, output

156ms, input, output

126ms, input, aspic, output, errors
c-examples/SPEED/PLDI09/Example5
2 + 3 * B - 3 * A
199ms, Ω(n), #vars: 2, input, output
36 * B^2 + 54 * A * B ...
543ms, O(n2), #vars: 2, input, output
max(-3 * A + 3 * B + 4...
362ms, O(n), #vars: 2, input, output
max(A, 0) + max(A, 0) ...
103ms, O(n), #vars: 2, input, output

122ms, input, aspic, output, errors
c-examples/SPEED/PLDI09/Example6
5 + G
147ms, Ω(n), #vars: 1, input, output
28 * D + 7 * G + 27
2435ms, O(n), #vars: 2, input, output
max(4, max(0, D + G) +...
664ms, O(n2), #vars: 1, input, output
max(G, 0) + max(G, 0) ...
147ms, O(n), #vars: 1, input, output

182ms, input, aspic, output, errors
c-examples/SPEED/PLDI09/NestedLoop
7 + 3 * C
526ms, Ω(n), #vars: 1, input, output
236 * A + 8 * C + 352 ...
1766ms, O(n2), #vars: 3, input, output
max(4 * A + 4, 5, max(...
4460ms, O(n2), #vars: 3, input, output
max(C, 0) + max(C, 0) ...
554ms, O(n2), #vars: 2, input, output

192ms, input, aspic, output
c-examples/SPEED/PLDI09/cyclic
2 + 3 * B - 3 * A
368ms, Ω(n), #vars: 2, input, output

2867ms, input, output
max(-3 * A + 3 * B + 8...
762ms, O(n), #vars: 2, input, output

125ms, input, output

135ms, input, aspic, output, errors
c-examples/SPEED/PLDI10/Ex1
-1 + 2 * (-1 + A) * A ...
242ms, Ω(n2), #vars: 1, input, output

5565ms, input, output
max(8, 2 * A + -4 + (2...
427ms, O(n2), #vars: 1, input, output
max(A, 0) + max(0, max...
117ms, O(n3), #vars: 1, input, output

126ms, input, aspic, output, errors
c-examples/SPEED/PLDI10/Ex2
INF
76ms, INF, #vars: 1, input, output

5971ms, input, output

483ms, input, output

138ms, input, output

131ms, input, aspic, output, errors
c-examples/SPEED/PLDI10/Ex3
4 + 3 * A
127ms, Ω(n), #vars: 1, input, output

3273ms, input, output

458ms, input, output

260ms, input, output

84ms, input, aspic, output, errors
c-examples/SPEED/PLDI10/Ex4
3 + 3 * A
122ms, Ω(n), #vars: 1, input, output
90 * A + 69
736ms, O(n), #vars: 1, input, output
max(6 * A + 5, 7, 3 * ...
611ms, O(n), #vars: 1, input, output

431ms, input, output

109ms, input, aspic, output, errors
c-examples/SPEED/PLDI10/Ex5
INF
153ms, INF, #vars: 1, input, output

5008ms, input, output

499ms, input, output

124ms, input, output

148ms, input, aspic, output, errors
c-examples/SPEED/PLDI10/Ex6
5 - 3 * B + 3 * A
202ms, Ω(n), #vars: 2, input, output
15 * A + 12 * B + 27 *...
362ms, O(n), #vars: 3, input, output
max(4, -3 * A + 3 * C ...
227ms, O(n), #vars: 2, input, output
max(0, max(0, A + 1 + ...
114ms, O(n2), #vars: 2, input, output

183ms, input, aspic, output, errors
c-examples/SPEED/PLDI10/Ex7
2 + 2 * B - 2 * A
368ms, Ω(n), #vars: 2, input, output

1464ms, input, output
max(-2 * A + 2 * B + 4...
513ms, O(n), #vars: 2, input, output

165ms, input, output

97ms, input, aspic, output, errors
c-examples/SPEED/POPL09/Dis1
2 - 3 * C + 3 * D
311ms, Ω(n), #vars: 2, input, output
6 * A + 6 * B + 6 * C ...
426ms, O(n), #vars: 4, input, output
max(-3 * A + 3 * B + -...
295ms, O(n), #vars: 4, input, output
max(0, D - C) + max(0,...
82ms, O(n), #vars: 2, input, output

87ms, input, aspic, output, errors
c-examples/SPEED/POPL09/Dis2
5 - 3 * C + 3 * A
206ms, Ω(n), #vars: 2, input, output
18 * A + 34 * B + 16 *...
368ms, O(n), #vars: 3, input, output
max(4, -3 * A + 3 * B ...
234ms, O(n), #vars: 2, input, output
max(0, max(0, A + 1 + ...
116ms, O(n2), #vars: 2, input, output

77ms, input, aspic, output, errors
c-examples/SPEED/POPL09/NestedMultiple
3 - 3 * C + 3 * D
283ms, Ω(n), #vars: 2, input, output

3567ms, input, output
max(-3 * A + 3 * B + -...
759ms, O(n), #vars: 4, input, output
max(0, D - C) + max(0,...
77ms, O(n), #vars: 2, input, output

153ms, input, aspic, output, errors
c-examples/SPEED/POPL09/NestedMultipleDep
2 + 2 * E * B + 3 * B
103ms, Ω(n2), #vars: 2, input, output
25 * B + 20 * B * E + 4
662ms, O(n2), #vars: 2, input, output
max(3 * B + 4, 4, (2 *...
347ms, O(n2), #vars: 2, input, output
max(B, 0) + max(0, max...
66ms, O(n2), #vars: 1, input, output

81ms, input, aspic, output, errors
c-examples/SPEED/POPL09/NestedSingle
3 + 3 * B
134ms, Ω(n), #vars: 1, input, output
48 * B + 16
4200ms, O(n), #vars: 1, input, output
max(7 * B + 4, 3 * B +...
625ms, O(n), #vars: 1, input, output
max(B, 0) + max(B, 0) ...
89ms, O(n), #vars: 1, input, output

106ms, input, aspic, output, errors
c-examples/SPEED/POPL09/SequentialSingle
2 + 3 * B
111ms, Ω(n), #vars: 1, input, output
21 * B + 6
213ms, O(n), #vars: 1, input, output
max(3 * B + 6, 2 * B +...
258ms, O(n), #vars: 1, input, output
max(B, 0) + max(B, 0)
50ms, O(n), #vars: 1, input, output

113ms, input, aspic, output, errors
c-examples/SPEED/POPL09/SimpleMultiple
2 + 3 * D
160ms, Ω(n), #vars: 1, input, output
6 * C + 6 * D + 8
464ms, O(n), #vars: 2, input, output
max(3 * C + 3 * D + 4,...
321ms, O(n), #vars: 2, input, output
max(C, 0) + max(D, 0) ...
81ms, O(n), #vars: 1, input, output

85ms, input, aspic, output, errors
c-examples/SPEED/POPL09/SimpleMultipleDep
-1 + 3 * C + 3 * (-1 +...
262ms, Ω(n2), #vars: 2, input, output
12 * C + 18 * D + 18 *...
495ms, O(n2), #vars: 2, input, output
max(4, max(0, D * C + ...
261ms, O(n2), #vars: 2, input, output
max(C, 0) + max(0, max...
72ms, O(n2), #vars: 1, input, output

111ms, input, aspic, output, errors
c-examples/SPEED/POPL09/SimpleSingle
2 + 2 * B
72ms, Ω(n), #vars: 1, input, output
4 * B + 6
99ms, O(n), #vars: 1, input, output
max(2 * B + 4, 4)
191ms, O(n), #vars: 1, input, output
max(B, 0)
46ms, O(n), #vars: 1, input, output

83ms, input, aspic, output, errors
c-examples/SPEED/POPL09/SimpleSingle2
2 + 3 * C
159ms, Ω(n), #vars: 1, input, output
20 * D + 12 * C + 17
295ms, O(n), #vars: 2, input, output
max(-1 * C + 4 * D + 6...
1060ms, O(n), #vars: 2, input, output
max(D, 0) + max(C, 0)
51ms, O(n), #vars: 1, input, output

113ms, input, aspic, output, errors
c-examples/WTC/aaron2
1
117ms, Ω(1), #vars: 0, input, output
35 * A + 28 * B + 28 *...
306ms, O(n), #vars: 3, input, output
max(3 * B + -3 * C + 7...
294ms, O(n), #vars: 2, input, output
max(0, max(0, B + 1 + ...
192ms, O(n2), #vars: 2, input, output

110ms, input, aspic, output, errors
c-examples/WTC/ax
2 * C * (-2 + C) + C
108ms, Ω(n2), #vars: 1, input, output
23 * C + 12 * C^2 + 14
201ms, O(n2), #vars: 1, input, output
max(2 * C + 2, 8, 2 * ...
416ms, O(n2), #vars: 1, input, output
max(0, C + -2) + max(0...
74ms, O(n2), #vars: 1, input, output

117ms, input, aspic, output, errors
c-examples/WTC/complex
8
601ms, Ω(1), #vars: 0, input, output

60011ms, input
max(4, max(0, min(-1 /...
37503ms, O(n2), #vars: 2, input, output

171ms, input, output

177ms, input, aspic, output, errors
c-examples/WTC/counterex1b
18 + 6 * (1 + A) * F +...
187ms, Ω(n2), #vars: 2, input, output

5180ms, input, output

1592ms, input, output

404ms, input, output

212ms, input, aspic, output, errors
c-examples/WTC/cousot9
2 + 3 * free
243ms, INF, #vars: 1, input, output

2661ms, input, output

243ms, input, output

66ms, input, output

135ms, input, aspic, output, errors
c-examples/WTC/easy1
1
97ms, Ω(1), #vars: 0, input, output
830
207ms, O(1), #vars: 0, input, output
124
250ms, O(1), #vars: 0, input, output
40
76ms, O(1), #vars: 0, input, output

93ms, input, aspic, output, errors
c-examples/WTC/easy2
2 + 2 * A
67ms, Ω(n), #vars: 1, input, output
4 * A + 6
94ms, O(n), #vars: 1, input, output
max(2 * A + 4, 4)
184ms, O(n), #vars: 1, input, output
max(A, 0)
44ms, O(n), #vars: 1, input, output

78ms, input, aspic, output, errors
c-examples/WTC/exmini
1
90ms, Ω(1), #vars: 0, input, output
2 * A + 2 * B + 2 * C ...
139ms, O(n), #vars: 3, input, output
max(-1 * A + B + -1 * ...
322ms, O(n), #vars: 3, input, output
max(0, B + 1 + 0 - C)
55ms, O(n), #vars: 2, input, output

111ms, input, aspic, output, errors
c-examples/WTC/gcd
1
129ms, Ω(1), #vars: 0, input, output

3385ms, input, output
max(3 * A + 3 * B + -2...
266ms, O(n), #vars: 2, input, output

59ms, input, output

121ms, input, aspic, output, errors
c-examples/WTC/insertsort
-7 / 2 + 3 / 2 * (-1 +...
131ms, Ω(n2), #vars: 1, input, output
172748 * B + 384 * B^2...
293ms, O(n2), #vars: 1, input, output
max(5, max(5 * B + -10...
464ms, O(n2), #vars: 1, input, output
max(0, B + -1) + max(0...
141ms, O(n2), #vars: 1, input, output

125ms, input, aspic, output, errors
c-examples/WTC/loops
8
217ms, Ω(1), #vars: 0, input, output
126 * A + 24 * A^2 + 107
752ms, O(n2), #vars: 1, input, output
max(3 * A + 7, 3, (2 *...
278ms, O(n2), #vars: 1, input, output
max(0, A + 1) + max(0,...
91ms, O(n2), #vars: 1, input, output

106ms, input, aspic, output, errors
c-examples/WTC/nd_loop
1
130ms, Ω(1), #vars: 0, input, output
15
85ms, O(1), #vars: 0, input, output
13
239ms, O(1), #vars: 0, input, output
1
45ms, O(1), #vars: 0, input, output
8
84ms, O(1), #vars: 0, input, aspic, output
c-examples/WTC/ndecr
-2 + 2 * A
69ms, Ω(n), #vars: 1, input, output
4 * A + 6
87ms, O(n), #vars: 1, input, output
max(2 * A, 4)
181ms, O(n), #vars: 1, input, output
max(0, A + -2)
46ms, O(n), #vars: 1, input, output

82ms, input, aspic, output, errors
c-examples/WTC/nestedLoop
8 + 2 * C
266ms, Ω(n), #vars: 1, input, output

60014ms, input
max(6 * A + -4 * C + 4...
1239ms, O(n2), #vars: 3, input, output
max(C, 0) + max(C, 0) ...
110ms, O(n2), #vars: 2, input, output

332ms, input, aspic, output, errors
c-examples/WTC/perfect
3 + 5 * meter
629ms, Ω(n), #vars: 1, input, output
39 * A + 12 * A^2 + 36
1049ms, O(n2), #vars: 1, input, output
max(3, max((2 * A + 1)...
449ms, O(n2), #vars: 1, input, output

274ms, input, output

143ms, input, aspic, output, errors
c-examples/WTC/random1d
2 + 2 * A
67ms, Ω(n), #vars: 1, input, output
12 * A + 13
155ms, O(n), #vars: 1, input, output
max(2 * A + 4, 3)
205ms, O(n), #vars: 1, input, output
max(A, 0)
55ms, O(n), #vars: 1, input, output
max(5, 2 + 1 + A__o' +...
102ms, O(n), #vars: 1, input, aspic, output
c-examples/WTC/random2d
2 + 2 * B
139ms, Ω(n), #vars: 1, input, output
216 * B + 139
811ms, O(n), #vars: 1, input, output
max(7 * B + 4, 4)
317ms, O(n), #vars: 1, input, output
max(B, 0)
67ms, O(n), #vars: 1, input, output

489ms, input, aspic, output, errors
c-examples/WTC/realbubble
-4 + 2 * (-1 + A)^2 + ...
206ms, Ω(n2), #vars: 1, input, output
212212 * A + 1248 * A^...
336ms, O(n2), #vars: 1, input, output
max(4 * A + 2, 4, (A +...
482ms, O(n2), #vars: 1, input, output
max(0, A + -1) + max(0...
101ms, O(n2), #vars: 1, input, output

179ms, input, aspic, output, errors
c-examples/WTC/realheapsort
1
8504ms, Ω(1), #vars: 0, input, output
891990781 * A + 759980...
2235ms, O(n4), #vars: 1, input, output

1005ms, input, output

685ms, input, output

307ms, input, aspic, output
c-examples/WTC/realheapsort_step1
1
8646ms, Ω(1), #vars: 0, input, output
216 * A^2 + 86139 * A ...
755ms, O(n2), #vars: 1, input, output
max(4, max(4 * A + -8,...
469ms, O(n2), #vars: 1, input, output

296ms, input, output

681ms, input, aspic, output, errors
c-examples/WTC/realheapsort_step2
-24 + 9 * A
872ms, Ω(n), #vars: 1, input, output
924 * A + 240 * A^2 + 888
1206ms, O(n2), #vars: 1, input, output

589ms, input, output

117ms, input, output

326ms, input, aspic, output, errors
c-examples/WTC/realselect
-1 - (-1 + B)^2 + 3 * ...
98ms, Ω(n2), #vars: 1, input, output
132 * B + 72 * B^2 + 64
643ms, O(n2), #vars: 1, input, output
max(4, (2 * B + 2) * (...
269ms, O(n2), #vars: 1, input, output
max(0, B + -1) + max(0...
88ms, O(n2), #vars: 1, input, output

112ms, input, aspic, output, errors
c-examples/WTC/realshellsort
1
988ms, Ω(1), #vars: 0, input, output
78 * A + 330 * A^2 + 2...
1061ms, O(n3), #vars: 1, input, output

1465ms, input, output

234ms, input, output

266ms, input, aspic, output, errors
c-examples/WTC/rsd
6 + 3 * A
127ms, Ω(n), #vars: 1, input, output
81 * A + 72 * A^2 + 30
1011ms, O(n2), #vars: 1, input, output
max(3, 3 * A + 3 + max...
316ms, O(n2), #vars: 1, input, output

144ms, input, output

110ms, input, aspic, output, errors
c-examples/WTC/sipma91
2 + 2 * meter
109ms, Ω(n), #vars: 1, input, output
27608 * A + 135 * A^2 ...
1106ms, O(n2), #vars: 1, input, output
max(79 / 11, -2 / 11 *...
382ms, O(n), #vars: 1, input, output
max(0, 9 * max(0, 101 ...
152ms, O(n), #vars: 1, input, output

201ms, input, aspic, output
c-examples/WTC/sipmabubble
2 + 3 / 2 * A^2 + 9 / ...
237ms, Ω(n2), #vars: 1, input, output
255 * A + 120 * A^2 + 139
546ms, O(n2), #vars: 1, input, output
max(7, (4 * A + 3) * A...
264ms, O(n2), #vars: 1, input, output
max(0, A + 1) + max(0,...
98ms, O(n2), #vars: 1, input, output

122ms, input, aspic, output, errors
c-examples/WTC/speedFails4
1
131ms, Ω(1), #vars: 0, input, output

3332ms, input, output

297ms, input, output

116ms, input, output

121ms, input, aspic, output, errors
c-examples/WTC/speedpldi2
1
192ms, Ω(1), #vars: 0, input, output
28 * A + 10
386ms, O(n), #vars: 1, input, output
max(6 * A + 1, 4)
249ms, O(n), #vars: 1, input, output

82ms, input, output

114ms, input, aspic, output, errors
c-examples/WTC/speedpldi3
-1 + 3 * (-1 + B) * A ...
292ms, Ω(n2), #vars: 2, input, output
6 * B + 225 * A + 30 *...
476ms, O(n2), #vars: 2, input, output
max(3, max(0, min(B * ...
349ms, O(n2), #vars: 2, input, output
max(B, 0) + max(0, max...
48ms, O(n2), #vars: 1, input, output

120ms, input, aspic, output, errors
c-examples/WTC/speedpldi4
1
143ms, Ω(1), #vars: 0, input, output
15 * B + 6
399ms, O(n), #vars: 1, input, output
max(-3 * A + 3 * B + 7...
271ms, O(n), #vars: 2, input, output

50ms, input, output
max(3 + 1 + B__o' + B_...
120ms, O(n), #vars: 2, input, aspic, output
c-examples/WTC/terminate
1
83ms, Ω(1), #vars: 0, input, output
2 * A + 2 * B + 2 * C ...
132ms, O(n), #vars: 3, input, output
max(-1 * A + B + -1 * ...
310ms, O(n), #vars: 3, input, output
max(0, B + 1 + 0 - C)
54ms, O(n), #vars: 2, input, output

90ms, input, aspic, output, errors
c-examples/WTC/wcet1
-2 + 4 * A
627ms, Ω(n), #vars: 1, input, output
44 * A + 26
370ms, O(n), #vars: 1, input, output
max(4 * A + 3, 7)
406ms, O(n), #vars: 1, input, output
max(0, A + -1)
63ms, O(n), #vars: 1, input, output
max(2 + A__o' + 1 + A_...
146ms, O(n), #vars: 1, input, aspic, output
c-examples/WTC/wcet2
1
126ms, Ω(1), #vars: 0, input, output
123984 * A + 360 * A^2...
211ms, O(n2), #vars: 1, input, output
max(-3 * A + 59, 46, -...
450ms, O(n), #vars: 1, input, output
max(0, 10 + 10 * max(0...
119ms, O(n), #vars: 1, input, output

92ms, input, aspic, output, errors
c-examples/WTC/while2
2 + 3 * B + 2 * B^2
98ms, Ω(n2), #vars: 1, input, output
19 * B + 12 * B^2 + 9
192ms, O(n2), #vars: 1, input, output
max(4, (2 * B + 3) * B...
263ms, O(n2), #vars: 1, input, output
max(B, 0) + max(0, max...
68ms, O(n2), #vars: 1, input, output

96ms, input, aspic, output, errors
c-examples/WTC/wise
-4 - 3 * B + 3 * A
165ms, Ω(n), #vars: 2, input, output
18 * B + 18 * A + 15
455ms, O(n), #vars: 2, input, output
max(3 * A + -3 * B + -...
291ms, O(n), #vars: 2, input, output

71ms, input, output
max(3 + 1 + B__o' + A_...
175ms, O(n), #vars: 2, input, aspic, output
costa/RAML/rationalPotential
1
117ms, Ω(1), #vars: 0, input, output
A + 1
169ms, O(n), #vars: 1, input, output
max(1, max(0, min(C, A...
201ms, O(n), #vars: 3, input, output
max(B, 0)
55ms, O(n), #vars: 1, input, output

80ms, input, aspic, output, errors
costa/misc/ack
1 + B
137ms, Ω(n), #vars: 1, input, output

2394ms, input, output

205ms, input, output

63ms, input, output

79ms, input, aspic, output, errors
costa/misc/direct_n_log_n
1
150ms, Ω(1), #vars: 0, input, output
4 * A + 9
81ms, O(n), #vars: 1, input, output
max(A, 1)
192ms, O(n), #vars: 1, input, output

47ms, input, output
max(2, 1 + A__o' + 1)
69ms, O(n), #vars: 1, input, aspic, output
costa/misc/linear
1 + A
65ms, Ω(n), #vars: 1, input, output
A + 2
85ms, O(n), #vars: 1, input, output
max(A + 1, 101)
183ms, O(n), #vars: 1, input, output
max(A, 100)
50ms, O(n), #vars: 1, input, output
max(2, 1 + 1 + A__o' + 1)
79ms, O(n), #vars: 1, input, aspic, output
costa/misc/logarithmic
nonlinear
1
145ms, Ω(1), #vars: 0, input, output
3
44ms, O(1), #vars: 0, input, output
1
168ms, O(1), #vars: 0, input, output
1
56ms, O(1), #vars: 0, input, output
Non-linear example not handled by prover.
costa/misc/merge
1 + A
158ms, Ω(n), #vars: 1, input, output
2 * A + 2 * B + 3
138ms, O(n), #vars: 2, input, output
max(A + B, 1)
208ms, O(n), #vars: 2, input, output
max(B, 0) + max(A, 0) ...
68ms, O(n), #vars: 1, input, output

84ms, input, aspic, output, errors
costa/misc/mspe
1
2061ms, Ω(1), #vars: 0, input, output
4 * B + 4 * F + 5
205ms, O(n), #vars: 2, input, output
max(-1 * A + B + 2, 1)
4269ms, O(n), #vars: 2, input, output

502ms, input, output
max(2, 1 + 2 + -1 * F_...
25241ms, O(n), #vars: 2, input, aspic, output