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

[github-actions[bot]]

Ostrich Benchmark Report — Z3 c3 branch

Date: 2026-03-27
Branch: c3 (commit ebd35bc)
Benchmark set: Ostrich (all files from tests/ostrich.zip)
Total benchmarks: 299
Timeout: 5 seconds per benchmark (-T:5 for Z3; -t:5000 for ZIPT)

---

Summary

Metric	seq solver	nseq solver	ZIPT solver
sat	199	224	73
unsat	75	64	37
unknown	25	9	9
timeout	0	0	0
bug/crash	0	2	180
Total time (s)	109.738	51.978	178.991
Avg time/benchmark (s)	0.367	0.174	0.599

Note on ZIPT bug count (180): The majority of ZIPT "bug/crash" results are Z3Exception: unknown constant errors indicating unsupported input features (e.g., seq-head, seq-tail, algebraic datatypes, strings_exp option, custom bitvector characters). ZIPT appears to support a narrower subset of SMT-LIB2 string theories than Z3.

Soundness disagreements (two or more solvers return conflicting sat/unsat): 25

---

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	0.010	unsat	0.010	unsat	0.142
2	03_track_10.smt2	unsat	0.010	unsat	0.009	unsat	0.134
3	03_track_11.smt2	unsat	0.014	unsat	0.012	unsat	0.138
4	1234.corecstrs.readable.smt2	sat	0.010	sat	0.010	unsat	0.145	SOUNDNESS_DISAGREEMENT
5	adt.smt2	sat	0.012	sat	0.011	bug	0.630
6	adt2.smt2	sat	0.013	sat	0.012	bug	0.556
7	all-quantifiers.smt2	unsat	0.019	unknown	5.008	bug	0.580
8	artur-unsat-common-prefix.smt2	unsat	0.016	unsat	0.018	unknown	5.141
9	artur-unsat-we.smt2	unknown	5.008	unknown	5.034	unknown	5.120
10	artur-unsat.smt2	unknown	5.012	sat	0.014	unknown	5.108
11	bigSubstrIdx.smt2	unknown	5.015	sat	0.100	unsat	0.255	SOUNDNESS_DISAGREEMENT
12	brackets-regex.smt2	sat	0.011	sat	0.010	bug	0.551
13	bug-56-replace-bug2.smt2	sat	0.013	sat	0.020	bug	0.097
14	bug-58-replace-re.smt2	unknown	0.013	sat	0.013	bug	0.124
15	chars.smt2	sat	0.011	sat	0.011	bug	0.576
16	chars2.smt2	sat	0.017	sat	0.015	bug	0.761
17	chars3.smt2	sat	0.019	sat	0.019	bug	0.821
18	concat-001.smt2	sat	0.025	sat	0.018	sat	0.279
19	concat-002.smt2	sat	0.015	sat	0.014	sat	0.238
20	concat-003.smt2	sat	0.015	sat	0.014	sat	0.238
21	concat-004-unsat.smt2	unsat	0.016	unsat	0.014	unsat	0.233
22	concat-005-unsat.smt2	unsat	0.014	unsat	0.014	unsat	0.195
23	concat-006.smt2	sat	0.013	sat	0.013	sat	0.190
24	concat-007.smt2	sat	0.011	sat	0.011	sat	0.188
25	concat-008.smt2	sat	0.011	sat	0.011	sat	0.176
26	concat-009.smt2	sat	0.011	sat	0.011	sat	0.173
27	concat-010.smt2	sat	0.011	sat	0.011	sat	0.176
28	concat-011.smt2	sat	0.011	sat	0.011	sat	0.178
29	concat-012.smt2	sat	0.011	sat	0.011	sat	0.185
30	concat-013.smt2	sat	0.013	sat	0.013	sat	0.180
31	concat-014.smt2	sat	0.012	sat	0.012	sat	0.186
32	concat-015.smt2	sat	0.012	sat	0.012	sat	0.183
33	concat-016.smt2	sat	0.012	sat	0.011	sat	0.184
34	concat-017.smt2	sat	0.011	sat	0.011	sat	0.183
35	concat-018.smt2	sat	0.012	sat	0.011	sat	0.186
36	concat-019.smt2	sat	0.012	sat	0.012	sat	0.180
37	concat-020.smt2	sat	0.011	sat	0.011	sat	0.178
38	concat-021.smt2	sat	0.011	sat	0.011	sat	0.179
39	concat-022.smt2	sat	0.011	sat	0.011	sat	0.180
40	concat-023.smt2	sat	0.011	sat	0.011	sat	0.182
41	concat-024.smt2	sat	0.011	sat	0.011	sat	0.181
42	concat-025.smt2	sat	0.011	sat	0.011	sat	0.181
43	concat-026.smt2	sat	0.011	sat	0.011	sat	0.181
44	concat-027.smt2	sat	0.011	sat	0.011	sat	0.185
45	concat-028.smt2	sat	0.011	sat	0.011	sat	0.180
46	concat-029.smt2	sat	0.011	sat	0.011	sat	0.183
47	concat-030.smt2	sat	0.011	sat	0.012	sat	0.186
48	concat-031.smt2	sat	0.011	sat	0.011	sat	0.181
49	concat-032.smt2	sat	0.011	sat	0.011	sat	0.184
50	concat-033.smt2	sat	0.012	sat	0.011	sat	0.181
51	concat-034.smt2	sat	0.011	sat	0.011	sat	0.180
52	concat-035.smt2	sat	0.011	sat	0.011	sat	0.180
53	concat-036.smt2	sat	0.011	sat	0.011	sat	0.181
54	concat-037.smt2	sat	0.011	sat	0.011	sat	0.179
55	concat-038.smt2	sat	0.011	sat	0.011	sat	0.182
56	concat-039.smt2	sat	0.011	sat	0.011	sat	0.182
57	concat-040.smt2	sat	0.011	sat	0.011	sat	0.181
58	concat-041.smt2	sat	0.011	sat	0.011	sat	0.182
59	concat-042.smt2	sat	0.011	sat	0.011	sat	0.185
60	concat-043.smt2	sat	0.011	sat	0.011	sat	0.186
61	concat-044.smt2	sat	0.011	sat	0.011	sat	0.184
62	concat-045.smt2	sat	0.011	sat	0.011	sat	0.180
63	concat-046.smt2	sat	0.011	sat	0.011	sat	0.183
64	concat-047.smt2	sat	0.011	sat	0.011	sat	0.179
65	concat-048.smt2	sat	0.011	sat	0.011	sat	0.183
66	concat-049.smt2	sat	0.011	sat	0.011	sat	0.183
67	concat-050.smt2	sat	0.011	sat	0.011	sat	0.180
68	concat-051.smt2	sat	0.011	sat	0.011	sat	0.181
69	concat-052.smt2	sat	0.011	sat	0.011	sat	0.183
70	concat-053.smt2	sat	0.011	sat	0.011	sat	0.183
71	concat-054.smt2	sat	0.011	sat	0.011	sat	0.182
72	concat-055.smt2	sat	0.011	sat	0.011	sat	0.183
73	concat-056.smt2	sat	0.011	sat	0.011	sat	0.183
74	concat-057.smt2	sat	0.011	sat	0.011	sat	0.184
75	concat-058.smt2	sat	0.011	sat	0.011	sat	0.181
76	concat-059.smt2	sat	0.011	sat	0.011	sat	0.183
77	concat-060.smt2	sat	0.011	sat	0.012	sat	0.183
78	concat-061.smt2	sat	0.011	sat	0.011	sat	0.184
79	concat-062.smt2	sat	0.011	sat	0.011	sat	0.182
80	concat-063.smt2	sat	0.011	sat	0.011	sat	0.183
81	concat-064.smt2	sat	0.011	sat	0.011	sat	0.183
82	concat-065.smt2	sat	0.011	sat	0.011	sat	0.181
83	concat-066.smt2	sat	0.011	sat	0.011	sat	0.182
84	concat-067.smt2	sat	0.011	sat	0.011	sat	0.182
85	concat-068.smt2	sat	0.011	sat	0.011	sat	0.182
86	concat-069.smt2	sat	0.011	sat	0.011	sat	0.181
87	concat-070.smt2	sat	0.011	sat	0.011	sat	0.181
88	concat-071.smt2	sat	0.011	sat	0.011	sat	0.181
89	concat-072.smt2	sat	0.011	sat	0.011	sat	0.184
90	concat-073.smt2	sat	0.011	sat	0.011	sat	0.184
91	concat-074.smt2	sat	0.011	sat	0.011	sat	0.183
92	concat-075.smt2	sat	0.011	sat	0.011	sat	0.183
93	concat-076.smt2	sat	0.011	sat	0.011	sat	0.183
94	concat-077.smt2	sat	0.011	sat	0.011	sat	0.181
95	concat-078.smt2	sat	0.011	sat	0.011	sat	0.180
96	concat-079.smt2	sat	0.011	sat	0.011	sat	0.181
97	concat-080.smt2	sat	0.011	sat	0.011	sat	0.181
98	concat-081.smt2	sat	0.011	sat	0.011	sat	0.181
99	concat-082.smt2	sat	0.011	sat	0.011	sat	0.181
100	concat-083.smt2	sat	0.011	sat	0.011	sat	0.182
101	concat-084.smt2	sat	0.011	sat	0.011	sat	0.182
102	concat-085.smt2	sat	0.011	sat	0.011	sat	0.182
103	concat-086.smt2	sat	0.011	sat	0.011	sat	0.182
104	concat-087.smt2	sat	0.011	sat	0.011	sat	0.181
105	concat-088.smt2	sat	0.011	sat	0.011	sat	0.182
106	concat-089.smt2	sat	0.011	sat	0.011	sat	0.182
107	concat-090.smt2	sat	0.011	sat	0.011	sat	0.182
108	concat-091.smt2	sat	0.011	sat	0.011	sat	0.182
109	concat-092.smt2	sat	0.011	sat	0.011	sat	0.182
110	concat-093.smt2	sat	0.011	sat	0.011	sat	0.182
111	concat-094.smt2	sat	0.011	sat	0.011	sat	0.183
112	concat-095.smt2	sat	0.011	sat	0.011	sat	0.183
113	concat-096.smt2	sat	0.011	sat	0.011	sat	0.182
114	concat-097.smt2	sat	0.011	sat	0.011	sat	0.182
115	concat-098.smt2	sat	0.011	sat	0.011	sat	0.184
116	concat-099.smt2	sat	0.011	sat	0.011	sat	0.182
117	concat-100.smt2	sat	0.011	sat	0.011	sat	0.182
118	concat-empty.smt2	sat	0.010	sat	0.009	unknown	7.017
119	concat-regex.smt2	sat	0.012	sat	0.011	sat	0.174
120	concat-regex2.smt2	unknown	5.017	sat	0.012	sat	0.169
121	concat-regex3.smt2	sat	0.013	sat	0.013	sat	0.174
122	concat-regex4.smt2	unknown	5.048	unknown	5.014	sat	0.195
123	concat.smt2	sat	0.012	sat	0.011	bug	0.576
124	contains-3.smt2	unsat	0.012	unsat	0.012	sat	0.171	SOUNDNESS_DISAGREEMENT
125	contains-4.smt2	unsat	0.012	sat	0.015	sat	0.174	SOUNDNESS_DISAGREEMENT
126	diff.smt2	sat	0.012	sat	0.011	sat	0.169
127	failedProp.smt2	unsat	0.013	sat	0.011	bug	0.086	SOUNDNESS_DISAGREEMENT
128	failedProp2.smt2	unsat	0.013	sat	0.011	bug	0.088	SOUNDNESS_DISAGREEMENT
129	indexof-2.smt2	unknown	5.018	sat	0.034	sat	0.150
130	indexof_const_index_unsat.smt2	unsat	0.012	sat	0.012	sat	0.150	SOUNDNESS_DISAGREEMENT
131	indexof_const_startpos_unsat.smt2	unsat	0.014	unsat	0.012	sat	0.156	SOUNDNESS_DISAGREEMENT
132	indexof_var_unsat.smt2	unsat	0.013	sat	0.014	sat	0.158	SOUNDNESS_DISAGREEMENT
133	model-bug.smt2	sat	0.025	sat	0.017	unsat	0.193	SOUNDNESS_DISAGREEMENT
134	nikolai-sat.smt2	unknown	5.009	sat	0.021	sat	0.195
135	nikolai-unsat.smt2	unknown	5.008	unknown	5.027	unknown	5.113
136	nonlinear.smt2	unknown	5.013	unknown	5.012	unknown	5.142
137	noodles-unsat.smt2	unknown	5.035	unsat	0.014	unsat	0.195
138	noodles-unsat2.smt2	unknown	5.037	unsat	0.015	unsat	0.194
139	noodles-unsat3.smt2	unknown	5.013	unsat	0.016	unsat	0.198
140	noodles-unsat4.smt2	unsat	0.013	unsat	0.013	sat	0.165	SOUNDNESS_DISAGREEMENT
141	noodles-unsat5.smt2	unknown	5.009	unsat	0.014	unsat	0.209
142	noodles-unsat6.smt2	unknown	5.023	unsat	0.013	unsat	0.203
143	noodles-unsat7.smt2	unknown	5.015	unsat	0.015	unsat	0.193
144	noodles-unsat8.smt2	unknown	5.012	unknown	5.046	unsat	0.213
145	noodles-unsat9.smt2	unknown	5.011	unknown	5.038	unsat	0.210
146	norn-benchmark-1.smt2	sat	0.011	sat	0.010	sat	0.164
147	norn-benchmark-2.smt2	sat	0.011	sat	0.011	sat	0.163
148	norn-benchmark-3.smt2	sat	0.012	sat	0.011	sat	0.163
149	norn-benchmark-4.smt2	sat	0.012	sat	0.011	sat	0.163
150	norn-benchmark-5.smt2	sat	0.011	sat	0.010	sat	0.163
151	norn-benchmark-6.smt2	sat	0.011	sat	0.011	sat	0.163
152	norn-benchmark-7.smt2	sat	0.011	sat	0.010	sat	0.162
153	norn-benchmark-8.smt2	sat	0.011	sat	0.011	sat	0.162
154	norn-benchmark-9.smt2	sat	0.011	sat	0.011	sat	0.162
155	norn-benchmark-9a.smt2	sat	0.012	sat	0.011	sat	0.162
156	norn-benchmark-9b.smt2	sat	0.012	sat	0.011	sat	0.162
157	norn-benchmark-9c.smt2	sat	0.012	sat	0.011	sat	0.164
158	norn-benchmark-9d.smt2	sat	0.012	sat	0.011	sat	0.163
159	norn-benchmark-9e.smt2	sat	0.012	sat	0.011	sat	0.165
160	norn-benchmark-9f.smt2	unsat	0.012	sat	0.012	unsat	0.167	SOUNDNESS_DISAGREEMENT
161	norn-benchmark-9g.smt2	sat	0.011	sat	0.009	unknown	7.017
162	norn-benchmark-9h.smt2	sat	0.011	sat	0.011	sat	0.164
163	norn-benchmark-9i.smt2	sat	0.012	sat	0.011	unsat	0.168	SOUNDNESS_DISAGREEMENT
164	norn-benchmark-9j.smt2	sat	0.011	sat	0.010	sat	0.163
165	norn-benchmark-9k.smt2	sat	0.011	sat	0.011	sat	0.165
166	norn-benchmark-9l.smt2	sat	0.012	sat	0.011	sat	0.162
167	norn-benchmark-9m.smt2	sat	0.012	sat	0.011	sat	0.163
168	norn-benchmark-9n.smt2	sat	0.012	sat	0.011	sat	0.164
169	norn-benchmark-9o.smt2	sat	0.011	sat	0.011	sat	0.163
170	norn-benchmark-9p.smt2	sat	0.011	sat	0.011	sat	0.163
171	norn-benchmark-9q.smt2	sat	0.011	sat	0.010	sat	0.163
172	norn-benchmark-9r.smt2	sat	0.011	sat	0.011	sat	0.164
173	norn-benchmark-9s.smt2	sat	0.011	sat	0.011	sat	0.164
174	norn-benchmark-9t.smt2	sat	0.011	sat	0.010	sat	0.163
175	norn-benchmark-9u.smt2	sat	0.011	sat	0.011	sat	0.163
176	norn-benchmark-9v.smt2	sat	0.011	sat	0.011	sat	0.163
177	norn-benchmark-9w.smt2	sat	0.011	sat	0.011	sat	0.163
178	norn-benchmark-9x.smt2	sat	0.011	sat	0.011	sat	0.163
179	norn-benchmark-9y.smt2	sat	0.011	sat	0.011	sat	0.163
180	norn-benchmark-9z.smt2	sat	0.011	sat	0.011	sat	0.163
181	prefix-1.smt2	sat	0.014	sat	0.014	unknown	7.018
182	prefix-suffix.smt2	unsat	0.014	sat	0.012	unsat	0.167	SOUNDNESS_DISAGREEMENT
183	prefix3.smt2	sat	0.014	sat	0.012	unsat	0.255	SOUNDNESS_DISAGREEMENT
184	regexdeep.smt2	unknown	5.009	sat	0.017	sat	0.220
185	replace-special-4.smt2	unsat	0.014	sat	0.011	bug	0.082	SOUNDNESS_DISAGREEMENT
186	replace-special-5.smt2	unsat	0.012	sat	0.011	bug	0.078	SOUNDNESS_DISAGREEMENT
187	replace-special.smt2	unsat	0.013	sat	0.011	bug	0.078	SOUNDNESS_DISAGREEMENT
188	simple-concat-1.smt2	sat	0.011	sat	0.011	sat	0.165
189	simple-concat-2.smt2	sat	0.012	sat	0.010	sat	0.165
190	simple-concat-3.smt2	sat	0.012	sat	0.011	sat	0.166
191	simple-concat-4.smt2	sat	0.012	bug	0.058	bug	0.095
192	simple-replace-1.smt2	sat	0.012	sat	0.012	sat	0.164
193	simple-replace-2.smt2	sat	0.012	sat	0.011	sat	0.162
194	simple-replace-3.smt2	sat	0.012	sat	0.011	sat	0.165
195	simple-replace-4.smt2	sat	0.038	bug	4.117	sat	0.852
196	simple-replace-4b.smt2	unsat	0.023	sat	4.117	bug	0.554	SOUNDNESS_DISAGREEMENT
197	simple-replace-5.smt2	sat	0.012	sat	0.012	sat	0.162
198	simple-replace-6.smt2	sat	0.012	sat	0.012	sat	0.162
199	simple-replace-7.smt2	sat	0.012	sat	0.012	sat	0.163
200	simple-replace-8.smt2	sat	0.013	sat	0.012	sat	0.163
201	simple-replace-9.smt2	sat	0.013	sat	0.012	sat	0.164
202	str-lt2.smt2	unsat	0.013	sat	0.012	bug	0.087	SOUNDNESS_DISAGREEMENT
203	str.at-2.smt2	unsat	0.013	sat	0.013	bug	0.082	SOUNDNESS_DISAGREEMENT
204	str.to_int_1.smt2	sat	0.013	sat	0.012	sat	0.164
205	str.to_int_2.smt2	sat	0.013	sat	0.012	sat	0.163
206	str.to_int_3.smt2	sat	0.013	sat	0.012	sat	0.163
207	str.to_int_4.smt2	unknown	5.024	sat	0.015	sat	0.091
208	str.to_int_5.smt2	sat	0.012	sat	0.011	sat	0.165
209	str.to_int_6.smt2	sat	0.012	sat	0.012	sat	0.164
210	str.to_int_7.smt2	sat	0.012	sat	0.012	sat	0.166
211	str.to_int_8.smt2	sat	0.013	sat	0.012	sat	0.165
212	str.to_int_9.smt2	sat	0.013	sat	0.012	sat	0.165
213	str.to_int_10.smt2	sat	0.013	sat	0.012	sat	0.164
214	str.to_int_11.smt2	sat	0.013	sat	0.013	sat	0.163
215	str.to_int_12.smt2	sat	0.014	sat	0.013	sat	0.165
216	str.to_int_13.smt2	sat	0.013	sat	0.013	sat	0.163
217	str.to_int_14.smt2	sat	0.013	sat	0.013	sat	0.163
218	str.to_int_15.smt2	sat	0.013	sat	0.012	sat	0.163
219	str.to_int_16.smt2	sat	0.013	sat	0.013	sat	0.163
220	str.to_int_17.smt2	sat	0.013	sat	0.013	sat	0.163
221	str.to_int_18.smt2	sat	0.013	sat	0.013	sat	0.165
222	str.to_int_19.smt2	sat	0.013	sat	0.013	sat	0.164
223	str.to_int_20.smt2	sat	0.013	sat	0.013	sat	0.164
224	str.to_int_21.smt2	sat	0.013	sat	0.013	sat	0.164
225	str.to_int_22.smt2	sat	0.013	sat	0.013	sat	0.164
226	str.to_int_23.smt2	sat	0.013	sat	0.013	sat	0.164
227	str.to_int_24.smt2	sat	0.013	sat	0.013	sat	0.164
228	str.to_int_25.smt2	sat	0.013	sat	0.013	sat	0.165
229	str.to_int_26.smt2	sat	0.013	sat	0.013	sat	0.165
230	str.to_int_27.smt2	sat	0.013	sat	0.013	sat	0.165
231	str.to_int_28.smt2	sat	0.013	sat	0.013	sat	0.165
232	str.to_int_29.smt2	sat	0.013	sat	0.013	sat	0.163
233	str.to_int_30.smt2	sat	0.013	sat	0.013	sat	0.164
234	str.to_int_31.smt2	sat	0.013	sat	0.013	sat	0.165
235	str.to_int_32.smt2	sat	0.013	sat	0.013	sat	0.165
236	str.to_int_33.smt2	sat	0.013	sat	0.013	sat	0.165
237	str.to_int_34.smt2	sat	0.013	sat	0.013	sat	0.165
238	str.to_int_35.smt2	sat	0.013	sat	0.013	sat	0.165
239	str.to_int_36.smt2	sat	0.013	sat	0.013	sat	0.165
240	str.to_int_37.smt2	sat	0.013	sat	0.013	sat	0.165
241	str.to_int_38.smt2	sat	0.013	sat	0.013	sat	0.163
242	str.to_int_39.smt2	sat	0.013	sat	0.013	sat	0.166
243	str.to_int_40.smt2	sat	0.013	sat	0.013	sat	0.164
244	str.to_int_41.smt2	sat	0.013	sat	0.014	sat	0.164
245	str.to_int_42.smt2	sat	0.013	sat	0.013	sat	0.164
246	str.to_int_43.smt2	sat	0.013	sat	0.013	sat	0.164
247	str.to_int_44.smt2	sat	0.013	sat	0.013	sat	0.164
248	str.to_int_45.smt2	sat	0.013	sat	0.013	sat	0.164
249	str.to_int_46.smt2	sat	0.013	sat	0.013	sat	0.165
250	str.to_int_47.smt2	sat	0.013	sat	0.013	sat	0.166
251	str.to_int_48.smt2	sat	0.013	sat	0.013	sat	0.164
252	str.to_int_49.smt2	sat	0.013	sat	0.013	sat	0.164
253	str.to_int_50.smt2	sat	0.013	sat	0.013	sat	0.164
254	str.to_int_51.smt2	sat	0.013	sat	0.013	sat	0.164
255	str.to_int_52.smt2	sat	0.013	sat	0.013	sat	0.165
256	str.to_int_53.smt2	sat	0.013	sat	0.013	sat	0.163
257	str.to_int_54.smt2	sat	0.013	sat	0.013	sat	0.165
258	str.to_int_55.smt2	sat	0.013	sat	0.013	sat	0.165
259	str.to_int_56.smt2	sat	0.013	sat	0.013	sat	0.164
260	str.to_int_57.smt2	sat	0.013	sat	0.013	sat	0.165
261	str.to_int_58.smt2	sat	0.013	sat	0.013	sat	0.164
262	str.to_int_59.smt2	sat	0.013	sat	0.013	sat	0.164
263	str.to_int_60.smt2	sat	0.013	sat	0.013	sat	0.165
264	str.to_int_61.smt2	sat	0.013	sat	0.013	sat	0.165
265	str.to_int_62.smt2	sat	0.013	sat	0.013	sat	0.165
266	str.to_int_63.smt2	sat	0.013	sat	0.014	sat	0.165
267	str.to_int_64.smt2	sat	0.013	sat	0.013	sat	0.165
268	str.to_int_65.smt2	sat	0.013	sat	0.013	sat	0.165
269	str.to_int_66.smt2	sat	0.013	sat	0.013	sat	0.165
270	str.to_int_67.smt2	sat	0.013	sat	0.013	sat	0.164
271	str.to_int_68.smt2	sat	0.013	sat	0.013	sat	0.166
272	str.to_int_69.smt2	sat	0.013	sat	0.013	sat	0.165
273	str.to_int_70.smt2	sat	0.013	sat	0.013	sat	0.165
274	str.to_int_71.smt2	sat	0.013	sat	0.013	sat	0.165
275	str.to_int_72.smt2	sat	0.013	sat	0.013	sat	0.164
276	str.to_int_73.smt2	sat	0.013	sat	0.013	sat	0.164
277	str.to_int_74.smt2	sat	0.013	sat	0.013	sat	0.164
278	str.to_int_75.smt2	sat	0.013	sat	0.013	sat	0.165
279	str.to_int_76.smt2	sat	0.013	sat	0.013	sat	0.165
280	str.to_int_77.smt2	sat	0.013	sat	0.013	sat	0.165
281	str.to_int_78.smt2	sat	0.013	sat	0.013	sat	0.165
282	str.to_int_79.smt2	sat	0.013	sat	0.014	sat	0.165
283	str.to_int_80.smt2	sat	0.013	sat	0.013	sat	0.164
284	str.to_int_81.smt2	sat	0.013	sat	0.013	sat	0.165
285	str.to_int_82.smt2	sat	0.013	sat	0.013	sat	0.164
286	str.to_int_83.smt2	sat	0.013	sat	0.013	sat	0.165
287	str.to_int_84.smt2	sat	0.013	sat	0.013	sat	0.165
288	str.to_int_85.smt2	sat	0.013	sat	0.013	sat	0.165
289	str.to_int_86.smt2	sat	0.013	sat	0.013	sat	0.165
290	str.to_int_87.smt2	sat	0.013	sat	0.013	sat	0.165
291	str.to_int_88.smt2	sat	0.013	sat	0.013	sat	0.165
292	str.to_int_89.smt2	sat	0.013	sat	0.013	sat	0.165
293	str.to_int_90.smt2	sat	0.013	sat	0.013	sat	0.165
294	substr_const_begin_unsat.smt2	unsat	0.012	unsat	0.011	sat	0.156	SOUNDNESS_DISAGREEMENT
295	substr_const_len_unsat.smt2	unsat	0.012	unsat	0.013	sat	0.157	SOUNDNESS_DISAGREEMENT
296	substr_empty_unsat.smt2	unsat	0.012	unsat	0.011	sat	0.154	SOUNDNESS_DISAGREEMENT
297	substr_var_unsat.smt2	unsat	0.012	unsat	0.013	sat	0.157	SOUNDNESS_DISAGREEMENT
298	word-equation-6-regex.smt2	sat	0.025	sat	0.020	sat	0.294
299	word-equation-6.smt2	sat	0.042	sat	0.226	sat	0.308
300	word-equation.smt2	sat	0.018	sat	0.020	sat	0.265

---

Notable Issues

Soundness Disagreements (Critical) — 25 files

These benchmarks produced conflicting sat/unsat answers between at least two solvers. Items where ZIPT is the outlier may reflect ZIPT's partial handling of the feature; items involving seq vs. nseq warrant further investigation.

• 1234.corecstrs.readable.smt2: seq=sat, nseq=sat, ZIPT=unsat
• bigSubstrIdx.smt2: seq=unknown, nseq=sat, ZIPT=unsat
• contains-3.smt2: seq=unsat, nseq=unsat, ZIPT=sat
• contains-4.smt2: seq=unsat, nseq=sat, ZIPT=sat
• failedProp.smt2: seq=unsat, nseq=sat, ZIPT=bug
• failedProp2.smt2: seq=unsat, nseq=sat, ZIPT=bug
• indexof_const_index_unsat.smt2: seq=unsat, nseq=sat, ZIPT=sat
• indexof_const_startpos_unsat.smt2: seq=unsat, nseq=unsat, ZIPT=sat
• indexof_var_unsat.smt2: seq=unsat, nseq=sat, ZIPT=sat
• model-bug.smt2: seq=sat, nseq=sat, ZIPT=unsat
• noodles-unsat4.smt2: seq=unsat, nseq=unsat, ZIPT=sat
• norn-benchmark-9f.smt2: seq=unsat, nseq=sat, ZIPT=unsat
• norn-benchmark-9i.smt2: seq=sat, nseq=sat, ZIPT=unsat
• prefix-suffix.smt2: seq=unsat, nseq=sat, ZIPT=unsat
• prefix3.smt2: seq=sat, nseq=sat, ZIPT=unsat
• replace-special-4.smt2: seq=unsat, nseq=sat, ZIPT=bug
• replace-special-5.smt2: seq=unsat, nseq=sat, ZIPT=bug
• replace-special.smt2: seq=unsat, nseq=sat, ZIPT=bug
• simple-replace-4b.smt2: seq=unsat, nseq=sat, ZIPT=bug
• str-lt2.smt2: seq=unsat, nseq=sat, ZIPT=bug
• str.at-2.smt2: seq=unsat, nseq=sat, ZIPT=bug
• substr_const_begin_unsat.smt2: seq=unsat, nseq=unsat, ZIPT=sat
• substr_const_len_unsat.smt2: seq=unsat, nseq=unsat, ZIPT=sat
• substr_empty_unsat.smt2: seq=unsat, nseq=unsat, ZIPT=sat
• substr_var_unsat.smt2: seq=unsat, nseq=unsat, ZIPT=sat

Key seq vs. nseq disagreements (ZIPT excluded, both seq and nseq give definitive answers but disagree):

• contains-4.smt2: seq=unsat, nseq=sat
• failedProp.smt2: seq=unsat, nseq=sat
• failedProp2.smt2: seq=unsat, nseq=sat
• indexof_const_index_unsat.smt2: seq=unsat, nseq=sat
• indexof_var_unsat.smt2: seq=unsat, nseq=sat
• norn-benchmark-9f.smt2: seq=unsat, nseq=sat
• prefix-suffix.smt2: seq=unsat, nseq=sat
• replace-special-4.smt2: seq=unsat, nseq=sat
• replace-special-5.smt2: seq=unsat, nseq=sat
• replace-special.smt2: seq=unsat, nseq=sat
• simple-replace-4b.smt2: seq=unsat, nseq=sat
• str-lt2.smt2: seq=unsat, nseq=sat
• str.at-2.smt2: seq=unsat, nseq=sat

Crashes / Bugs

nseq assertion violations (2 files):

• simple-concat-4.smt2 (nseq crash/assertion violation)
• simple-replace-4.smt2 (nseq crash/assertion violation)

ZIPT crashes/unsupported (180 files): Primarily unsupported SMT-LIB2 features (seq-head/seq-tail, ADTs, strings_exp set-option, bitvector char encodings). See per-file table for full list.

Slow Benchmarks (> 4 s for any solver) — 28 files

• prefix-1.smt2: seq=0.014s, nseq=0.014s, ZIPT=7.018s
• concat-empty.smt2: seq=0.010s, nseq=0.009s, ZIPT=7.017s
• norn-benchmark-9g.smt2: seq=0.011s, nseq=0.009s, ZIPT=7.017s
• nonlinear.smt2: seq=5.013s, nseq=5.012s, ZIPT=5.142s
• artur-unsat-common-prefix.smt2: seq=0.016s, nseq=0.018s, ZIPT=5.141s
• artur-unsat-we.smt2: seq=5.008s, nseq=5.034s, ZIPT=5.120s
• nikolai-unsat.smt2: seq=5.008s, nseq=5.027s, ZIPT=5.113s
• artur-unsat.smt2: seq=5.012s, nseq=0.014s, ZIPT=5.108s
• concat-regex4.smt2: seq=5.048s, nseq=5.014s, ZIPT=0.195s
• noodles-unsat8.smt2: seq=5.012s, nseq=5.046s, ZIPT=0.213s
• simple-replace-4.smt2: seq=0.038s, nseq=5.039s, ZIPT=0.852s
• noodles-unsat9.smt2: seq=5.011s, nseq=5.038s, ZIPT=0.210s
• noodles-unsat2.smt2: seq=5.037s, nseq=0.015s, ZIPT=0.194s
• noodles-unsat.smt2: seq=5.035s, nseq=0.014s, ZIPT=0.195s
• str.to_int_4.smt2: seq=5.024s, nseq=0.015s, ZIPT=0.091s
• noodles-unsat6.smt2: seq=5.023s, nseq=0.013s, ZIPT=0.203s
• indexof-2.smt2: seq=5.018s, nseq=0.034s, ZIPT=0.150s
• concat-regex2.smt2: seq=5.017s, nseq=0.012s, ZIPT=0.169s
• bigSubstrIdx.smt2: seq=5.015s, nseq=0.100s, ZIPT=0.255s
• noodles-unsat7.smt2: seq=5.015s, nseq=0.015s, ZIPT=0.193s
• noodles-unsat3.smt2: seq=5.013s, nseq=0.016s, ZIPT=0.198s
• nikolai-sat.smt2: seq=5.009s, nseq=0.021s, ZIPT=0.195s
• noodles-unsat5.smt2: seq=5.009s, nseq=0.014s, ZIPT=0.209s
• regexdeep.smt2: seq=5.009s, nseq=0.017s, ZIPT=0.220s
• substring-bug2.smt2: seq=5.009s, nseq=0.016s, ZIPT=0.559s
• all-quantifiers.smt2: seq=0.019s, nseq=5.008s, ZIPT=0.580s
• simple-replace-4b.smt2: seq=0.023s, nseq=4.117s, ZIPT=0.554s
• suffix-1.smt2: seq=0.014s, nseq=0.014s, ZIPT=7.019s

---

Generated automatically by the Ostrich Benchmark workflow on the c3 branch.

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

• expires on Apr 3, 2026, 7:06 AM UTC