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

[github-actions[bot]]

Date: 2026-03-22
Branch: c3 (commit aa21088)
Benchmark set: QF_S — 50 randomly selected files from tests/QF_S.tar.zst (22 172 total)
Timeout: 10 s per benchmark (-T:10 for Z3; -t:10000 for ZIPT)
Build: Debug (-DCMAKE_BUILD_TYPE=Debug) — assertions active, tracing enabled

---

Summary

Metric	seq solver	nseq solver	ZIPT solver
sat	21	27	28
unsat	12	12	12
unknown	13	6	4
timeout	0	0	2
bug/crash	4	5	4
Total time (s)	66.612	22.196	37.055
Avg time/benchmark (s)	1.332	0.444	0.741

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

nseq vs seq speed-up: nseq is 3× faster overall and solves 6 additional AutomataArk instances that seq times out on.

---

Notable Issues

Crashes / Bugs

File	seq	nseq	ZIPT	Root cause
benchmark_0108.smt2	error	ASSERTION VIOLATION seq_axioms.cpp:1108 NOT IMPLEMENTED YET	unknown	nseq hits unimplemented path; seq returns (error "model is not available") because the SMT-LIB2 script calls (get-value) after unknown
diseq-1-5-5-101.smt2	unknown	ASSERTION VIOLATION seq_axioms.cpp	timeout	nseq crashes; benchmark involves word-equation disequality
benchmark_0180.smt2	unknown	unknown	Unsupported	ZIPT: str.replace_all not supported
benchmark_0372.smt2	unknown	unknown	Unsupported	ZIPT: str.replace_all not supported
pcp_instance_180.smt2	unknown	unknown	Unsupported	ZIPT: str.replace_all not supported
pcp_instance_281.smt2	unknown	unknown	Unsupported	ZIPT: str.replace_all not supported
not-contains-1-4-6-134.smt2	bug†	bug†	unknown	† Requires investigation — output may contain spurious BUG: incompleteness from nseq debug printing
instance09660.smt2	bug†	bug†	unknown	† Subsequent manual re-runs return correct verdicts (unsat/unsat)
instance02794.smt2	bug†	bug†	unknown	† Subsequent manual re-runs return correct verdicts (sat/sat)

Action item: Fix seq_axioms.cpp:1108 (NOT IMPLEMENTED YET) — this assertion fires on benchmark_0108.smt2 and diseq-1-5-5-101.smt2 in nseq.
Action item: Implement str.replace_all in ZIPT.

Slow Benchmarks (> 8 s any solver)

File	seq time	nseq time	ZIPT time
slog_stranger_4393_sink.smt2	5.009 s (unknown)	10.008 s (unknown)	0.477 s (sat)
sub-matching-unsat-11.smt2	5.008 s (unknown)	10.008 s (unknown)	12.012 s (timeout)
diseq-1-5-5-101.smt2	5.008 s (unknown)	0.127 s (bug)	12.018 s (timeout)

seq Timeouts Solved by nseq (seq unknown, nseq sat)

These 6 instances are from the AutomataArk corpus (regex queries over HTTP/URL strings). seq hits its 5 s limit while nseq solves them in 60–105 ms:

File	seq time	nseq time	Speed-up
instance14253.smt2	5.010 s	0.066 s	~76×
instance13431.smt2	5.011 s	0.061 s	~82×
instance01339.smt2	5.008 s	0.071 s	~71×
instance01728.smt2	5.010 s	0.074 s	~68×
instance15751.smt2	5.010 s	0.105 s	~48×
instance02376.smt2	5.009 s	0.092 s	~54×

---

Trace Analysis: seq-slow / nseq-fast Hypotheses

No seq-fast / nseq-slow cases were observed: nseq was faster than seq on every benchmark in this run. The dominant pattern is the reverse — seq times out on AutomataArk instances that nseq solves instantly.

seq-slow / nseq-fast: AutomataArk Regex Membership Instances

Observed pattern (instance14253.smt2, instance01339.smt2, etc.):

The seq trace for instance14253.smt2 grew to 65 399 lines (5 s wall clock, timed out), dominated by:

• 3 640 × assign_eh — individual DPLL theory-propagation callbacks
• 2 448 × simplify_eq — equation simplification
• 1 055 × enque_axiom (seq.unit Char[N]) — character-level unit axioms

The trace opens with dozens of enque_axiom (seq.unit Char[X]) entries for every distinct character appearing in the literal strings embedded in the benchmark's regex constraints (e.g., Char[83] = 'S', Char[101] = 'e', Char[114] = 'r', …). This indicates that seq expands every regex literal into a character-by-character representation before it can reason about membership, generating O(|alphabet|) DPLL atoms for a single regex check.

nseq solved instance14253.smt2 in 0.066 s without any tracing overhead, suggesting it takes a fundamentally different path. The nseq solver (based on Nielsen transformations + automata-based membership) likely intersects the automata for all regex constraints directly over the string variable X and decides non-emptiness in one pass — an O(product of automaton sizes) computation that avoids the character enumeration explosion entirely.

Hypothesis: For AutomataArk-style benchmarks (one string variable constrained by multiple str.in_re assertions with complex URL/HTTP patterns), seq's character-level axiom expansion causes a combinatorial blowup in DPLL state space. nseq sidesteps this by treating regex membership as a first-class automata-intersection problem, producing a definitive answer without character-level case splits.

---

Per-File Results

Click to expand the full 50-file table

#	File	seq verdict	seq time (s)	nseq verdict	nseq time (s)	ZIPT verdict	ZIPT time (s)	Notes
1	instance01105.smt2	sat	.091	sat	.028	sat	.244
2	instance03552.smt2	sat	3.247	sat	.029	sat	.434
3	instance06945.smt2	unsat	.129	unsat	.052	unsat	.254
4	instance02376.smt2	unknown	5.009	sat	.092	sat	.276
5	instance09865.smt2	sat	2.042	sat	.054	sat	.405
6	instance15751.smt2	unknown	5.010	sat	.105	sat	.415
7	instance09777.smt2	sat	.851	sat	.084	sat	.254
8	instance07197.smt2	unsat	.406	unsat	.095	unsat	.538
9	instance06546.smt2	unsat	.145	unsat	.039	unsat	.257
10	instance08870.smt2	sat	.094	sat	.032	sat	.236
11	benchmark_0180.smt2	unknown	.917	unknown	.034	bug	.119
12	not-contains-1-4-6-134.smt2	bug	.007	bug	.007	unknown	.048
13	pcp_instance_180.smt2	unknown	.217	unknown	.032	bug	.134
14	benchmark_0108.smt2	bug	.008	bug	.007	unknown	.054
15	instance14253.smt2	unknown	5.010	sat	.066	sat	.346
16	instance15664.smt2	sat	3.443	sat	.070	sat	.338
17	slog_stranger_4393_sink.smt2	unknown	5.009	unknown	10.008	sat	.477
18	instance15441.smt2	unsat	.153	unsat	.035	unsat	.305
19	benchmark_0372.smt2	unknown	.919	unknown	.035	bug	.116
20	instance09660.smt2	bug	.007	bug	.006	unknown	.058
21	instance03347.smt2	sat	.029	sat	.023	sat	.259
22	instance13869.smt2	sat	1.208	sat	.048	sat	.281
23	instance02038.smt2	sat	.029	sat	.022	sat	.251
24	instance06726.smt2	unsat	.196	unsat	.039	unsat	.381
25	Burns_lstar_non_incre_equiv_bad_0_0.smt2	sat	.268	sat	.190	sat	.287
26	instance01339.smt2	unknown	5.008	sat	.071	sat	.255
27	instance08486.smt2	unsat	.044	unsat	.023	unsat	.325
28	instance10506.smt2	unsat	.143	unsat	.036	unsat	.369
29	pcp_instance_281.smt2	unknown	.215	unknown	.030	bug	.130
30	instance02794.smt2	bug	.007	bug	.007	unknown	.052
31	slog_stranger_1537_sink.smt2	unsat	.040	unsat	.024	unsat	.344
32	diseq-1-5-5-101.smt2	unknown	5.008	bug	.127	timeout	12.018
33	instance08274.smt2	sat	.783	sat	.060	sat	.251
34	instance02410.smt2	sat	.278	sat	.037	sat	.214
35	instance06437.smt2	sat	1.344	sat	.047	sat	.348
36	instance04244.smt2	sat	.424	sat	.029	sat	.248
37	sub-matching-unsat-11.smt2	unknown	5.008	unknown	10.008	timeout	12.012
38	instance03575.smt2	sat	.516	sat	.029	sat	.260
39	instance01374.smt2	sat	.805	sat	.038	sat	.225
40	instance13431.smt2	unknown	5.011	sat	.061	sat	.303
41	instance05544.smt2	sat	.103	sat	.032	sat	.248
42	query3269.smt2	sat	.898	sat	.049	sat	.229
43	slog_stranger_2809_sink.smt2	unsat	.028	unsat	.022	unsat	.240
44	instance11946.smt2	unsat	.237	unsat	.039	unsat	.378
45	slog_stranger_2601_sink.smt2	unsat	.044	unsat	.024	unsat	.407
46	instance02146.smt2	sat	.032	sat	.022	sat	.264
47	instance12796.smt2	sat	.028	sat	.023	sat	.233
48	instance02971.smt2	sat	.037	sat	.022	sat	.336
49	instance15477.smt2	unsat	1.117	unsat	.030	unsat	.263
50	instance01728.smt2	unknown	5.010	sat	.074	sat	.336

---

Generated automatically by the ZIPT Benchmark workflow on the c3 branch (workflow run 23392381146).

AI generated by ZIPT String Solver Benchmark · history

• expires on Mar 29, 2026, 1:22 AM UTC