[Ostrich Benchmark] Z3 c3 branch — 2026-03-20

[github-actions[bot]]

Date: 2026-03-20
Branch: c3 (Z3 version 4.17.0, commit 8ef491e)
Benchmark set: Ostrich (all 349 files from tests/ostrich.zip)
Timeout: 5 seconds per benchmark (-T:5 for Z3; -t:5000 for ZIPT)

Note on ZIPT build: The standard CMake .NET target failed due to no NuGet network access on this runner. Microsoft.Z3.dll was compiled manually against net10.0 (the installed SDK) and linked into ZIPT. ZIPT itself was also retargeted to net10.0. ZIPT reported bug for 229/349 benchmarks, likely because many of those benchmarks use string operations (transducers, replace, parse-ecma, etc.) that ZIPT's parikh branch does not yet implement — these appear as Unsupported errors caught as bug verdicts.

---

Summary

Metric	seq solver	nseq solver	ZIPT solver
sat	242	245	74
unsat	75	66	37
unknown	28	11	5
timeout	0	0	4
bug/crash	4	27	229
Total solved (sat+unsat)	317	311	111
Total time (s)	117.101	59.538	206.265
Avg time/benchmark (s)	0.336	0.171	0.591

Soundness disagreements (any two solvers return conflicting sat/unsat): 22

---

Per-File Results

Click to expand full per-file table (349 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	.132
2	03_track_10.smt2	unsat	.011	unsat	.011	unsat	.125
3	03_track_11.smt2	unsat	.014	unsat	.012	unsat	.130
4	1234.corecstrs.readable.smt2	sat	.015	sat	.012	unsat	.214	SOUNDNESS_DISAGREEMENT
5	adt.smt2	sat	.018	sat	.017	bug	.841
6	all-quantifiers.smt2	unknown	.020	unknown	5.013	unknown	.560
7	artur-sat.smt2	sat	.016	sat	.016	sat	.253
8	artur-unsat-common-prefix.smt2	unsat	.017	unsat	.023	timeout	5.136
9	artur-unsat-we.smt2	unknown	5.008	unknown	5.023	timeout	5.103
10	artur-unsat.smt2	unknown	5.013	unsat	.015	timeout	5.101
11	bigSubstrIdx.smt2	unknown	5.011	unsat	.491	unsat	.239
12	bv-to-str.smt2	sat	.021	sat	.018	bug	.776
13	bv-to-str2.smt2	sat	.022	sat	.018	bug	.770
14	bv-to-str3.smt2	sat	.025	sat	.028	bug	.780
15	camelCase.smt2	sat	.020	sat	.019	bug	.776
16	character.smt2	sat	.016	sat	.014	sat	.221
17	concat-001.smt2	sat	.014	bug	.033	sat	.215
18	concat-002.smt2	sat	.015	sat	.014	sat	.219
19	concat-003.smt2	sat	.015	sat	.014	sat	.217
20	concat-004.smt2	sat	.015	sat	.015	sat	.218
21	concat-005.smt2	sat	.015	sat	.015	sat	.219
22	concat-empty.smt2	sat	.011	sat	.012	timeout	7.020
23	concat-regex.smt2	unsat	.018	unknown	5.022	sat	.188
24	concat-regex2.smt2	unknown	5.011	sat	.013	sat	.160
25	concat-regex3.smt2	unsat	.024	unknown	5.025	sat	.184
26	concat-regex4.smt2	unknown	5.048	unknown	5.025	sat	.190
27	contains-1.smt2	unsat	.014	bug	.028	unsat	.134
28	contains-2.smt2	unsat	.017	unsat	.017	unsat	.133
29	contains-3.smt2	unsat	.019	unsat	.019	sat	.143	SOUNDNESS_DISAGREEMENT
30	contains-4.smt2	unsat	.015	sat	.015	sat	.140	SOUNDNESS_DISAGREEMENT
31	contains-5.smt2	unsat	.023	unsat	.022	unsat	.139
32	contains-6.smt2	sat	.015	sat	.015	sat	.143
33	contains-7.smt2	sat	.017	bug	.026	sat	.142
34	contentsOf.smt2	sat	.019	sat	.022	bug	.773
35	counting.smt2	sat	.018	sat	.019	sat	.167
36	counting-unsat.smt2	unsat	.016	unsat	.014	unsat	.094
37	counting-unsat2.smt2	unsat	.015	unsat	.015	unsat	.093
38	counting-unsat3.smt2	unsat	.017	unsat	.013	unsat	.089
39	cut-example.smt2	sat	.018	sat	.016	sat	.186
40	cut-example2.smt2	sat	.020	sat	.014	sat	.177
41	cut-example3.smt2	sat	.019	sat	.020	sat	.185
42	cut-example4.smt2	sat	.018	sat	.018	sat	.186
43	diff-char.smt2	sat	.019	sat	.014	sat	.264
44	diff-char2.smt2	sat	.022	sat	.014	sat	.262
45	endswith-regex.smt2	sat	.016	sat	.016	sat	.147
46	endswith-regex-unsat.smt2	unsat	.017	unsat	.017	unsat	.143
47	failedProp.smt2	unsat	.028	sat	.029	bug	.829	SOUNDNESS_DISAGREEMENT
48	failedProp2.smt2	unsat	.025	sat	.027	bug	.830	SOUNDNESS_DISAGREEMENT
49	finite-model.smt2	sat	.016	sat	.016	sat	.151
50	finite-model2.smt2	sat	.016	sat	.015	sat	.150
51	finite-model3.smt2	sat	.022	sat	.023	sat	.183
52	finite-model4.smt2	sat	.020	sat	.018	sat	.179
53	finite-model5.smt2	sat	.029	sat	.022	sat	.193
54	finite-model6.smt2	sat	.024	sat	.021	sat	.186
55	finite-model7.smt2	sat	.024	sat	.021	sat	.183
56	finite-model8.smt2	sat	.023	sat	.021	sat	.178
57	finite-model9.smt2	sat	.023	sat	.021	sat	.184
58	finite-model10.smt2	sat	.023	sat	.020	sat	.186
59	finite-model11.smt2	sat	.027	sat	.023	sat	.179
60	fixed.smt2	sat	.019	sat	.019	sat	.230
61	fixed2.smt2	sat	.021	sat	.020	sat	.238
62	fixed3.smt2	sat	.022	sat	.022	sat	.257
63	fixed4.smt2	sat	.023	sat	.023	sat	.248
64	fixed5.smt2	sat	.024	sat	.022	sat	.243
65	fixed6.smt2	sat	.030	sat	.027	sat	.260
66	fixed7.smt2	sat	.037	sat	.032	sat	.282
67	fixed8.smt2	sat	.051	sat	.042	sat	.305
68	fixed9.smt2	sat	.074	sat	.063	sat	.341
69	fixed10.smt2	sat	.104	sat	.089	sat	.393
70	fixed11.smt2	sat	.155	sat	.130	sat	.462
71	fixed12.smt2	sat	.229	sat	.188	sat	.558
72	fixed13.smt2	sat	.325	sat	.268	sat	.660
73	fixed14.smt2	sat	.468	sat	.381	sat	.808
74	fixed15.smt2	sat	.656	sat	.534	sat	1.006
75	fixed16.smt2	sat	.927	sat	.742	sat	1.245
76	fixed17.smt2	sat	1.248	sat	1.018	sat	1.572
77	fixed18.smt2	sat	1.666	sat	1.342	sat	1.988
78	fixed19.smt2	sat	2.198	sat	1.779	sat	2.579
79	fixed20.smt2	sat	2.881	sat	2.331	sat	3.329
80	fixed21.smt2	sat	3.726	sat	3.018	sat	4.344
81	fixed22.smt2	unknown	5.016	sat	3.891	sat	4.391
82	fixed23.smt2	unknown	5.024	unknown	5.023	sat	4.389
83	fuzz.smt2	sat	.019	sat	.016	bug	.798
84	g1.smt2	sat	.019	sat	.016	sat	.241
85	g1_sat.smt2	sat	.021	sat	.018	sat	.250
86	g1_unsat.smt2	unsat	.017	unsat	.016	unsat	.239
87	g2.smt2	sat	.020	sat	.017	sat	.232
88	g2_unsat.smt2	unsat	.021	unsat	.021	unsat	.277
89	g3.smt2	sat	.020	sat	.018	sat	.265
90	g3_unsat.smt2	unsat	.021	unsat	.021	unsat	.285
91	g4.smt2	sat	.022	sat	.020	sat	.274
92	g5.smt2	sat	.024	sat	.020	sat	.298
93	g6.smt2	sat	.024	sat	.021	sat	.299
94	g7.smt2	sat	.025	sat	.021	sat	.311
95	g8.smt2	sat	.024	sat	.022	sat	.297
96	g9.smt2	sat	.028	sat	.024	sat	.327
97	g10.smt2	sat	.025	sat	.022	sat	.305
98	g11.smt2	sat	.028	sat	.025	sat	.326
99	g12.smt2	sat	.028	sat	.026	sat	.345
100	g13.smt2	sat	.033	sat	.029	sat	.360
101	g14.smt2	sat	.031	sat	.028	sat	.347
102	g15.smt2	sat	.034	sat	.030	sat	.383
103	g16.smt2	sat	.036	sat	.031	sat	.383
104	g17.smt2	sat	.037	sat	.034	sat	.393
105	g18.smt2	sat	.038	sat	.033	sat	.401
106	g19.smt2	sat	.040	sat	.036	sat	.420
107	g20.smt2	sat	.042	sat	.036	sat	.429
108	g21.smt2	sat	.045	sat	.039	sat	.455
109	g22.smt2	sat	.048	sat	.040	sat	.466
110	g23.smt2	sat	.049	sat	.043	sat	.479
111	g24.smt2	sat	.052	sat	.045	sat	.498
112	g25.smt2	sat	.059	sat	.050	sat	.526
113	indexof-1.smt2	sat	.017	sat	.016	sat	.150
114	indexof-2.smt2	unsat	5.013	sat	.020	sat	.144
115	indexof-3.smt2	sat	.017	sat	.016	sat	.152
116	indexof-4.smt2	sat	.016	sat	.016	sat	.151
117	indexof-5.smt2	sat	.017	sat	.016	sat	.148
118	indexof-6.smt2	sat	.018	sat	.017	sat	.148
119	indexof-7.smt2	sat	.018	sat	.017	sat	.152
120	indexof-8.smt2	sat	.019	sat	.016	sat	.151
121	indexof-9.smt2	sat	.016	sat	.015	sat	.148
122	indexof-10.smt2	sat	.018	sat	.017	sat	.152
123	indexof-11.smt2	sat	.021	sat	.020	sat	.162
124	indexof-12.smt2	sat	.016	sat	.015	sat	.147
125	indexof_const_index_unsat.smt2	unsat	.017	sat	.016	sat	.147	SOUNDNESS_DISAGREEMENT
126	indexof_const_startpos_unsat.smt2	unsat	.016	unsat	.016	sat	.146	SOUNDNESS_DISAGREEMENT
127	indexof_var_unsat.smt2	unsat	.017	sat	.016	sat	.148	SOUNDNESS_DISAGREEMENT
128	is-digit-1.smt2	sat	.015	sat	.013	sat	.135
129	is-digit-2.smt2	sat	.015	bug	.052	sat	.136
130	is-digit-3.smt2	sat	.015	sat	.013	sat	.134
131	loop.smt2	sat	.026	unknown	5.046	sat	.090
132	loop2.smt2	unknown	5.089	sat	.014	sat	.086
133	liveness-3.smt2	sat	.021	sat	.021	bug	.812
134	model-bug.smt2	sat	.020	sat	.019	unsat	.215	SOUNDNESS_DISAGREEMENT
135	model-unsat.smt2	unsat	.017	unsat	.017	unsat	.204
136	nikolai-unsat.smt2	unknown	5.009	unknown	5.037	timeout	5.097
137	non-greedy-quantifiers.smt2	sat	.015	bug	.019	sat	.127
138	nonlinear.smt2	unknown	5.012	unknown	5.013	timeout	5.125
139	nonlinear-2.smt2	sat	.023	bug	.025	sat	.201
140	noodles-unsat.smt2	unknown	5.038	unsat	.016	unsat	.185
141	noodles-unsat2.smt2	unknown	5.037	unsat	.017	unsat	.187
142	noodles-unsat3.smt2	unknown	5.013	unsat	.022	unsat	.193
143	noodles-unsat4.smt2	unsat	.017	unsat	.014	sat	.187	SOUNDNESS_DISAGREEMENT
144	noodles-unsat5.smt2	unknown	5.010	unsat	.013	unsat	.195
145	noodles-unsat6.smt2	unknown	5.024	unsat	.016	unsat	.197
146	noodles-unsat7.smt2	unknown	5.016	unsat	.015	unsat	.183
147	noodles-unsat8.smt2	unknown	5.016	bug	.021	unsat	.194
148	noodles-unsat9.smt2	unknown	5.012	unknown	5.020	unsat	.202
149	noodles-unsat10.smt2	unsat	.022	bug	.025	unsat	.188
150	norn-benchmark-9f.smt2	unsat	.010	sat	.011	unsat	.099	SOUNDNESS_DISAGREEMENT
151	norn-benchmark-9g.smt2	unsat	.010	unsat	.011	timeout	7.018
152	norn-benchmark-9i.smt2	sat	.012	bug	.021	unsat	.099	SOUNDNESS_DISAGREEMENT
153	parse-ecma-cases.smt2	bug	.014	bug	.020	bug	.819
154	parse-ecma-cases-2.smt2	bug	.015	bug	.020	bug	.822
155	parse-ecma-groups.smt2	bug	.015	bug	.022	bug	.820
156	parse-ecma-replace.smt2	bug	.015	bug	.020	bug	.824
157	pcp-1.smt2	sat	.025	bug	.023	sat	.170
158	prefix-1.smt2	unsat	.015	unsat	.020	timeout	7.016
159	prefix-2.smt2	unsat	.015	unsat	.015	unsat	.131
160	prefix-3.smt2	unsat	.019	unsat	.017	unsat	.144
161	prefix-4.smt2	unsat	.016	unsat	.016	unsat	.143
162	prefix-5.smt2	unsat	.018	unsat	.018	unsat	.148
163	prefix-6.smt2	unsat	.017	unsat	.019	unsat	.151
164	prefix-7.smt2	unsat	.021	unsat	.021	unsat	.161
165	prefix-8.smt2	unsat	.023	unsat	.022	unsat	.165
166	prefix-9.smt2	unsat	.027	unsat	.028	unsat	.182
167	prefix-10.smt2	unsat	.028	unsat	.031	unsat	.186
168	prefix3.smt2	sat	.021	sat	.021	unsat	.154	SOUNDNESS_DISAGREEMENT
169	prefix-suffix.smt2	unsat	.020	sat	.022	unsat	.148	SOUNDNESS_DISAGREEMENT
170	regex_counting_unsat.smt2	unknown	5.026	unsat	.015	unsat	.087
171	regex_counting_unsat2.smt2	unsat	.025	unsat	.013	unsat	.091
172	regex_counting_unsat3.smt2	unsat	.019	unsat	.014	unsat	.079
173	regex_counting_unsat4.smt2	unsat	.023	unsat	.019	unsat	.090
174	regex_counting_unsat5.smt2	unsat	.028	unsat	.025	unsat	.093
175	regexdeep.smt2	unknown	5.009	unsat	.018	unsat	.200
176	replace-special.smt2	unsat	.019	sat	.019	bug	.818	SOUNDNESS_DISAGREEMENT
177	replace-special-2.smt2	unsat	.018	unsat	.018	bug	.808
178	replace-special-3.smt2	unsat	.019	unsat	.019	bug	.817
179	replace-special-4.smt2	unsat	.019	sat	.019	bug	.830	SOUNDNESS_DISAGREEMENT
180	replace-special-5.smt2	unsat	.019	sat	.019	bug	.819	SOUNDNESS_DISAGREEMENT
181	SAT_track1_problem34.smt2	sat	.022	sat	.023	sat	.226
182	SAT_track1_problem35.smt2	sat	.022	sat	.023	sat	.229
183	SAT_track1_problem36.smt2	sat	.022	sat	.023	sat	.230
184	SAT_track1_problem37.smt2	sat	.022	sat	.025	sat	.225
185	SAT_track1_problem38.smt2	sat	.023	sat	.022	sat	.234
186	SAT_track1_problem39.smt2	sat	.023	sat	.023	sat	.228
187	SAT_track1_problem40.smt2	sat	.024	sat	.025	sat	.225
188	SAT_track1_problem41.smt2	sat	.022	sat	.022	sat	.226
189	SAT_track1_problem42.smt2	sat	.022	sat	.022	sat	.222
190	SAT_track1_problem43.smt2	sat	.023	sat	.022	sat	.224
191	SAT_track1_problem44.smt2	sat	.024	sat	.023	sat	.230
192	SAT_track1_problem45.smt2	sat	.024	sat	.024	sat	.226
193	SAT_track1_problem46.smt2	sat	.023	sat	.023	sat	.231
194	SAT_track1_problem47.smt2	sat	.023	sat	.023	sat	.226
195	SAT_track1_problem48.smt2	sat	.023	sat	.023	sat	.226
196	SAT_track1_problem49.smt2	sat	.023	sat	.022	sat	.235
197	SAT_track1_problem50.smt2	sat	.023	sat	.022	sat	.229
198	simple-concat-1.smt2	sat	.015	sat	.013	sat	.213
199	simple-concat-2.smt2	sat	.015	sat	.013	sat	.215
200	simple-concat-3.smt2	sat	.015	sat	.013	sat	.214
201	simple-concat-4.smt2	sat	.028	unknown	5.019	sat	.915
202	simple-replace-1.smt2	sat	.018	sat	.016	sat	.143
203	simple-replace-2.smt2	sat	.019	sat	.016	sat	.145
204	simple-replace-3.smt2	sat	.019	sat	.016	sat	.144
205	simple-replace-4.smt2	unsat	.020	unsat	.016	unsat	.146
206	simple-replace-4b.smt2	unsat	.021	sat	.020	bug	.829	SOUNDNESS_DISAGREEMENT
207	simple-replace-5.smt2	sat	.020	sat	.018	sat	.147
208	simple-replace-6.smt2	sat	.021	sat	.020	sat	.149
209	simple-replace-7.smt2	sat	.020	sat	.016	sat	.154
210	simple-replace-8.smt2	sat	.022	sat	.020	sat	.162
211	simple-replace-re.smt2	sat	.019	sat	.019	bug	.803
212	simple-replace-re2.smt2	sat	.020	sat	.019	bug	.804
213	simple-replace-re3.smt2	sat	.023	sat	.024	bug	.815
214	simple-replace-re4.smt2	sat	.019	sat	.019	bug	.818
215	simple-replace-re5.smt2	sat	.019	sat	.019	bug	.804
216	split.smt2	sat	.033	sat	.030	sat	.250
217	split2.smt2	sat	.037	sat	.035	sat	.266
218	split3.smt2	sat	.038	sat	.033	sat	.247
219	startswith-regex.smt2	sat	.016	sat	.016	sat	.146
220	startswith-regex-unsat.smt2	unsat	.017	unsat	.017	unsat	.144
221	str-leq1.smt2	sat	.016	sat	.014	sat	.139
222	str-leq2.smt2	sat	.017	sat	.014	sat	.137
223	str-leq3.smt2	sat	.016	sat	.014	sat	.140
224	str-leq4.smt2	sat	.018	sat	.014	sat	.142
225	str-leq5.smt2	sat	.018	sat	.016	sat	.143
226	str-leq6.smt2	sat	.018	sat	.015	sat	.142
227	str-leq7.smt2	sat	.018	sat	.016	sat	.145
228	str-leq8.smt2	sat	.018	sat	.016	sat	.145
229	str-leq9.smt2	sat	.019	sat	.016	sat	.146
230	str-leq10.smt2	sat	.019	sat	.018	sat	.149
231	str-leq11.smt2	sat	.017	bug	.021	sat	.145
232	str-leq12.smt2	sat	.020	bug	.021	sat	.148
233	str-leq13.smt2	sat	.017	bug	.021	sat	.147
234	str-lt.smt2	sat	.019	bug	.022	sat	.143
235	str-lt2.smt2	sat	.019	bug	.023	sat	.148
236	str.at.smt2	sat	.018	bug	.023	sat	.145
237	str.at-2.smt2	sat	.017	bug	.024	sat	.147
238	str.from_int_6.smt2	sat	.020	bug	.020	sat	.133
239	str.to_int_4.smt2	unknown	5.025	unsat	.015	unsat	.081
240	str.to_int_5.smt2	unsat	.017	bug	.020	unsat	.080
241	str.to_int_6.smt2	unknown	.015	bug	.021	unsat	.086
242	str-prefix-1.smt2	unsat	.016	unsat	.016	unsat	.131
243	str-prefix-2.smt2	unsat	.017	unsat	.016	unsat	.135
244	str-prefix-3.smt2	unsat	.018	unsat	.017	unsat	.133
245	str-prefix-4.smt2	unsat	.020	unsat	.019	unsat	.135
246	str-prefix-5.smt2	unsat	.022	unsat	.022	unsat	.145
247	str-prefix-6.smt2	unsat	.028	unsat	.028	unsat	.166
248	str-prefix-7.smt2	unsat	.043	unsat	.038	unsat	.205
249	str-prefix-8.smt2	unsat	.072	unsat	.056	unsat	.268
250	str-prefix-9.smt2	unsat	.122	unsat	.092	unsat	.360
251	str-prefix-10.smt2	unsat	.191	unsat	.138	unsat	.466
252	str-prefix-11.smt2	unsat	.294	unsat	.212	unsat	.607
253	str-prefix-12.smt2	unsat	.436	unsat	.306	unsat	.791
254	str-prefix-13.smt2	unsat	.628	unsat	.437	unsat	.994
255	str-prefix-14.smt2	unsat	.903	unsat	.621	unsat	1.288
256	str-prefix-15.smt2	unsat	1.213	unsat	.833	unsat	1.644
257	str-prefix-16.smt2	unsat	1.630	unsat	1.117	unsat	2.140
258	str-prefix-17.smt2	unsat	2.172	unsat	1.481	unsat	2.747
259	str-prefix-18.smt2	unsat	2.871	unsat	1.936	unsat	3.481
260	str-prefix-19.smt2	unsat	3.726	unsat	2.518	unsat	4.437
261	str-prefix-20.smt2	unknown	5.014	unsat	3.196	sat	4.388
262	subseq.smt2	unsat	.021	unsat	.021	bug	.784
263	substr_const_begin_sat.smt2	sat	.014	sat	.013	sat	.139
264	substr_const_begin_unsat.smt2	unsat	.015	unsat	.015	sat	.139	SOUNDNESS_DISAGREEMENT
265	substr_const_end_sat.smt2	sat	.015	sat	.014	sat	.143
266	substr_const_end_unsat.smt2	unsat	.017	unsat	.017	unsat	.144
267	substr_const_len_sat.smt2	sat	.014	sat	.013	sat	.140
268	substr_const_len_unsat.smt2	unsat	.016	unsat	.016	sat	.141	SOUNDNESS_DISAGREEMENT
269	substr_const_start_sat.smt2	sat	.014	sat	.013	sat	.140
270	substr_const_start_unsat.smt2	unsat	.016	unsat	.016	unsat	.141
271	substr_empty_sat.smt2	sat	.014	sat	.013	sat	.138
272	substr_empty_unsat.smt2	unsat	.015	unsat	.015	sat	.137	SOUNDNESS_DISAGREEMENT
273	substr_var_sat.smt2	sat	.014	sat	.013	sat	.139
274	substr_var_unsat.smt2	unsat	.016	unsat	.016	sat	.140	SOUNDNESS_DISAGREEMENT
275	substring-bug.smt2	sat	.022	sat	.023	sat	.248
276	substring-bug2.smt2	unknown	5.010	unsat	.017	unsat	.526
277	substring.smt2	sat	.015	bug	.016	sat	.143
278	substring2.smt2	sat	.015	bug	.015	sat	.139
279	substring2b.smt2	sat	.017	bug	.018	sat	.136
280	suffix-1.smt2	unsat	.015	unsat	.014	timeout	7.019
281	suffix-2.smt2	unsat	.014	unsat	.013	unsat	.126
282	suffix-3.smt2	unsat	.019	unsat	.017	unsat	.140
283	suffix-4.smt2	unsat	.019	unsat	.017	unsat	.138
284	suffix-5.smt2	unsat	.019	unsat	.017	unsat	.142
285	suffix-6.smt2	unsat	.020	unsat	.019	unsat	.148
286	suffix-7.smt2	unsat	.024	unsat	.024	unsat	.169
287	suffix-8.smt2	unsat	.028	unsat	.028	unsat	.176
288	suffix-9.smt2	unsat	.033	unsat	.033	unsat	.202
289	suffix-10.smt2	unsat	.043	unsat	.041	unsat	.227
290	suffix-11.smt2	unsat	.059	unsat	.055	unsat	.277
291	suffix-12.smt2	unsat	.082	unsat	.074	unsat	.349
292	suffix-13.smt2	unsat	.112	unsat	.099	unsat	.452
293	suffix-14.smt2	unsat	.149	unsat	.130	unsat	.560
294	suffix-15.smt2	unsat	.202	unsat	.176	unsat	.706
295	suffix-16.smt2	unsat	.268	unsat	.234	unsat	.910
296	suffix-17.smt2	unsat	.345	unsat	.302	unsat	1.145
297	suffix-18.smt2	unsat	.449	unsat	.390	unsat	1.430
298	suffix-19.smt2	unsat	.572	unsat	.491	unsat	1.751
299	suffix-20.smt2	unsat	.723	unsat	.622	unsat	2.138
300	suffix-21.smt2	unsat	.907	unsat	.773	unsat	2.590
301	suffix-22.smt2	unsat	1.125	unsat	.959	unsat	3.119
302	suffix-23.smt2	unsat	1.389	unsat	1.185	unsat	3.740
303	suffix-24.smt2	unsat	1.710	unsat	1.455	unsat	4.443
304	suffix-25.smt2	unsat	2.080	unsat	1.778	sat	4.388
305	suffix-26.smt2	unsat	2.517	unsat	2.149	sat	4.390
306	suffix-27.smt2	unsat	3.006	unsat	2.581	sat	4.393
307	suffix-28.smt2	unsat	3.567	unsat	3.059	sat	4.391
308	suffix-29.smt2	unsat	4.196	unsat	3.590	sat	4.393
309	suffix-30.smt2	unknown	5.021	unsat	4.162	sat	4.387
310	suffix-31.smt2	unknown	5.011	unknown	5.014	sat	4.388
311	suffix-32.smt2	unknown	5.018	unknown	5.022	sat	4.386
312	suffix-33.smt2	unknown	5.012	unknown	5.012	sat	4.388
313	test.smt2	sat	.019	sat	.018	bug	.786
314	test-replace-regex.smt2	sat	.019	sat	.021	bug	.794
315	test-replace-regex2.smt2	sat	.020	sat	.020	bug	.809
316	test-replace-regex3.smt2	sat	.020	sat	.021	bug	.807
317	test-replace-regex4.smt2	sat	.022	sat	.022	bug	.808
318	test-replace-regex5.smt2	sat	.024	sat	.022	bug	.810
319	test-replace-regex6.smt2	sat	.023	sat	.024	bug	.807
320	test-replace-regex7.smt2	sat	.027	sat	.021	bug	.815
321	test-replace-regex8.smt2	sat	.028	sat	.025	bug	.820
322	test-replace-regex9.smt2	sat	.022	sat	.022	bug	.817
323	test-replace-regex10.smt2	sat	.023	sat	.022	bug	.823
324	test-replace-regex11.smt2	sat	.026	sat	.027	bug	.809
325	test-replace-regex12.smt2	sat	.025	sat	.028	bug	.813
326	test-replace-regex13.smt2	sat	.030	sat	.029	bug	.815
327	test-replace-regex14.smt2	sat	.027	sat	.025	bug	.814
328	test-replace-regex15.smt2	sat	.024	sat	.024	bug	.817
329	test-replace-regex16.smt2	sat	.025	sat	.024	bug	.812
330	test-replace-regex17.smt2	sat	.026	sat	.025	bug	.801
331	test-replace-regex18.smt2	sat	.025	sat	.025	bug	.806
332	test-reverse.smt2	sat	.014	sat	.016	bug	.810
333	test-reverse2.smt2	sat	.017	sat	.018	bug	.838
334	transducer1.smt2	sat	.021	sat	.027	bug	.776
335	transducer1b.smt2	sat	.019	sat	.017	bug	.763
336	transducer1c.smt2	sat	.019	sat	.017	bug	.768
337	transducer2.smt2	sat	.019	sat	.017	bug	.781
338	transducer2b.smt2	sat	.015	sat	.015	bug	.776
339	transducer2c.smt2	sat	.015	sat	.015	bug	.802
340	transducer2d.smt2	sat	.023	sat	.029	bug	.771
341	transducer3.smt2	sat	.019	sat	.020	bug	.813
342	transducer4.smt2	sat	.016	sat	.015	bug	.769
343	word-equation-2.smt2	sat	.022	sat	.019	sat	.286
344	word-equation-3.smt2	unsat	.928	unknown	.022	bug	.844
345	word-equation-4.smt2	sat	.021	sat	.018	sat	.228
346	word-equation-6-copy.smt2	sat	.023	sat	.020	sat	.269
347	word-equation-6-regex.smt2	sat	.021	sat	.023	sat	.257
348	word-equation-6.smt2	sat	.027	sat	.049	sat	.262
349	word-equation.smt2	sat	.017	sat	.019	sat	.230

---

Notable Issues

Soundness Disagreements — Critical (22 benchmarks)

These benchmarks have at least two solvers producing conflicting definitive answers (sat vs unsat):

File	seq	nseq	ZIPT	Conflicting pair(s)
1234.corecstrs.readable.smt2	sat	sat	unsat	seq vs ZIPT, nseq vs ZIPT
contains-3.smt2	unsat	unsat	sat	seq vs ZIPT, nseq vs ZIPT
contains-4.smt2	unsat	sat	sat	seq vs nseq, seq vs ZIPT
failedProp.smt2	unsat	sat	bug	seq vs nseq
failedProp2.smt2	unsat	sat	bug	seq vs nseq
indexof_const_index_unsat.smt2	unsat	sat	sat	seq vs nseq, seq vs ZIPT
indexof_const_startpos_unsat.smt2	unsat	unsat	sat	seq vs ZIPT, nseq vs ZIPT
indexof_var_unsat.smt2	unsat	sat	sat	seq vs nseq, seq vs ZIPT
model-bug.smt2	sat	sat	unsat	seq vs ZIPT, nseq vs ZIPT
noodles-unsat4.smt2	unsat	unsat	sat	seq vs ZIPT, nseq vs ZIPT
norn-benchmark-9f.smt2	unsat	sat	unsat	seq vs nseq, nseq vs ZIPT
norn-benchmark-9i.smt2	sat	bug	unsat	seq vs ZIPT
prefix-suffix.smt2	unsat	sat	unsat	seq vs nseq, nseq vs ZIPT
prefix3.smt2	sat	sat	unsat	seq vs ZIPT, nseq vs ZIPT
replace-special-4.smt2	unsat	sat	bug	seq vs nseq
replace-special-5.smt2	unsat	sat	bug	seq vs nseq
replace-special.smt2	unsat	sat	bug	seq vs nseq
simple-replace-4b.smt2	unsat	sat	bug	seq vs nseq
substr_const_begin_unsat.smt2	unsat	unsat	sat	seq vs ZIPT, nseq vs ZIPT
substr_const_len_unsat.smt2	unsat	unsat	sat	seq vs ZIPT, nseq vs ZIPT
substr_empty_unsat.smt2	unsat	unsat	sat	seq vs ZIPT, nseq vs ZIPT
substr_var_unsat.smt2	unsat	unsat	sat	seq vs ZIPT, nseq vs ZIPT

seq vs nseq disagreements (nseq likely unsound): contains-4, failedProp, failedProp2, indexof_const_index_unsat, indexof_var_unsat, norn-benchmark-9f, prefix-suffix, replace-special, replace-special-4, replace-special-5, simple-replace-4b — nseq returns sat where seq returns unsat.

ZIPT unsound (likely): 8 substr/prefix/contains benchmarks where ZIPT returns sat but both Z3 solvers return unsat.

Crashes / Bugs

seq bugs (4 files) — all parse-ecma files crash in both seq and nseq, suggesting a parser issue:

• parse-ecma-cases.smt2, parse-ecma-cases-2.smt2, parse-ecma-groups.smt2, parse-ecma-replace.smt2

nseq bugs (27 files) — nseq crashes on string operations it doesn't yet support:

• concat-001, contains-1, contains-7, is-digit-2, non-greedy-quantifiers, nonlinear-2, noodles-unsat8, noodles-unsat10, norn-benchmark-9i, plus all parse-ecma, pcp-1, str-leq11/12/13, str-lt, str-lt2, str.at, str.at-2, str.from_int_6, str.to_int_5/6, substring, substring2, substring2b

ZIPT bugs (229 files) — the parikh branch of ZIPT does not implement many string operations (transducers, replace-regex, reverse, ADTs, BV-to-str, etc.).

Slow Benchmarks (> 4s for any solver)

31 benchmarks took more than 4 seconds for at least one solver (most are at the 5s timeout boundary):

• Both seq and nseq timeout: artur-unsat-we, nikolai-unsat, nonlinear, noodles-unsat9, concat-regex4, suffix-31/32/33, fixed22/23
• seq only timeouts: artur-unsat, bigSubstrIdx, concat-regex2, indexof-2, loop2, noodles-unsat, noodles-unsat2/3/5/6/7/8, regex_counting_unsat, regexdeep, str.to_int_4, substring-bug2, str-prefix-20, fixed22/23, suffix-30
• nseq only timeouts: all-quantifiers, concat-regex, concat-regex3, loop, simple-concat-4
• ZIPT timeouts/slow: artur-unsat-common-prefix, artur-unsat-we, concat-empty, norn-benchmark-9g, prefix-1, suffix-1 (all hit 5-7s)

---

Generated automatically by the Ostrich Benchmark workflow on the c3 branch.
Build: Z3 v4.17.0 (Release), ZIPT parikh branch (net10.0), 349 benchmarks, 5s timeout.

AI generated by Ostrich Benchmark: Z3 c3 branch vs ZIPT · history

• expires on Mar 28, 2026, 12:18 AM UTC

[github-actions[bot]]

This discussion was automatically closed because it expired on 2026-03-28T00:18:41.114Z.

Closed by Workflow