[QF_S Benchmark] seq vs nseq on 299 ostrich benchmarks (c3 branch, 2026-06-11)

[github-actions[bot]]

Date: 2026-06-11
Branch: c3
Commit: be62700
Workflow Run: #27350603468
Files benchmarked: 299 (from tests/ostrich.zip, timeout 5 s per file, Z3 internal timeout 4 s)

---

Summary

Metric	seq	nseq
Files solved (sat/unsat)	274	273
Timeouts	18	25
Unknown	7	1
Median solve time (solved files)	10 ms	10 ms
Mean solve time (solved files)	43 ms	33 ms
Disagreements (sat≠unsat)	—	1

Both solvers perform well. On files both can solve, nseq is slightly faster on average (33 ms vs. 43 ms). Median solve time is identical at 10 ms.

---

Performance Comparison

seq-fast / nseq-slow (seq < 2 s, nseq timed out) — 11 files

File	seq (ms)	nseq (ms)	seq result
concat_backjump_bug.smt2	74	4048	sat
parikh-constraints.smt2	20	4017	sat
word-equation-3.smt2	127	4013	unsat
contains-4.smt2	9	4011	unsat
str-lt.smt2	85	4011	sat
str-leq5.smt2	71	4010	sat
str.to_int_5.smt2	178	4008	sat
prefix-suffix.smt2	9	4006	unsat
str.from_int_6.smt2	54	4006	sat
str.to_int_6.smt2	142	4006	sat
cvc_replace_28.smt2	3505	4005	sat

nseq gaps: str.to_int/str.from_int, string ordering predicates (str.<, str.<=), Parikh-style length constraints, prefix/suffix/contains.

nseq-fast / seq-slow (nseq < 2 s, seq timed out) — 7 files

File	seq (ms)	nseq (ms)	nseq result
str.to_int_4.smt2	4018	10	unsat
noodles-unsat3.smt2	4011	31	unsat
concat-regex2.smt2	4010	11	unsat
nonlinear.smt2	4009	28	unsat
indexof-2.smt2	4008	387	unsat
bigSubstrIdx.smt2	4013	445	sat
regexdeep.smt2	4006	1481	sat

nseq wins on: nonlinear word equations, concat+regex, deep regex, and some indexof/str.to_int variants.

---

Correctness

⚠️ 1 DISAGREEMENT — potential soundness bug in nseq

File	seq	nseq
indexof_const_index_sat.smt2	sat	unsat

The benchmark (annotated status sat) asserts a ∈ {"hhhbbb", "bhhh"} and str.indexof(a, "hhh", 0) = 1. For a = "bhhh", indexof is 1 — satisfiable. seq is correct; nseq returning unsat is a bug in its str.indexof handling.

---

Raw Data (selected rows)

Interesting cases CSV (click to expand)

file,seq_result,seq_time_ms,nseq_result,nseq_time_ms
artur-unsat-we.smt2,timeout,4006,timeout,4021
artur-unsat.smt2,timeout,4009,timeout,4032
bigSubstrIdx.smt2,timeout,4013,sat,445
bug-58-replace-re.smt2,unknown,9,sat,10
concat-regex2.smt2,timeout,4010,unsat,11
concat-regex4.smt2,sat,3723,timeout,4014
concat_backjump_bug.smt2,sat,74,timeout,4048
contains-4.smt2,unsat,9,timeout,4011
contains-7.smt2,unknown,18,timeout,4013
contains-8.smt2,unknown,10,sat,10
cvc_replace_28.smt2,sat,3505,timeout,4005
cvc_replace_4062.smt2,sat,68,timeout,4005
indexof-2.smt2,timeout,4008,unsat,387
indexof_const_index_sat.smt2,sat,26,unsat,145
nikolai-sat.smt2,sat,680,sat,30
nikolai-unsat.smt2,timeout,4005,timeout,4014
nonlinear.smt2,timeout,4009,unsat,28
noodles-unsat.smt2,timeout,4030,timeout,4011
noodles-unsat2.smt2,timeout,4030,timeout,4008
noodles-unsat3.smt2,timeout,4011,unsat,31
noodles-unsat5.smt2,timeout,4006,timeout,4030
noodles-unsat6.smt2,timeout,4016,timeout,4032
noodles-unsat7.smt2,timeout,4011,timeout,4032
noodles-unsat8.smt2,timeout,4008,timeout,4025
noodles-unsat9.smt2,timeout,4006,timeout,4019
parikh-constraints.smt2,sat,20,timeout,4017
pcp-1.smt2,unknown,19,sat,206
prefix-suffix.smt2,unsat,9,timeout,4006
regexdeep.smt2,timeout,4006,sat,1481
replace-length-2.smt2,sat,75,sat,793
str-leq5.smt2,sat,71,timeout,4010
str-leq7.smt2,sat,26,sat,125
str-lt.smt2,sat,85,timeout,4011
str-lt2.smt2,unsat,57,unsat,710
str.from_int_6.smt2,sat,54,timeout,4006
str.to_int_4.smt2,timeout,4018,unsat,10
str.to_int_5.smt2,sat,178,timeout,4008
str.to_int_6.smt2,sat,142,timeout,4006
substring-bug2.smt2,timeout,4006,timeout,4006
word-equation-3.smt2,unsat,127,timeout,4013

---

To reproduce: build Z3 from c3 and run z3 smt.string_solver=seq|nseq -T:10 <file.smt2>.

Generated by QF_S String Solver Benchmark · sonnet46 3.5M · ◷

• expires on Jun 18, 2026, 2:21 PM UTC

[github-actions[bot]]

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

A newer discussion is available at Discussion #9832.