You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Date: 2026-03-23 Branch: c3 (commit ced7952) Benchmark set: Ostrich — all 299 files from tests/ostrich.zip Timeout: 5 seconds per benchmark (-T:5 for Z3 seq/nseq; -t:5000 for ZIPT) Z3 version: 4.17.0 — build ced7952a7b51a8a8079b6469710326549d558dca ZIPT: built from parikh branch of CEisenhofer/ZIPT against Z3 .NET bindings (net8.0)
Summary
Metric
seq solver
nseq solver
ZIPT solver
sat
200
205
73
unsat
75
65
37
unknown
24
24
9
timeout
0
0
0
bug/crash
0
5
180
Total time (s)
106.115
117.509
176.134
Avg time/benchmark (s)
0.355
0.393
0.589
Soundness disagreements (any two solvers return conflicting sat/unsat): 22
Note on ZIPT bugs: ZIPT reported bug/crash on 180 benchmarks (60%). Inspection shows ZIPT does not support several Z3 string operations used in this benchmark set (transducers, str.replace_re, str.to_int, str.from_int, str.indexof, str.substr with complex arguments, quantifiers, ADT sorts, etc.). These are counted as crashes/unsupported rather than sound verdicts.
Per-File Results
Click to expand full per-file table (299 benchmarks)
#
File
seq verdict
seq time (s)
nseq verdict
nseq time (s)
ZIPT verdict
ZIPT time (s)
Notes
1
03_track_1.smt2
unsat
.011
unsat
.010
unsat
.139
2
03_track_10.smt2
unsat
.010
unsat
.010
unsat
.142
3
03_track_11.smt2
unsat
.014
unsat
.012
unsat
.148
4
1234.corecstrs.readable.smt2
sat
.011
sat
.011
unsat
.153
SOUNDNESS_DISAGREEMENT
5
adt.smt2
sat
.013
sat
.012
bug
.690
6
adt2.smt2
sat
.013
sat
.013
bug
.540
7
all-quantifiers.smt2
unsat
.020
unknown
5.012
bug
.614
8
artur-unsat-common-prefix.smt2
unsat
.013
unsat
.016
unknown
5.119
9
artur-unsat-we.smt2
unknown
5.009
unknown
5.020
unknown
5.110
10
artur-unsat.smt2
unknown
5.013
sat
.015
unknown
5.109
11
bigSubstrIdx.smt2
unknown
5.011
unsat
.473
unsat
.256
12
brackets-regex.smt2
sat
.011
sat
.011
bug
.539
13
bug-56-replace-bug2.smt2
sat
.014
sat
.016
bug
.115
14
bug-58-replace-re.smt2
unknown
.012
sat
.014
bug
.115
15
chars.smt2
sat
.013
sat
.011
bug
.567
16
chars2.smt2
sat
.013
sat
.013
bug
.706
17
chars3.smt2
sat
.018
sat
.025
bug
.803
18
concat-001.smt2
sat
.024
bug
.020
sat
.299
19
concat-002.smt2
sat
.016
sat
.063
sat
.291
20
concat-003.smt2
sat
.014
sat
.015
sat
.250
21
concat-004-unsat.smt2
unsat
.016
unsat
.015
unsat
.228
22
concat-005-unsat.smt2
unsat
.015
unsat
.013
unsat
.160
23
concat-006.smt2
sat
.014
sat
.012
sat
.238
24
concat-007.smt2
sat
.015
sat
.014
sat
.228
25
concat-008.smt2
sat
.015
sat
.013
sat
.232
26
concat-009.smt2
sat
.014
sat
.013
sat
.225
27
concat-010.smt2
sat
.013
sat
.012
sat
.228
28
concat-011.smt2
sat
.013
sat
.013
sat
.241
29
concat-012.smt2
sat
.013
sat
.013
sat
.234
30
concat-013.smt2
sat
.013
sat
.013
sat
.231
31
concat-014.smt2
sat
.014
sat
.012
sat
.225
32
concat-015.smt2
sat
.016
sat
.014
sat
.236
33
concat-016.smt2
sat
.013
sat
.014
sat
.235
34
concat-017.smt2
sat
.015
sat
.013
sat
.237
35
concat-018.smt2
sat
.014
sat
.014
sat
.231
36
concat-019.smt2
sat
.015
sat
.013
sat
.226
37
concat-020.smt2
sat
.015
sat
.013
sat
.229
38
concat-021.smt2
sat
.016
sat
.016
sat
.243
39
concat-022.smt2
sat
.017
sat
.015
sat
.232
40
concat-023.smt2
sat
.015
sat
.014
sat
.229
41
concat-024.smt2
sat
.015
sat
.018
sat
.231
42
concat-025.smt2
sat
.020
sat
.014
sat
.237
43
concat-026.smt2
sat
.017
sat
.016
sat
.232
44
concat-027.smt2
sat
.023
sat
.015
sat
.236
45
concat-028.smt2
sat
.016
sat
.015
sat
.229
46
concat-029.smt2
sat
.015
sat
.014
sat
.235
47
concat-030.smt2
sat
.014
sat
.015
sat
.229
48
concat-031.smt2
sat
.013
sat
.014
sat
.233
49
concat-032.smt2
sat
.015
sat
.016
sat
.231
50
concat-033.smt2
sat
.013
sat
.015
sat
.228
51
concat-034.smt2
sat
.013
sat
.015
sat
.234
52
concat-035.smt2
sat
.014
sat
.015
sat
.228
53
concat-036.smt2
sat
.018
sat
.014
sat
.225
54
concat-037.smt2
sat
.013
sat
.015
sat
.229
55
concat-038.smt2
sat
.014
sat
.014
sat
.229
56
concat-039.smt2
sat
.016
sat
.013
sat
.226
57
concat-040.smt2
sat
.013
sat
.013
sat
.225
58
concat-041.smt2
sat
.013
sat
.013
sat
.241
59
concat-042.smt2
sat
.014
sat
.014
sat
.225
60
concat-043.smt2
sat
.014
sat
.013
sat
.225
61
concat-044.smt2
sat
.014
sat
.015
sat
.229
62
concat-045.smt2
sat
.013
sat
.015
sat
.224
63
concat-046.smt2
sat
.014
sat
.013
sat
.225
64
concat-047.smt2
sat
.013
sat
.013
sat
.226
65
concat-048.smt2
sat
.014
sat
.013
sat
.225
66
concat-049.smt2
sat
.014
sat
.014
sat
.228
67
concat-050.smt2
sat
.013
sat
.013
sat
.230
68
concat-051.smt2
sat
.014
sat
.013
sat
.228
69
concat-052.smt2
sat
.014
sat
.016
sat
.229
70
concat-053.smt2
sat
.014
sat
.013
sat
.224
71
concat-054.smt2
sat
.013
sat
.013
sat
.229
72
concat-055.smt2
sat
.014
sat
.013
sat
.227
73
concat-056.smt2
sat
.014
sat
.013
sat
.230
74
concat-057.smt2
sat
.013
sat
.014
sat
.230
75
concat-058.smt2
sat
.016
sat
.014
sat
.229
76
concat-059.smt2
sat
.014
sat
.015
sat
.227
77
concat-060.smt2
sat
.014
sat
.013
sat
.228
78
concat-061.smt2
sat
.013
sat
.013
sat
.225
79
concat-062.smt2
sat
.013
sat
.014
sat
.229
80
concat-063.smt2
sat
.015
sat
.013
sat
.237
81
concat-064.smt2
sat
.016
sat
.013
sat
.232
82
concat-065.smt2
sat
.015
sat
.013
sat
.236
83
concat-066.smt2
sat
.013
sat
.013
sat
.234
84
concat-067.smt2
sat
.013
sat
.014
sat
.229
85
concat-068.smt2
sat
.013
sat
.013
sat
.233
86
concat-069.smt2
sat
.014
sat
.014
sat
.232
87
concat-070.smt2
sat
.014
sat
.013
sat
.225
88
concat-071.smt2
sat
.013
sat
.013
sat
.228
89
concat-072.smt2
sat
.014
sat
.014
sat
.231
90
concat-073.smt2
sat
.013
sat
.013
sat
.231
91
concat-074.smt2
sat
.015
sat
.014
sat
.228
92
concat-075.smt2
sat
.014
sat
.015
sat
.230
93
concat-076.smt2
sat
.013
sat
.013
sat
.228
94
concat-077.smt2
sat
.014
sat
.013
sat
.230
95
concat-078.smt2
sat
.013
sat
.013
sat
.231
96
concat-079.smt2
sat
.013
sat
.013
sat
.226
97
concat-080.smt2
sat
.014
sat
.013
sat
.226
98
concat-081.smt2
sat
.014
sat
.014
sat
.227
99
concat-082.smt2
sat
.013
sat
.013
sat
.231
100
concat-083.smt2
sat
.013
sat
.013
sat
.229
101
concat-084.smt2
sat
.014
sat
.013
sat
.230
102
concat-085.smt2
sat
.014
sat
.013
sat
.225
103
concat-086.smt2
sat
.014
sat
.013
sat
.227
104
concat-087.smt2
sat
.014
sat
.013
sat
.226
105
concat-088.smt2
sat
.014
sat
.015
sat
.229
106
concat-089.smt2
sat
.015
sat
.014
sat
.229
107
concat-090.smt2
sat
.013
sat
.014
sat
.226
108
concat-091.smt2
sat
.013
sat
.014
sat
.226
109
concat-092.smt2
sat
.014
sat
.013
sat
.228
110
concat-093.smt2
sat
.014
sat
.013
sat
.230
111
concat-094.smt2
sat
.014
sat
.014
sat
.227
112
concat-095.smt2
sat
.016
sat
.015
sat
.226
113
concat-096.smt2
sat
.014
sat
.014
sat
.226
114
concat-097.smt2
sat
.014
sat
.014
sat
.225
115
concat-098.smt2
sat
.014
sat
.014
sat
.228
116
concat-099.smt2
sat
.013
sat
.013
sat
.225
117
concat-100.smt2
sat
.015
sat
.013
sat
.229
118
concat-empty.smt2
unsat
.010
unsat
.011
unknown
7.017
119
concat-regex.smt2
sat
.017
unknown
5.022
sat
.202
120
concat-regex2.smt2
unknown
5.011
sat
.013
sat
.184
121
concat-regex3.smt2
sat
.025
unknown
5.023
sat
.205
122
concat-regex4.smt2
unknown
5.050
unknown
5.025
sat
.201
123
contains-1.smt2
sat
.017
unknown
5.008
sat
.128
124
contains-2.smt2
sat
.014
sat
.015
sat
.136
125
contains-3.smt2
unsat
.011
unsat
.012
sat
.145
SOUNDNESS_DISAGREEMENT
126
contains-4.smt2
unsat
.012
sat
.013
sat
.137
SOUNDNESS_DISAGREEMENT
127
failedProp.smt2
unsat
.012
sat
.012
bug
.106
SOUNDNESS_DISAGREEMENT
128
failedProp2.smt2
unsat
.012
sat
.013
bug
.106
SOUNDNESS_DISAGREEMENT
129
indexof-1.smt2
sat
.016
sat
.016
sat
.154
130
indexof-2.smt2
unknown
5.011
sat
.015
sat
.149
131
indexof_const_index_unsat.smt2
unsat
.014
sat
.013
sat
.131
SOUNDNESS_DISAGREEMENT
132
indexof_const_startpos_unsat.smt2
unsat
.013
unsat
.013
sat
.128
SOUNDNESS_DISAGREEMENT
133
indexof_var_unsat.smt2
unsat
.013
sat
.013
sat
.124
SOUNDNESS_DISAGREEMENT
134
is-digit-1.smt2
sat
.015
sat
.014
sat
.508
135
is-digit-2.smt2
sat
.034
unknown
5.007
sat
.538
136
is-digit-3.smt2
sat
.014
sat
.015
sat
.519
137
model-bug.smt2
sat
.011
sat
.012
unsat
.140
SOUNDNESS_DISAGREEMENT
138
nikolai-unsat.smt2
unknown
5.008
unknown
5.040
unknown
5.105
139
nonlinear-2.smt2
sat
.019
bug
.020
sat
.290
140
nonlinear.smt2
unknown
5.009
unknown
5.012
unknown
5.134
141
noodles-unsat.smt2
unknown
5.038
unsat
.018
unsat
.195
142
noodles-unsat10.smt2
unsat
.044
bug
.021
unsat
.218
143
noodles-unsat2.smt2
unknown
5.036
unsat
.017
unsat
.195
144
noodles-unsat3.smt2
unknown
5.014
unsat
.023
unsat
.202
145
noodles-unsat4.smt2
unsat
.016
unsat
.017
sat
.194
SOUNDNESS_DISAGREEMENT
146
noodles-unsat5.smt2
unknown
5.010
unsat
.014
unsat
.204
147
noodles-unsat6.smt2
unknown
5.021
unsat
.014
unsat
.211
148
noodles-unsat7.smt2
unknown
5.015
unsat
.013
unsat
.196
149
noodles-unsat8.smt2
unknown
5.015
bug
.021
unsat
.206
150
noodles-unsat9.smt2
unknown
5.012
unknown
5.018
unsat
.208
151
norn-benchmark-9f.smt2
unsat
.012
sat
.011
unsat
.140
SOUNDNESS_DISAGREEMENT
152
norn-benchmark-9g.smt2
unsat
.011
unsat
.010
unknown
7.018
153
norn-benchmark-9i.smt2
sat
.013
unknown
5.007
unsat
.166
SOUNDNESS_DISAGREEMENT
154
prefix-1.smt2
unsat
.011
unsat
.010
unknown
7.018
155
prefix-2.smt2
unsat
.011
unsat
.011
unsat
.150
156
prefix-3.smt2
unsat
.011
unsat
.012
unsat
.145
157
prefix-suffix.smt2
unsat
.011
sat
.011
unsat
.144
SOUNDNESS_DISAGREEMENT
158
prefix3.smt2
sat
.019
sat
.017
unsat
.172
SOUNDNESS_DISAGREEMENT
159
regexdeep.smt2
unknown
5.009
sat
.018
unsat
.214
160
replace-special-4.smt2
unsat
.013
sat
.011
bug
.113
SOUNDNESS_DISAGREEMENT
161
replace-special-5.smt2
unsat
.012
sat
.012
bug
.113
SOUNDNESS_DISAGREEMENT
162
replace-special.smt2
unsat
.012
sat
.011
bug
.113
SOUNDNESS_DISAGREEMENT
163
simple-concat-4.smt2
sat
.023
unknown
5.015
sat
.714
164
simple-replace-1.smt2
sat
.020
sat
.013
sat
.175
165
simple-replace-2.smt2
sat
.017
sat
.016
sat
.172
166
simple-replace-3.smt2
sat
.013
sat
.013
sat
.172
167
simple-replace-4.smt2
unsat
.014
unsat
.013
unsat
.168
168
simple-replace-4b.smt2
unsat
.013
sat
.012
bug
.114
SOUNDNESS_DISAGREEMENT
169
simple-replace-5.smt2
sat
.019
sat
.018
sat
.177
170
str-leq.smt2
sat
.024
sat
.023
bug
.103
171
str-leq1.smt2
sat
.022
sat
.022
bug
.101
172
str-leq10.smt2
sat
.027
sat
.026
bug
.100
173
str-leq11.smt2
sat
.102
unknown
5.008
bug
.095
174
str-leq12.smt2
sat
.042
unknown
5.007
bug
.095
175
str-leq13.smt2
sat
.029
bug
.027
bug
.099
176
str-leq2.smt2
sat
.026
sat
.025
bug
.099
177
str-leq3.smt2
sat
.026
sat
.026
bug
.099
178
str-leq4.smt2
sat
.023
sat
.024
bug
.099
179
str-leq5.smt2
sat
.023
sat
.025
bug
.098
180
str-leq6.smt2
sat
.024
sat
.024
bug
.099
181
str-leq7.smt2
sat
.026
sat
.024
bug
.098
182
str-leq8.smt2
sat
.024
sat
.023
bug
.099
183
str-leq9.smt2
sat
.025
sat
.024
bug
.098
184
str-lt.smt2
sat
.041
unknown
5.007
bug
.095
185
str-lt2.smt2
sat
.066
unknown
5.007
bug
.097
186
str.at-2.smt2
sat
.034
unknown
5.008
sat
.542
187
str.at.smt2
sat
.021
unknown
5.013
sat
.546
188
str.from_int.smt2
sat
.012
sat
.013
bug
.559
189
str.from_int_2.smt2
sat
.013
sat
.014
bug
.558
190
str.from_int_3.smt2
sat
.012
sat
.014
bug
.557
191
str.from_int_4.smt2
sat
.013
sat
.014
bug
.561
192
str.from_int_5.smt2
sat
.014
sat
.015
bug
.559
193
str.from_int_6.smt2
sat
.056
unknown
5.009
bug
.558
194
str.from_int_7.smt2
sat
.013
sat
.015
bug
.557
195
str.from_int_8.smt2
sat
.013
sat
.015
bug
.567
196
str.to_int.smt2
sat
.013
sat
.014
bug
.098
197
str.to_int_2.smt2
sat
.015
sat
.020
bug
.099
198
str.to_int_3.smt2
sat
.015
sat
.017
bug
.099
199
str.to_int_4.smt2
unknown
5.027
sat
.015
bug
.098
200
str.to_int_5.smt2
sat
.253
unknown
5.007
bug
.089
201
str.to_int_6.smt2
sat
.143
unknown
5.007
bug
.095
202
str.to_int_7.smt2
sat
.016
sat
.017
bug
.098
203
str.to_int_8.smt2
sat
.018
sat
.017
bug
.097
204
str.to_int_9.smt2
sat
.013
sat
.014
bug
.099
205
substr_const_begin_unsat.smt2
unsat
.013
unsat
.013
sat
.131
SOUNDNESS_DISAGREEMENT
206
substr_const_len_unsat.smt2
unsat
.013
unsat
.013
sat
.130
SOUNDNESS_DISAGREEMENT
207
substr_empty_unsat.smt2
unsat
.011
unsat
.011
sat
.132
SOUNDNESS_DISAGREEMENT
208
substr_var_unsat.smt2
unsat
.013
unsat
.013
sat
.128
SOUNDNESS_DISAGREEMENT
209
substring-bug.smt2
sat
.012
sat
.014
sat
.547
210
substring-bug2.smt2
unknown
5.010
sat
.017
sat
.553
211
substring.smt2
sat
.018
unknown
5.007
sat
.544
212
suffix-1.smt2
unsat
.011
unsat
.010
unknown
7.019
213
test-replace.smt2
sat
.015
sat
.015
sat
.256
214
test-replace2.smt2
sat
.016
sat
.015
sat
.248
215
test-replace3.smt2
sat
.018
sat
.017
bug
.845
216
test-replace4.smt2
sat
.039
sat
.018
bug
.846
217
transducer1.smt2
sat
.033
sat
.019
bug
.746
218
transducer1b.smt2
sat
.025
sat
.017
bug
.845
219
transducer1c.smt2
sat
.021
sat
.017
bug
.840
220
transducer2.smt2
sat
.018
sat
.017
bug
.885
221
transducer2b.smt2
sat
.016
sat
.019
bug
.882
222
transducer2c.smt2
sat
.025
sat
.018
bug
.834
223
transducer2d.smt2
sat
.015
sat
.016
bug
.814
224
transducer3.smt2
sat
.024
sat
.022
bug
.833
225
transducer4.smt2
sat
.024
sat
.022
bug
.854
226
word-equation-2.smt2
sat
.021
sat
.023
sat
.220
227
word-equation-3.smt2
unsat
.940
unknown
.025
bug
.926
228
word-equation-4.smt2
sat
.020
sat
.020
sat
.261
229
word-equation-6-copy.smt2
sat
.021
sat
.020
sat
.275
230
word-equation-6-regex.smt2
sat
.024
sat
.021
sat
.284
231
word-equation-6.smt2
sat
.029
sat
.029
sat
.296
232
word-equation.smt2
sat
.016
sat
.028
sat
.240
Notable Issues
Soundness Disagreements (Critical) — 22 files
The following 22 benchmarks have at least two solvers returning conflicting sat/unsat verdicts. Cases where nseq disagrees with seq on benchmarks named *unsat* or where ZIPT disagrees may indicate soundness bugs.
1234.corecstrs.readable.smt2: seq=sat vs zipt=unsat, nseq=sat vs zipt=unsat
contains-3.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=sat
contains-4.smt2: seq=unsat vs nseq=sat, seq=unsat vs zipt=sat
failedProp.smt2: seq=unsat vs nseq=sat
failedProp2.smt2: seq=unsat vs nseq=sat
indexof_const_index_unsat.smt2: seq=unsat vs nseq=sat, seq=unsat vs zipt=sat
indexof_const_startpos_unsat.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=sat
indexof_var_unsat.smt2: seq=unsat vs nseq=sat, seq=unsat vs zipt=sat
model-bug.smt2: seq=sat vs zipt=unsat, nseq=sat vs zipt=unsat
noodles-unsat4.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=sat
norn-benchmark-9f.smt2: seq=unsat vs nseq=sat, nseq=sat vs zipt=unsat
norn-benchmark-9i.smt2: seq=sat vs zipt=unsat
prefix-suffix.smt2: seq=unsat vs nseq=sat, nseq=sat vs zipt=unsat
prefix3.smt2: seq=sat vs zipt=unsat, nseq=sat vs zipt=unsat
replace-special-4.smt2: seq=unsat vs nseq=sat
replace-special-5.smt2: seq=unsat vs nseq=sat
replace-special.smt2: seq=unsat vs nseq=sat
simple-replace-4b.smt2: seq=unsat vs nseq=sat
substr_const_begin_unsat.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=sat
substr_const_len_unsat.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=sat
substr_empty_unsat.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=sat
substr_var_unsat.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=sat
reacted with thumbs up emoji reacted with thumbs down emoji reacted with laugh emoji reacted with hooray emoji reacted with confused emoji reacted with heart emoji reacted with rocket emoji reacted with eyes emoji
Uh oh!
There was an error while loading. Please reload this page.
-
Ostrich Benchmark Report — Z3 c3 branch
Date: 2026-03-23
Branch: c3 (commit
ced7952)Benchmark set: Ostrich — all 299 files from
tests/ostrich.zipTimeout: 5 seconds per benchmark (
-T:5for Z3 seq/nseq;-t:5000for ZIPT)Z3 version: 4.17.0 — build
ced7952a7b51a8a8079b6469710326549d558dcaZIPT: built from
parikhbranch of CEisenhofer/ZIPT against Z3 .NET bindings (net8.0)Summary
Soundness disagreements (any two solvers return conflicting sat/unsat): 22
Per-File Results
Click to expand full per-file table (299 benchmarks)
03_track_1.smt203_track_10.smt203_track_11.smt21234.corecstrs.readable.smt2adt.smt2adt2.smt2all-quantifiers.smt2artur-unsat-common-prefix.smt2artur-unsat-we.smt2artur-unsat.smt2bigSubstrIdx.smt2brackets-regex.smt2bug-56-replace-bug2.smt2bug-58-replace-re.smt2chars.smt2chars2.smt2chars3.smt2concat-001.smt2concat-002.smt2concat-003.smt2concat-004-unsat.smt2concat-005-unsat.smt2concat-006.smt2concat-007.smt2concat-008.smt2concat-009.smt2concat-010.smt2concat-011.smt2concat-012.smt2concat-013.smt2concat-014.smt2concat-015.smt2concat-016.smt2concat-017.smt2concat-018.smt2concat-019.smt2concat-020.smt2concat-021.smt2concat-022.smt2concat-023.smt2concat-024.smt2concat-025.smt2concat-026.smt2concat-027.smt2concat-028.smt2concat-029.smt2concat-030.smt2concat-031.smt2concat-032.smt2concat-033.smt2concat-034.smt2concat-035.smt2concat-036.smt2concat-037.smt2concat-038.smt2concat-039.smt2concat-040.smt2concat-041.smt2concat-042.smt2concat-043.smt2concat-044.smt2concat-045.smt2concat-046.smt2concat-047.smt2concat-048.smt2concat-049.smt2concat-050.smt2concat-051.smt2concat-052.smt2concat-053.smt2concat-054.smt2concat-055.smt2concat-056.smt2concat-057.smt2concat-058.smt2concat-059.smt2concat-060.smt2concat-061.smt2concat-062.smt2concat-063.smt2concat-064.smt2concat-065.smt2concat-066.smt2concat-067.smt2concat-068.smt2concat-069.smt2concat-070.smt2concat-071.smt2concat-072.smt2concat-073.smt2concat-074.smt2concat-075.smt2concat-076.smt2concat-077.smt2concat-078.smt2concat-079.smt2concat-080.smt2concat-081.smt2concat-082.smt2concat-083.smt2concat-084.smt2concat-085.smt2concat-086.smt2concat-087.smt2concat-088.smt2concat-089.smt2concat-090.smt2concat-091.smt2concat-092.smt2concat-093.smt2concat-094.smt2concat-095.smt2concat-096.smt2concat-097.smt2concat-098.smt2concat-099.smt2concat-100.smt2concat-empty.smt2concat-regex.smt2concat-regex2.smt2concat-regex3.smt2concat-regex4.smt2contains-1.smt2contains-2.smt2contains-3.smt2contains-4.smt2failedProp.smt2failedProp2.smt2indexof-1.smt2indexof-2.smt2indexof_const_index_unsat.smt2indexof_const_startpos_unsat.smt2indexof_var_unsat.smt2is-digit-1.smt2is-digit-2.smt2is-digit-3.smt2model-bug.smt2nikolai-unsat.smt2nonlinear-2.smt2nonlinear.smt2noodles-unsat.smt2noodles-unsat10.smt2noodles-unsat2.smt2noodles-unsat3.smt2noodles-unsat4.smt2noodles-unsat5.smt2noodles-unsat6.smt2noodles-unsat7.smt2noodles-unsat8.smt2noodles-unsat9.smt2norn-benchmark-9f.smt2norn-benchmark-9g.smt2norn-benchmark-9i.smt2prefix-1.smt2prefix-2.smt2prefix-3.smt2prefix-suffix.smt2prefix3.smt2regexdeep.smt2replace-special-4.smt2replace-special-5.smt2replace-special.smt2simple-concat-4.smt2simple-replace-1.smt2simple-replace-2.smt2simple-replace-3.smt2simple-replace-4.smt2simple-replace-4b.smt2simple-replace-5.smt2str-leq.smt2str-leq1.smt2str-leq10.smt2str-leq11.smt2str-leq12.smt2str-leq13.smt2str-leq2.smt2str-leq3.smt2str-leq4.smt2str-leq5.smt2str-leq6.smt2str-leq7.smt2str-leq8.smt2str-leq9.smt2str-lt.smt2str-lt2.smt2str.at-2.smt2str.at.smt2str.from_int.smt2str.from_int_2.smt2str.from_int_3.smt2str.from_int_4.smt2str.from_int_5.smt2str.from_int_6.smt2str.from_int_7.smt2str.from_int_8.smt2str.to_int.smt2str.to_int_2.smt2str.to_int_3.smt2str.to_int_4.smt2str.to_int_5.smt2str.to_int_6.smt2str.to_int_7.smt2str.to_int_8.smt2str.to_int_9.smt2substr_const_begin_unsat.smt2substr_const_len_unsat.smt2substr_empty_unsat.smt2substr_var_unsat.smt2substring-bug.smt2substring-bug2.smt2substring.smt2suffix-1.smt2test-replace.smt2test-replace2.smt2test-replace3.smt2test-replace4.smt2transducer1.smt2transducer1b.smt2transducer1c.smt2transducer2.smt2transducer2b.smt2transducer2c.smt2transducer2d.smt2transducer3.smt2transducer4.smt2word-equation-2.smt2word-equation-3.smt2word-equation-4.smt2word-equation-6-copy.smt2word-equation-6-regex.smt2word-equation-6.smt2word-equation.smt2Notable Issues
Soundness Disagreements (Critical) — 22 files
The following 22 benchmarks have at least two solvers returning conflicting sat/unsat verdicts. Cases where nseq disagrees with seq on benchmarks named
*unsat*or where ZIPT disagrees may indicate soundness bugs.1234.corecstrs.readable.smt2: seq=sat vs zipt=unsat, nseq=sat vs zipt=unsatcontains-3.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=satcontains-4.smt2: seq=unsat vs nseq=sat, seq=unsat vs zipt=satfailedProp.smt2: seq=unsat vs nseq=satfailedProp2.smt2: seq=unsat vs nseq=satindexof_const_index_unsat.smt2: seq=unsat vs nseq=sat, seq=unsat vs zipt=satindexof_const_startpos_unsat.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=satindexof_var_unsat.smt2: seq=unsat vs nseq=sat, seq=unsat vs zipt=satmodel-bug.smt2: seq=sat vs zipt=unsat, nseq=sat vs zipt=unsatnoodles-unsat4.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=satnorn-benchmark-9f.smt2: seq=unsat vs nseq=sat, nseq=sat vs zipt=unsatnorn-benchmark-9i.smt2: seq=sat vs zipt=unsatprefix-suffix.smt2: seq=unsat vs nseq=sat, nseq=sat vs zipt=unsatprefix3.smt2: seq=sat vs zipt=unsat, nseq=sat vs zipt=unsatreplace-special-4.smt2: seq=unsat vs nseq=satreplace-special-5.smt2: seq=unsat vs nseq=satreplace-special.smt2: seq=unsat vs nseq=satsimple-replace-4b.smt2: seq=unsat vs nseq=satsubstr_const_begin_unsat.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=satsubstr_const_len_unsat.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=satsubstr_empty_unsat.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=satsubstr_var_unsat.smt2: seq=unsat vs zipt=sat, nseq=unsat vs zipt=satCrashes / Bugs
concat-001.smt2(nseq)nonlinear-2.smt2(nseq)noodles-unsat10.smt2(nseq)noodles-unsat8.smt2(nseq)str-leq13.smt2(nseq)Slow Benchmarks (> 4s) — 41 files
all-quantifiers.smt2: nseq=5.012s(unknown)artur-unsat-common-prefix.smt2: zipt=5.119s(unknown)artur-unsat-we.smt2: seq=5.009s(unknown), nseq=5.020s(unknown), zipt=5.110s(unknown)artur-unsat.smt2: seq=5.013s(unknown), zipt=5.109s(unknown)bigSubstrIdx.smt2: seq=5.011s(unknown)concat-empty.smt2: zipt=7.017s(unknown)concat-regex.smt2: nseq=5.022s(unknown)concat-regex2.smt2: seq=5.011s(unknown)concat-regex3.smt2: nseq=5.023s(unknown)concat-regex4.smt2: seq=5.050s(unknown), nseq=5.025s(unknown)contains-1.smt2: nseq=5.008s(unknown)indexof-2.smt2: seq=5.011s(unknown)is-digit-2.smt2: nseq=5.007s(unknown)nikolai-unsat.smt2: seq=5.008s(unknown), nseq=5.040s(unknown), zipt=5.105s(unknown)nonlinear.smt2: seq=5.009s(unknown), nseq=5.012s(unknown), zipt=5.134s(unknown)noodles-unsat.smt2: seq=5.038s(unknown)noodles-unsat2.smt2: seq=5.036s(unknown)noodles-unsat3.smt2: seq=5.014s(unknown)noodles-unsat5.smt2: seq=5.010s(unknown)noodles-unsat6.smt2: seq=5.021s(unknown)noodles-unsat7.smt2: seq=5.015s(unknown)noodles-unsat8.smt2: seq=5.015s(unknown)noodles-unsat9.smt2: seq=5.012s(unknown), nseq=5.018s(unknown)norn-benchmark-9g.smt2: zipt=7.018s(unknown)norn-benchmark-9i.smt2: nseq=5.007s(unknown)prefix-1.smt2: zipt=7.018s(unknown)regexdeep.smt2: seq=5.009s(unknown)simple-concat-4.smt2: nseq=5.015s(unknown)str-leq11.smt2: nseq=5.008s(unknown)str-leq12.smt2: nseq=5.007s(unknown)str-lt.smt2: nseq=5.007s(unknown)str-lt2.smt2: nseq=5.007s(unknown)str.at-2.smt2: nseq=5.008s(unknown)str.at.smt2: nseq=5.013s(unknown)str.from_int_6.smt2: nseq=5.009s(unknown)str.to_int_4.smt2: seq=5.027s(unknown)str.to_int_5.smt2: nseq=5.007s(unknown)str.to_int_6.smt2: nseq=5.007s(unknown)substring-bug2.smt2: seq=5.010s(unknown)substring.smt2: nseq=5.007s(unknown)suffix-1.smt2: zipt=7.019s(unknown)Generated automatically by the Ostrich Benchmark workflow on the c3 branch.
Beta Was this translation helpful? Give feedback.
All reactions