[ZIPT Benchmark] Z3 c3 branch — 2026-03-28

[github-actions[bot]]

Date: 2026-03-28
Branch: c3 (commit ebd35bc)
Benchmark set: QF_S (200 randomly selected from 22,172 files in tests/QF_S.tar.zst)
Timeout: seq -T:5 + outer 7 s; nseq -T:5 + outer 12 s; ZIPT -t:5000 + outer 12 s
Z3 build: Debug (CMake, ninja), v4.17.0, commit ebd35bc
ZIPT: parikh branch, built against Microsoft.Z3.dll (net8.0)

---

Summary

Metric	seq solver	nseq solver	ZIPT solver
sat	83	104	110
unsat	57	59	61
unknown	57	28	3
timeout (outer)	0	0	3
bug/crash	3	9	23
Total time (s)	250.877	33.016	98.741
Avg time/benchmark (s)	1.254	0.165	0.494

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

Key observations:

• nseq is 7.6× faster than seq on average (0.165 s vs 1.254 s per benchmark); solves 23 more definitive cases
• ZIPT solves the most definitively (171 sat+unsat) but has 23 crashes and 1 confirmed soundness error
• seq times out 57 times vs 28 for nseq and 3 for ZIPT
• nseq crashes on not-contains and diseq benchmarks (6 cases), emitting a DOT debug graph instead of a verdict
• seq and nseq both produce non-standard output on 3 slog_stranger/instance files (unsupported constructs)

---

Notable Issues

Soundness Disagreements (Critical)

1. coffee-can_lstar_non_incre_equiv_init_0_0.smt2 — seq=unsat, nseq=unsat, ZIPT=sat
   • Source: HornStr CHC-over-strings benchmark (:status unknown)
   • Both Z3 solvers agree on unsat; ZIPT's sat answer is almost certainly a soundness bug in ZIPT
   • The formula involves complex regex equivalence queries: re.*, re.++, re.union, re.comp

Crashes / Bugs

nseq-only crashes (6 files) — not-contains and diseq benchmarks:

• not-contains-1-5-5-133.smt2, not-contains-1-4-5-135.smt2, not-contains-1-4-5-121.smt2, not-contains-1-5-6-125.smt2
• diseq-None-5-6-106.smt2, diseq-1-5-6-106.smt2

nseq emits a DOT-format debug graph (digraph G {) to stdout instead of sat/unsat when encountering string disequality constraints. This is a debug output path being triggered rather than a solver verdict, indicating an incomplete or debugging code path in the nseq solver on these problem types.

seq+nseq both produce non-standard output (3 files):

• slog_stranger_3304_sink.smt2, slog_stranger_1530_sink.smt2, instance08332.smt2

Both seq and nseq output something other than sat/unsat/unknown on these files (likely unsupported string constructs or internal assertion failures during trace).

ZIPT crashes (23 events, 22 unique files):

• Primarily pcp_*, unsolved_pcp_* (Post Correspondence Problem), and benchmark_0xxx families
• ZIPT does not support PCP-style encodings or certain query patterns

Slow Benchmarks (outer-killed > 8 s)

• diseq-None-5-6-106.smt2 (zipt: 12.016 s outer-killed)
• wildcard-matching-regex-30.smt2 (zipt: 12.009 s outer-killed)
• diseq-1-5-6-106.smt2 (zipt: 12.017 s outer-killed)

Trace Analysis: seq-fast / nseq-slow Hypotheses

No files met the strict criterion (seq < 1.0 s AND nseq > 3× seq AND nseq > 0.5 s) in this 200-file sample.

The dominant pattern was the opposite: nseq consistently outperformed seq. Many cases where seq timed out at 5 s were solved by nseq in under 0.1 s — for example:

• instance15640: seq=3.984 s vs nseq=0.045 s (88× faster)
• instance04470: seq=5.018 s (timeout) vs nseq=0.062 s
• slog_stranger_4749_sink: seq=5.009 s (timeout) vs nseq=0.043 s

This reflects nseq's Nielsen-graph + Parikh constraint architecture providing tighter early termination compared to seq's SMT-based sequence rewriting calculus, which can generate large numbers of intermediate lemmas before concluding.

The one notable case where both solvers were slow is instance14567.smt2 (seq=3.917 s, nseq=2.632 s, ZIPT=0.329 s), suggesting ZIPT's arithmetic/length constraint propagation is most effective on that instance.

---

Per-File Results (200 benchmarks)

#	File	seq verdict	seq time (s)	nseq verdict	nseq time (s)	ZIPT verdict	ZIPT time (s)	Notes
1	instance09421.smt2	unsat	.108	unsat	.031	unsat	.256
2	unsolved_pcp_instance_221.smt2	unknown	.364	unknown	.199	bug	.135
3	instance11040.smt2	unknown	5.009	unsat	.053	unsat	.250
4	instance05427.smt2	sat	.061	sat	.028	sat	.190
5	query7313.smt2	unknown	5.009	sat	.039	sat	.254
6	instance15599.smt2	unsat	.307	unsat	.060	unsat	.421
7	instance00980.smt2	sat	.183	sat	.037	sat	.235
8	slog_stranger_1662_sink.smt2	unsat	.024	unsat	.022	unsat	.235
9	benchmark_0181.smt2	unknown	1.055	unknown	.251	bug	.177
10	instance12848.smt2	unsat	.526	unsat	.083	unsat	.603
11	instance15064.smt2	sat	.854	sat	.057	sat	.423
12	instance14113.smt2	unsat	.209	unsat	.039	unsat	.342
13	slog_stranger_2087_sink.smt2	unsat	1.696	unknown	5.009	unsat	2.093
14	instance05920.smt2	sat	.084	sat	.029	sat	.242
15	instance02335.smt2	sat	.047	sat	.026	sat	.183
16	instance15640.smt2	sat	3.984	sat	.045	sat	.363
17	unsolved_pcp_instance_146.smt2	unknown	.352	unknown	.192	bug	.191
18	instance07354.smt2	unsat	2.190	unsat	.234	unsat	.313
19	instance11494.smt2	sat	.932	sat	.045	sat	.363
20	instance15774.smt2	unsat	2.113	unsat	.045	unsat	.323
21	unsolved_pcp_instance_111.smt2	unknown	.362	unknown	.198	bug	.197
22	not-contains-1-5-5-133.smt2	unknown	5.010	bug	1.414	sat	.187
23	03_track_176.smt2	unknown	5.008	sat	.093	sat	.301
24	slog_stranger_1407_sink.smt2	sat	.917	sat	.038	sat	.253
25	instance05507.smt2	sat	1.123	sat	.028	sat	.335
26	instance02933.smt2	sat	.081	sat	.029	sat	.234
27	instance05340.smt2	sat	.129	sat	.031	sat	.193
28	04_track_177.smt2	sat	3.092	sat	.084	sat	.601
29	pcp_instance_402.smt2	unknown	.360	unknown	.191	bug	.132
30	instance06612.smt2	sat	.188	sat	.078	sat	.262
31	query5196.smt2	sat	1.177	sat	.043	sat	.326
32	unsolved_pcp_instance_217.smt2	unknown	.437	unknown	.191	bug	.196
33	benchmark_0424.smt2	unknown	1.505	unknown	.278	bug	.169
34	instance09835.smt2	unsat	.033	unsat	.030	unsat	.410
35	instance05566.smt2	sat	.096	sat	.028	sat	.244
36	instance02380.smt2	sat	1.873	sat	.028	sat	.354
37	instance14478.smt2	unsat	.045	unsat	.022	unsat	.386
38	instance05831.smt2	sat	.437	sat	.040	sat	.226
39	instance13449.smt2	unsat	.030	unsat	.023	unsat	.271
40	instance02409.smt2	sat	.060	sat	.028	sat	.204
41	instance06258.smt2	unsat	.051	unsat	.022	unsat	.392
42	instance07891.smt2	unsat	.133	unsat	.035	unsat	.330
43	instance00905.smt2	sat	.032	sat	.022	sat	.288
44	instance15772.smt2	unsat	.287	unsat	.039	unsat	.309
45	instance05191.smt2	sat	.290	sat	.039	sat	.214
46	instance11816.smt2	sat	.868	sat	.055	sat	.283
47	instance05164.smt2	sat	.085	sat	.030	sat	.241
48	instance10954.smt2	unsat	.141	unsat	.044	unsat	.296
49	instance12741.smt2	unsat	.030	unsat	.024	unsat	.271
50	instance06256.smt2	sat	.130	sat	.031	sat	.242
51	04_track_60.smt2	unsat	.330	unsat	.025	unsat	.462
52	unsolved_pcp_instance_437.smt2	unknown	.346	unknown	.190	bug	.199
53	instance14691.smt2	sat	.208	sat	.046	sat	.258
54	instance03496.smt2	sat	.087	sat	.029	sat	.215
55	instance07039.smt2	unsat	.149	unsat	.041	unsat	.371
56	instance07863.smt2	unknown	5.010	unsat	.071	unsat	.297
57	pcp_instance_491.smt2	unknown	.402	unknown	.188	bug	.197
58	unsolved_pcp_instance_356.smt2	unknown	.513	unknown	.251	bug	.259
59	instance06488.smt2	sat	.090	sat	.029	sat	.627
60	instance02576.smt2	sat	.084	sat	.034	sat	.347
61	instance05555.smt2	sat	.115	sat	.036	sat	.317
62	instance00418.smt2	sat	1.023	sat	.027	sat	.285
63	instance01579.smt2	sat	.076	sat	.027	sat	.213
64	pcp_instance_15.smt2	unknown	.364	unknown	.181	bug	.133
65	instance08228.smt2	sat	1.166	sat	.051	sat	.349
66	instance10441.smt2	unsat	.497	unknown	.045	unsat	.458
67	slog_stranger_3304_sink.smt2	bug	.007	bug	.006	unknown	.049
68	Lehmann-Rabin_sat_non_incre_equiv_trans_15_0.smt2	unsat	.028	unsat	.025	unsat	.233
69	slog_stranger_4552_sink.smt2	sat	.406	sat	.033	sat	.243
70	instance06866.smt2	sat	.806	sat	.053	sat	.314
71	03_track_170.smt2	unknown	5.011	sat	.114	sat	.300
72	instance01580.smt2	sat	.044	sat	.026	sat	.185
73	instance06755.smt2	unknown	5.009	sat	.274	sat	.324
74	pcp_instance_478.smt2	unknown	.389	unknown	.194	bug	.205
75	instance15610.smt2	sat	.207	sat	.043	sat	.378
76	instance14918.smt2	sat	.664	sat	.038	sat	.300
77	instance07315.smt2	unsat	.035	unsat	.027	unsat	.373
78	instance14871.smt2	unknown	5.008	sat	2.174	sat	1.284
79	slog_stranger_4234_sink.smt2	unknown	5.008	sat	.062	sat	.402
80	instance06482.smt2	unsat	.043	unsat	.023	unsat	.445
81	instance05104.smt2	unknown	5.009	sat	.059	sat	.251
82	instance13133.smt2	unsat	.241	unsat	.046	unsat	.331
83	slog_stranger_4749_sink.smt2	unknown	5.009	sat	.043	sat	.475
84	slog_stranger_2525_sink.smt2	unsat	.034	unsat	.022	unsat	.311
85	instance04448.smt2	sat	.067	sat	.027	sat	.204
86	instance00510.smt2	sat	.123	sat	.029	sat	.198
87	instance10454.smt2	unknown	5.009	sat	.069	sat	.343
88	instance15698.smt2	unsat	.132	unsat	.037	unsat	.308
89	slog_stranger_1559_sink.smt2	unsat	.031	unsat	.023	unsat	.281
90	instance04606.smt2	sat	.683	sat	.034	sat	.221
91	query5997.smt2	sat	.593	unknown	.036	sat	.241
92	instance08332.smt2	bug	.006	bug	.006	unknown	.047
93	instance01649.smt2	sat	.051	sat	.027	sat	.195
94	instance07156.smt2	unsat	.299	unsat	.064	unsat	.416
95	instance07015.smt2	unsat	.184	unsat	.038	unsat	.390
96	instance08027.smt2	sat	.182	sat	.030	sat	.400
97	instance14689.smt2	unsat	.125	unsat	.031	unsat	.296
98	pcp_instance_136.smt2	unknown	.378	unknown	.193	bug	.194
99	instance07200.smt2	sat	.052	sat	.029	sat	.586
100	instance15965.smt2	unknown	5.015	sat	.048	sat	.362
101	eqdist_lstar_non_incre_equiv_trans_0_22.smt2	unknown	5.008	unknown	5.008	unsat	.408
102	instance00970.smt2	sat	.037	sat	.021	sat	.351
103	instance02430.smt2	sat	.075	sat	.028	sat	.222
104	benchmark_0031.smt2	unknown	1.030	unknown	.194	bug	.116
105	instance07146.smt2	sat	.173	sat	.031	sat	.316
106	instance04511.smt2	sat	.060	sat	.028	sat	.241
107	instance13606.smt2	sat	1.174	sat	.037	sat	.352
108	pcp_instance_451.smt2	unknown	.387	unknown	.189	bug	.130
109	instance10542.smt2	unsat	.036	unsat	.023	unsat	.346
110	instance04659.smt2	sat	.030	sat	.024	sat	.263
111	instance06195.smt2	sat	.044	sat	.024	sat	.467
112	instance00339.smt2	sat	1.409	sat	.027	sat	.324
113	slog_stranger_642_sink.smt2	unsat	.028	unsat	.022	unsat	.251
114	instance04470.smt2	unknown	5.018	sat	.062	sat	.346
115	instance04479.smt2	sat	.464	sat	.027	sat	.255
116	unsolved_pcp_instance_387.smt2	unknown	.349	unknown	.190	bug	.197
117	benchmark_0488.smt2	unknown	1.332	unknown	.280	bug	.204
118	not-contains-1-4-5-135.smt2	unknown	5.010	bug	.125	sat	.174
119	instance12253.smt2	unsat	.035	unsat	.022	unsat	.339
120	instance13373.smt2	sat	.037	sat	.029	sat	.349
121	instance06310.smt2	unsat	1.902	unsat	.045	unsat	.357
122	instance05896.smt2	sat	.030	sat	.021	sat	.260
123	instance09391.smt2	unsat	.042	unsat	.023	unsat	.417
124	instance15678.smt2	unsat	.045	unsat	.032	unsat	.351
125	slog_stranger_753_sink.smt2	sat	.572	sat	.030	sat	.249
126	slog_stranger_202_sink.smt2	unsat	.032	unsat	.022	unsat	.294
127	instance01817.smt2	sat	.129	sat	.030	sat	.192
128	benchmark_0406.smt2	unknown	1.015	unknown	.198	bug	.116
129	diseq-None-5-6-106.smt2	unknown	5.008	bug	.097	timeout	12.016
130	instance07978.smt2	unsat	.251	unsat	.045	unsat	.355
131	not-contains-1-4-5-121.smt2	unknown	5.009	bug	.128	sat	.175
132	instance00749.smt2	sat	.102	sat	.031	sat	.227
133	instance03293.smt2	sat	1.015	sat	.038	sat	.218
134	01_track_4.smt2	sat	.206	sat	.037	sat	.246
135	instance09474.smt2	sat	2.295	sat	.059	sat	.442
136	two_token_pass_lstar_non_incre_equiv_bad_0_1.smt2	unknown	5.008	unsat	.042	unsat	.273
137	instance09671.smt2	unsat	2.211	unsat	.043	unsat	.373
138	slog_stranger_5046_sink.smt2	unknown	5.011	sat	2.109	sat	1.049
139	instance05133.smt2	sat	2.456	sat	.039	sat	.217
140	wildcard-matching-regex-30.smt2	unknown	5.008	unknown	.420	timeout	12.009
141	slog_stranger_1530_sink.smt2	bug	.007	bug	.006	unknown	.055
142	instance00340.smt2	sat	2.118	sat	.071	sat	.266
143	slog_stranger_2228_sink.smt2	unsat	.033	unsat	.023	unsat	.297
144	diseq-1-5-6-106.smt2	unknown	5.008	bug	.097	timeout	12.017
145	instance09949.smt2	sat	1.415	sat	.043	sat	.304
146	instance05757.smt2	sat	.156	sat	.037	sat	.293
147	instance03809.smt2	unknown	5.010	sat	.037	sat	.219
148	instance02989.smt2	sat	.130	sat	.029	sat	.377
149	instance07465.smt2	unsat	.034	unsat	.022	unsat	.311
150	instance13735.smt2	sat	.253	sat	.043	sat	.298
151	slog_stranger_2174_sink.smt2	unknown	5.009	sat	.101	sat	.361
152	instance07655.smt2	unsat	.391	unsat	.055	unsat	.395
153	instance11913.smt2	sat	.036	sat	.023	sat	.342
154	slog_stranger_1562_sink.smt2	unsat	.291	unsat	.089	unsat	1.040
155	benchmark_0082.smt2	unknown	1.018	unknown	.195	bug	.117
156	instance05339.smt2	sat	.044	sat	.022	sat	.712
157	instance13000.smt2	unknown	5.012	sat	.070	sat	.290
158	query6109.smt2	sat	.932	sat	.033	sat	.221
159	instance07417.smt2	unsat	.134	unsat	.041	unsat	.273
160	benchmark_0145.smt2	unknown	1.002	unknown	.195	bug	.167
161	slog_stranger_3072_sink.smt2	unknown	5.010	sat	.040	sat	.358
162	instance00461.smt2	sat	.074	sat	.029	sat	.224
163	instance09105.smt2	unsat	.195	unsat	.060	unsat	.310
164	slog_stranger_1604_sink.smt2	unsat	.027	unsat	.021	unsat	.239
165	instance11019.smt2	unsat	.250	unsat	.051	unsat	.314
166	slog_stranger_2119_sink.smt2	unsat	.033	unsat	.023	unsat	.306
167	instance01329.smt2	sat	.080	sat	.035	sat	.199
168	instance07709.smt2	sat	2.195	sat	.085	sat	.249
169	slog_stranger_4597_sink.smt2	unknown	5.008	sat	.148	sat	.386
170	03_track_34.smt2	unsat	.028	unsat	.020	unsat	.240
171	coffee-can_lstar_non_incre_equiv_init_0_0.smt2	unsat	.024	unsat	.023	sat	.268	SOUNDNESS_DISAGREEMENT
172	instance11261.smt2	unsat	.034	unsat	.024	unsat	.295
173	slog_stranger_5032_sink.smt2	unknown	5.011	sat	1.780	sat	1.967
174	benchmark_0406.smt2	unknown	1.028	unknown	.191	bug	.115
175	instance14837.smt2	unsat	.102	unsat	.030	unsat	.278
176	instance03570.smt2	sat	.068	sat	.029	sat	.188
177	instance06516.smt2	unsat	.207	unsat	.046	unsat	.458
178	unsolved_pcp_instance_181.smt2	unknown	.428	unknown	.274	bug	.258
179	instance04518.smt2	sat	.101	sat	.036	sat	.288
180	instance11386.smt2	unsat	.686	unsat	.092	unsat	.421
181	instance10627.smt2	unknown	5.010	sat	.078	sat	.320
182	slog_stranger_2475_sink.smt2	unsat	.041	unsat	.022	unsat	.383
183	instance01542.smt2	sat	.126	sat	.029	sat	.299
184	instance03846.smt2	sat	.029	sat	.021	sat	.250
185	instance02004.smt2	sat	.107	sat	.037	sat	.219
186	instance14567.smt2	unsat	3.917	unsat	2.632	unsat	.329
187	pcp_instance_226.smt2	unknown	.362	unknown	.190	bug	.132
188	instance13782.smt2	unknown	5.011	sat	.056	sat	.351
189	instance03029.smt2	sat	.073	sat	.027	sat	.208
190	instance06065.smt2	unknown	5.011	sat	.053	sat	.265
191	instance10834.smt2	unsat	.197	unsat	.035	unsat	.370
192	slog_stranger_5416_sink.smt2	sat	.178	sat	.030	sat	.232
193	instance00299.smt2	sat	.069	sat	.027	sat	.213
194	instance04520.smt2	sat	.098	sat	.031	sat	.235
195	not-contains-1-5-6-125.smt2	unknown	5.008	bug	.214	sat	.178
196	instance11056.smt2	unknown	5.011	sat	.141	sat	.309
197	instance08238.smt2	sat	2.100	sat	.093	sat	.363
198	Lehmann-Rabin_lstar_non_incre_equiv_bad_0_1.smt2	unknown	5.008	unsat	.049	unsat	.274
199	instance02951.smt2	sat	.108	sat	.028	sat	.238
200	instance06924.smt2	unsat	.243	unsat	.060	unsat	.359

---

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

AI generated by ZIPT String Solver Benchmark · history

• expires on Apr 4, 2026, 1:23 AM UTC

[github-actions[bot]]

This discussion has been marked as outdated by ZIPT String Solver Benchmark.

A newer discussion is available at Discussion #9214.