Z3str4 is an SMT solver for the SMT-LIB theory of strings based on Z3. The solver includes two new algorithms for string solving: a length abstraction algorithm and an abstraction-refinement reduction to bit-vectors. Z3str4 also includes an algorithm selection architecture which chooses the best algorithms to run based on their expected performance on the input. This page contains information on downloading and using Z3str4, as well as the results of an extensive experimental evaluation against other leading string solvers.

Z3str4 String Solver

This website consists of supplementary material to our paper (currently under submission). We share the following components presented in our corresponding paper:

Reproduction package - Download

Untar the package by executing tar xf fm.tar.gz which will create a folder called FM.

Compiling Z3str4

We include a bash script named compileZ3str4.sh which compiles the provided source code. To compile the solver you simply have to execute

bash compileZ3str4.sh

Now Z3str4 is compiled within tool_source/build and ready to run.

Running Z3str4:

Z3str4 is invoked from the command line with ./z3 smt.string_solver=z3str3 unicode=false smt.str.tactic=3probe smt.arith.solver=2 inputFile.smt where inputFile.smt is the desired SMT-LIB instance, the parameter dump_models asks Z3 to output the found model (if it answers SAT).

Simple Example

Using Z3str4 to solve the string constraint x0 = x1 . x2 and x0 = solution is as simple as providing the instance below to Z3str4.

(set-logic QF_S)
(declare-fun x0 () String)
(declare-fun x1 () String)
(declare-fun x2 () String)
(assert (= x0 (str.++ x1 x2)))
(assert (= x0 "solution"))
(check-sat)

As can be seen from the output below, Z3str4 finds a solution to the equation where it sets x0 = solution, and x1 and x2 are set to the empty string.

sat
(model
(define-fun x0 () String
"solution")
(define-fun x1 () String
"")
(define-fun x2 () String
"")
)

Trying the different features of Z3str4

The following information is given inside the help command of Z3str4. The selection corresponds to the newly added parameters directly related to our presented work. The following parameters require the choice of using Z3str3 as the main solver for string constraints. Simply pass smt.string_solver=z3str3 to your binary to enable it.

Using algorithms in isolation

str.tactic (unsigned int)

This option changes which algorithms (resp. arms) are used.

3probe all algorithms as presented in the paper
regex only use the regex arm
seq only use the sequence solver arm
alwayscf only use the conjunctive fragment arm
nevercf only use the non-conjunctive fragment arm

Use one of the following parameters to run a single solver within Z3str4

las length abstraction,
arr arrangement solver
seqsequence solver

Using the constraint sharing between arms

str.share_constraints (bool)

Enable constraint sharing across tactics (Z3str3 only, has no effect outside of portfolio tactic) (default: true)

Competing string solvers

As describe in the corresponding paper we are comparing our approach against Z3Seq, Z3Str3, and CVC4.

Z3 Sequence Solver

The Z3 theorem prover is a DPLL(T)-based SMT solver for theory combinations over first-order logic. Z3 includes an arithmetic solver for linear integer arithmetic and a sequence solver (Z3Seq) that supports word-based reasoning about strings.

Z3Str3 String Solver

The Z3str3 solver is based on Z3. It uses a reduction known as the arrangement technique to convert word equations into simpler formulas until a "solved form" is reached.

CVC4 String Solver

The CVC4 solver handles constraints over the theory of strings and arithmetic using an algebraic approach, and uses a similar DPLL(T) architecture to Z3.

Availability

Within the comparison we used CVC4’s binary version 1.8 which is available at here. The sequence solver and Z3str3 were pulled from their official GIT repository. We used commit #7e7360dd0c04cdee95c3f74a59908209742c5212 of Z3. All pre compiled binaries are included within our reproduction package (FM/SolverBinaries).

Reproduction of our Results

Warning

This benchmark tool was tested on Python 3.9.

Install the prerequisites

To install the required packages we provide a script called installTools.sh. Executing bash installTools.sh installs all dependencies needed for running our solver and reproducing our empirical evaluation.

In order to reproduce the figures presented in the paper you need a LaTeX environment. The following command downloads the required packages for Ubuntu like systems

sudo -S apt-get -y install latexmk texlive-latex-recommended texlive-latex-extra texlive-fonts-extra asciidoctor

These packages are not needed to reproduce our results.

Repeating the run using all solvers on all presented benchmarks (including the bit-vector experiment and clause-sharing):

bash runAll.sh

Repeating the run including the fragment analysis:

bash runFragment.sh

After the ZaligVinder run has finished a webserver is started. You can review the results by guiding your browser to http://localhost:8081.

Further post analysis steps

Within the ZaligVinder folder zaligvinder we stored the database of our experimental evaluation.

Inspecting the results within the web browser:

Execute the following commands to review our results within ZaligVinder’s web gui:

cd zaligvinder
python3 startwebserver.py fm_all.db

Afterwards navigate to http://localhost:8081 in your web browser.

Generate an tables, plots and ASCII Doctor web page to review the results:

Execute the following commands

cd zaligvinder
python3 tablegen.py

which will open a terminal gui. Select fm_all.db as database and a place to store the output file — entering no output name stores the output data within the folder zaligvinder/external_data/<today’s_date>. Afterwards you are able to select the benchmark sets of your choice being present within our run and the solvers. Bye selecting the database fm_frag.db you are able to explore the fragment experiment.

Next step is selecting whether you want to generate the cactus plots, tables or the ASCII Doctor page.

Tables and Plots.

Tables and plots need to be compiled by using latexmk. Simply execute

latexmk -pdf <yourFileName>

to generate a PDF.

Generating HTML for the ASCII doctor page.

To view the ASCII Doctor page conveniently in your browser execute

asciidoctor <yourFileName>

which will create a <yourFileName>.html file. To open firefox execute firefox <yourFileName>.html.

You can perform these post analysis steps on your own generated database too. To do so instead of using fm_all.db within the terminal gui simply select your own generated database having a name similar to All_results_1611768687.585239.db for running the experiment on all benchmarks or Fragments_results_1611768687.585239.db if you selected the fragments experiment.

A detailed view on our Results

All tests were performed on a server running Ubuntu 18.04.3 LTS with 2 Intel Xeon Gold 6242 CPUs each having 16 cores and 1.5 TB of memory.

Benchmark Results

General Experiment

PyEx

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
CVC4	24777 (31.96)	11003	13774	0	0	0	644	33671284	25421	24777	20791284	7911284
Z3str4	24483 (1.46)	10789	13694	37	0	0	901	52372918	25421	24520	32872918	14852918
Z3str4-seq	24409 (0.11)	10723	13686	35	0	0	977	55563330	25421	24444	34623330	15083330
Z3seq	24099 (2.24)	10380	13719	2	0	0	1320	76784822	25421	24101	50304822	23904822
Z3str4-regex	21914 (0.34)	8207	13707	17	0	0	3490	143397636	25421	21931	72917636	3117636
Z3str4-nevercf	21866 (0.0)	8159	13707	21	0	0	3534	145291844	25421	21887	73771844	3091844
Z3str4-alwayscf	16006 (21.98)	2323	13683	2039	0	130	7376	381003345	25421	18045	151923345	4403345
Z3str3	14901 (0.34)	1151	13750	2	0	0	10518	421730508	25421	14903	211290508	930508
Z3str4-arr	14848 (0.0)	1143	13705	240	0	0	10333	425001881	25421	15088	208741881	2081881
Z3str4-virtualBestSolver	24713 (-)	11005	13708	182	0	0	526	40605271	25421	24895	23216571	12285271

Note	CVC4 had the biggest lead with 1.01 and CVC4 hat the largest contribution with 31.96. Other solvers contributed as follows: Z3str4-alwayscf: 21.98,Z3seq: 2.24,Z3str4: 1.46,Z3str4-regex: 0.34,Z3str3: 0.34,Z3str4-seq: 0.11,Z3str4-arr: 0.0,Z3str4-nevercf: 0.0.

SMTLIB25

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-regex	5478 (0.81)	1905	3573	79	0	0	356	19368328	5913	5557	9088328	1968328
Z3str4-nevercf	5477 (0.46)	1894	3583	68	0	0	368	19285544	5913	5545	9205544	1845544
Z3str4	5463 (0.23)	1869	3594	6	0	0	444	19503735	5913	5469	10383735	1503735
CVC4	5462 (9.69)	1854	3608	1	0	0	450	19325827	5913	5463	10285827	1285827
Z3seq	5427 (1.38)	1879	3548	0	0	0	486	19849425	5913	5427	10129425	409425
Z3str4-arr	5302 (0.58)	1800	3502	77	0	0	534	25715170	5913	5379	11955170	1275170
Z3str4-seq	5290 (0.58)	1741	3549	10	0	0	613	26470630	5913	5300	13810630	1550630
Z3str4-alwayscf	5285 (0.12)	1777	3508	59	0	9	569	26440910	5913	5344	12700910	1320910
Z3str3	5302 (0.35)	1774	3529	99	1	0	511	25019511	5913	5402	10699511	479511
Z3str4-virtualBestSolver	5563 (-)	1943	3620	81	0	0	269	15515984	5913	5644	7447864	1515984

Note	Z3str4-regex had the biggest lead with 1.0 and CVC4 hat the largest contribution with 9.69. Other solvers contributed as follows: Z3seq: 1.38,Z3str4-regex: 0.81,Z3str4-arr: 0.58,Z3str4-seq: 0.58,Z3str4-nevercf: 0.46,Z3str3: 0.35,Z3str4: 0.23,Z3str4-alwayscf: 0.12.

Pisa

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
CVC4	12 (0.0)	8	4	0	0	0	0	2363	12	12	2363	2363
Z3str3	11 (0.0)	7	4	0	0	0	1	40705	12	11	20705	705
Z3str4	8 (0.0)	8	0	0	0	0	4	160583	12	8	80583	583
Z3str4-seq	8 (0.0)	8	0	0	0	0	4	160718	12	8	80718	718
Z3str4-nevercf	8 (0.0)	8	0	0	0	0	4	160761	12	8	80761	761
Z3str4-regex	8 (0.0)	8	0	0	0	0	4	160787	12	8	80787	787
Z3seq	8 (0.0)	8	0	0	0	0	4	160813	12	8	80813	813
Z3str4-alwayscf	7 (0.0)	7	0	0	0	0	5	201446	12	7	101446	1446
Z3str4-arr	6 (0.0)	6	0	0	0	0	6	240335	12	6	120335	335
Z3str4-virtualBestSolver	8 (-)	8	0	0	0	0	4	160569	12	8	80569	569

Note	CVC4 had the biggest lead with 1.09 and Z3str4-arr hat the largest contribution with 0.0. Other solvers contributed as follows: CVC4: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

Norn

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	954 (0.0)	712	242	0	0	0	73	3027248	1027	954	1567248	107248
Z3str4-regex	954 (0.0)	712	242	0	0	0	73	3033649	1027	954	1573649	113649
Z3str4-nevercf	954 (0.0)	712	242	0	0	0	73	3034548	1027	954	1574548	114548
CVC4	932 (2.9)	710	222	0	0	0	95	3987855	1027	932	2087855	187855
Z3str4-seq	909 (0.0)	712	197	0	0	0	118	4768619	1027	909	2408619	48619
Z3seq	907 (0.0)	712	195	0	0	0	120	4896291	1027	907	2496291	96291
Z3str4-arr	883 (0.0)	693	190	0	0	0	144	5805341	1027	883	2925341	45341
Z3str4-alwayscf	880 (0.7)	693	187	31	0	6	116	5963598	1027	911	2403598	83598
Z3str3	653 (0.0)	510	143	0	0	0	374	14988522	1027	653	7508522	28522
Z3str4-virtualBestSolver	960 (-)	712	248	9	0	0	58	2758293	1027	969	1244077	78293

Note	Z3str4 had the biggest lead with 1.0 and CVC4 hat the largest contribution with 2.9. Other solvers contributed as follows: Z3str4-alwayscf: 0.7,Z3str4-arr: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3seq: 0.0,Z3str4: 0.0.

Trau Light

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-regex	98 (0.0)	4	94	1	0	0	1	92966	100	99	32966	12966
Z3str4-nevercf	98 (0.0)	4	94	1	0	0	1	93787	100	99	33787	13787
CVC4	98 (0.0)	4	94	0	0	0	2	82180	100	98	42180	2180
Z3str4-seq	98 (0.0)	4	94	0	0	0	2	86661	100	98	46661	6661
Z3seq	98 (0.0)	4	94	0	0	0	2	87527	100	98	47527	7527
Z3str4-arr	97 (0.0)	4	93	1	0	0	2	133050	100	98	53050	13050
Z3str4	97 (0.0)	4	93	0	0	0	3	124388	100	97	64388	4388
Z3str4-alwayscf	97 (0.0)	4	93	0	0	0	3	125660	100	97	65660	5660
Z3str3	97 (0.0)	4	93	0	0	0	3	127363	100	97	67363	7363
Z3str4-virtualBestSolver	98 (-)	4	94	1	0	0	1	83247	100	99	29427	3247

Note	Z3str4-regex had the biggest lead with 1.0 and Z3str4-arr hat the largest contribution with 0.0. Other solvers contributed as follows: CVC4: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

Leetcode Strings

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
CVC4	2661 (0.0)	850	1811	0	0	0	0	129591	2661	2661	129591	129591
Z3seq	2661 (0.0)	850	1811	0	0	0	0	165675	2661	2661	165675	165675
Z3str4-seq	2658 (0.0)	847	1811	0	0	0	3	307091	2661	2658	247091	187091
Z3str4	2657 (0.0)	846	1811	1	0	0	3	312633	2661	2658	212633	152633
Z3str4-regex	2654 (0.0)	843	1811	0	0	0	7	456843	2661	2654	316843	176843
Z3str4-nevercf	2654 (0.0)	843	1811	0	0	0	7	460782	2661	2654	320782	180782
Z3str4-alwayscf	2526 (0.0)	715	1811	33	0	0	102	5590085	2661	2559	2230085	190085
Z3str4-arr	2517 (0.0)	706	1811	14	0	0	130	5962291	2661	2531	2802291	202291
Z3str3	2401 (0.0)	590	1811	126	0	0	134	10580725	2661	2527	2860725	180725
Z3str4-virtualBestSolver	2658 (-)	847	1811	0	0	0	3	279949	2661	2658	219949	159949

Note	CVC4 had the biggest lead with 1.0 and Z3str4-arr hat the largest contribution with 0.0. Other solvers contributed as follows: CVC4: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

IBM Appscan

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
CVC4	8 (0.0)	8	0	0	0	0	0	7967	8	8	7967	7967
Z3str4-seq	8 (0.0)	8	0	0	0	0	0	14710	8	8	14710	14710
Z3seq	6 (0.0)	6	0	0	0	0	2	87342	8	6	47342	7342
Z3str4-alwayscf	5 (0.0)	5	0	0	0	0	3	120484	8	5	60484	484
Z3str4-arr	5 (0.0)	5	0	0	0	0	3	120506	8	5	60506	506
Z3str4	5 (0.0)	5	0	0	0	0	3	121421	8	5	61421	1421
Z3str4-regex	5 (0.0)	5	0	0	0	0	3	121472	8	5	61472	1472
Z3str4-nevercf	5 (0.0)	5	0	0	0	0	3	121580	8	5	61580	1580
Z3str3	5 (0.0)	5	0	0	0	0	3	129763	8	5	69763	9763
Z3str4-virtualBestSolver	8 (-)	8	0	0	0	0	0	12907	8	8	12907	12907

Note	CVC4 had the biggest lead with 1.0 and Z3str4-arr hat the largest contribution with 0.0. Other solvers contributed as follows: CVC4: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

Sloth

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
CVC4	24 (0.11)	10	14	0	0	0	0	498	24	24	498	498
Z3str4	23 (0.0)	10	13	0	0	0	1	41033	24	23	21033	1033
Z3str4-seq	23 (0.0)	10	13	0	0	0	1	41188	24	23	21188	1188
Z3str4-regex	23 (0.0)	10	13	0	0	0	1	41433	24	23	21433	1433
Z3str4-alwayscf	23 (0.0)	10	13	0	0	0	1	41485	24	23	21485	1485
Z3str4-nevercf	23 (0.0)	10	13	0	0	0	1	41521	24	23	21521	1521
Z3str4-arr	23 (0.0)	10	13	0	0	0	1	41610	24	23	21610	1610
Z3seq	23 (0.0)	10	13	0	0	0	1	41658	24	23	21658	1658
Z3str3	19 (0.0)	9	10	0	0	0	5	201312	24	19	101312	1312
Z3str4-virtualBestSolver	23 (-)	10	13	0	0	0	1	40922	24	23	20922	922

Note	CVC4 had the biggest lead with 1.04 and CVC4 hat the largest contribution with 0.11. Other solvers contributed as follows: Z3str4-arr: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

Woorpje Word Equations

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-seq	786 (0.23)	622	164	0	0	0	23	1112740	809	786	652740	192740
CVC4	783 (0.23)	619	164	0	0	0	26	1249396	809	783	729396	209396
Z3seq	768 (0.0)	604	164	0	0	0	41	1822419	809	768	1002419	182419
Z3str4-alwayscf	727 (0.0)	563	164	0	0	0	82	3353284	809	727	1713284	73284
Z3str4	727 (0.0)	563	164	0	0	0	82	3354318	809	727	1714318	74318
Z3str4-regex	771 (0.0)	607	166	8	2	0	28	1857227	809	781	697227	137227
Z3str4-nevercf	771 (0.0)	607	167	8	3	0	27	1958551	809	782	678551	138551
Z3str4-arr	687 (0.0)	523	172	11	8	0	103	5819968	809	706	2199968	139968
Z3str3	685 (0.0)	522	171	14	8	0	102	5925016	809	707	2205016	165016
Z3str4-virtualBestSolver	787 (-)	623	164	6	0	0	16	994883	809	793	471521	114883

Note	Z3str4-seq had the biggest lead with 1.0 and CVC4 hat the largest contribution with 0.23. Other solvers contributed as follows: Z3str4-seq: 0.23,Z3str4-arr: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

Kaluza

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	46526 (0.45)	34539	11987	99	0	0	659	34304368	47284	46625	17164368	3984368
Z3str4-alwayscf	46507 (0.0)	34519	11988	30	0	0	747	34737117	47284	46537	18597117	3657117
Z3str4-regex	46432 (6.16)	34446	11986	120	0	0	732	40174612	47284	46552	20734612	6094612
Z3str4-nevercf	46422 (4.92)	34437	11985	134	0	0	728	40779971	47284	46556	20859971	6299971
Z3str3	46102 (2.8)	34303	11799	215	0	0	967	51598350	47284	46317	23658350	4318350
Z3str4	45444 (0.67)	33458	11986	64	0	0	1776	79420496	47284	45508	41340496	5820496
Z3seq	45431 (0.0)	33787	11644	0	0	0	1853	78476060	47284	45431	41416060	4356060
Z3str4-seq	45251 (0.0)	33452	11799	0	0	0	2033	86761363	47284	45251	46101363	5441363
CVC4	44215 (0.0)	32389	11826	0	0	0	3069	132038767	47284	44215	70658767	9278767
Z3str4-virtualBestSolver	46862 (-)	34874	11988	139	0	0	283	20937152	47284	47001	10995496	4057152

Note	Z3str4-arr had the biggest lead with 1.0 and Z3str4-regex hat the largest contribution with 6.16. Other solvers contributed as follows: Z3str4-nevercf: 4.92,Z3str3: 2.8,Z3str4: 0.67,Z3str4-arr: 0.45,CVC4: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0.

StringFuzz

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-alwayscf	1004 (0.0)	702	302	0	0	0	61	2738984	1065	1004	1518984	298984
Z3str4-regex	938 (0.0)	715	223	17	0	0	110	6395416	1065	955	3515416	1315416
Z3str4-nevercf	937 (0.0)	714	223	17	0	0	111	6460086	1065	954	3560086	1340086
Z3str4-arr	890 (0.0)	662	228	0	0	0	175	7388595	1065	890	3888595	388595
Z3str3	792 (0.0)	606	186	3	0	0	270	11181513	1065	795	5661513	261513
CVC4	741 (0.0)	490	251	0	0	0	324	14167509	1065	741	7687509	1207509
Z3str4	714 (0.0)	412	302	45	0	0	306	14595111	1065	759	6675111	555111
Z3seq	567 (0.0)	354	213	43	0	0	455	20790128	1065	610	9970128	870128
Z3str4-seq	566 (0.0)	354	212	43	0	0	456	20714495	1065	609	9874495	754495
Z3str4-virtualBestSolver	1058 (-)	756	302	0	0	0	7	564989	1065	1058	424989	284989

Note	Z3str4-alwayscf had the biggest lead with 1.07 and Z3str4-arr hat the largest contribution with 0.0. Other solvers contributed as follows: CVC4: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

z3Str3 Regression

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
CVC4	242 (0.0)	196	46	0	0	0	0	6288	242	242	6288	6288
Z3str4-alwayscf	242 (0.0)	196	46	0	0	0	0	12559	242	242	12559	12559
Z3str4-regex	242 (0.0)	196	46	0	0	0	0	19352	242	242	19352	19352
Z3str4-nevercf	242 (0.0)	196	46	0	0	0	0	20729	242	242	20729	20729
Z3str3	238 (0.0)	194	44	1	0	0	3	172650	242	239	72650	12650
Z3str4-arr	238 (0.0)	192	46	0	0	0	4	170959	242	238	90959	10959
Z3str4	233 (0.0)	196	37	0	0	0	9	367287	242	233	187287	7287
Z3str4-seq	233 (0.0)	196	37	0	0	0	9	369399	242	233	189399	9399
Z3seq	232 (0.0)	195	37	0	0	0	10	414648	242	232	214648	14648
Z3str4-virtualBestSolver	242 (-)	196	46	0	0	0	0	8591	242	242	8591	8591

Note	CVC4 had the biggest lead with 1.0 and Z3str4-arr hat the largest contribution with 0.0. Other solvers contributed as follows: CVC4: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

Cashew

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-alwayscf	394 (0.0)	382	12	0	0	0	0	16588	394	394	16588	16588
Z3str4-arr	394 (0.0)	382	12	0	0	0	0	17067	394	394	17067	17067
Z3str4	394 (0.0)	382	12	0	0	0	0	22184	394	394	22184	22184
Z3str4-nevercf	394 (0.0)	382	12	0	0	0	0	25939	394	394	25939	25939
Z3str3	394 (0.0)	382	12	0	0	0	0	31303	394	394	31303	31303
Z3str4-regex	393 (0.0)	381	12	0	0	0	1	64193	394	393	44193	24193
Z3str4-seq	391 (0.0)	379	12	0	0	0	3	168054	394	391	108054	48054
Z3seq	387 (0.0)	375	12	0	0	0	7	311243	394	387	171243	31243
CVC4	378 (0.0)	366	12	0	0	0	16	678968	394	378	358968	38968
Z3str4-virtualBestSolver	394 (-)	382	12	0	0	0	0	13142	394	394	13142	13142

Note	Z3str4-alwayscf had the biggest lead with 1.0 and Z3str4-arr hat the largest contribution with 0.0. Other solvers contributed as follows: CVC4: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

JOACO

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
CVC4	94 (0.0)	73	21	0	0	0	0	10979	94	94	10979	10979
Z3str4	94 (0.0)	73	21	0	0	0	0	31331	94	94	31331	31331
Z3str4-regex	94 (0.0)	73	21	0	0	0	0	31381	94	94	31381	31381
Z3str4-nevercf	94 (0.0)	73	21	0	0	0	0	31548	94	94	31548	31548
Z3str4-seq	94 (0.0)	73	21	0	0	0	0	62700	94	94	62700	62700
Z3seq	94 (0.0)	73	21	0	0	0	0	67521	94	94	67521	67521
Z3str4-arr	37 (0.0)	17	20	57	0	0	0	2284465	94	94	4465	4465
Z3str4-alwayscf	37 (0.0)	17	20	57	0	0	0	2285500	94	94	5500	5500
Z3str3	37 (0.0)	17	20	57	0	0	0	2285867	94	94	5867	5867
Z3str4-virtualBestSolver	94 (-)	73	21	0	0	0	0	14374	94	94	14374	14374

Note	CVC4 had the biggest lead with 1.0 and Z3str4-arr hat the largest contribution with 0.0. Other solvers contributed as follows: CVC4: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

Stranger

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str3	4 (0.0)	4	0	0	0	0	0	246	4	4	246	246
Z3str4-arr	4 (0.0)	4	0	0	0	0	0	294	4	4	294	294
Z3str4-alwayscf	4 (0.0)	4	0	0	0	0	0	338	4	4	338	338
CVC4	4 (0.0)	4	0	0	0	0	0	677	4	4	677	677
Z3str4-nevercf	4 (0.0)	4	0	0	0	0	0	4315	4	4	4315	4315
Z3str4-regex	4 (0.0)	4	0	0	0	0	0	4315	4	4	4315	4315
Z3str4	4 (0.0)	4	0	0	0	0	0	4317	4	4	4317	4317
Z3seq	4 (0.0)	4	0	0	0	0	0	9745	4	4	9745	9745
Z3str4-seq	4 (0.0)	4	0	0	0	0	0	10721	4	4	10721	10721
Z3str4-virtualBestSolver	4 (-)	4	0	0	0	0	0	338	4	4	338	338

Note	Z3str3 had the biggest lead with 1.0 and Z3str4-arr hat the largest contribution with 0.0. Other solvers contributed as follows: CVC4: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

Kausler

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3seq	118 (0.11)	118	0	0	0	0	2	108625	120	118	68625	28625
Z3str4-seq	117 (0.0)	117	0	0	0	0	3	157238	120	117	97238	37238
CVC4	117 (0.0)	117	0	0	0	0	3	161353	120	117	101353	41353
Z3str4-regex	115 (0.0)	115	0	0	0	0	5	256434	120	115	156434	56434
Z3str4-nevercf	115 (0.0)	115	0	0	0	0	5	256676	120	115	156676	56676
Z3str3	99 (0.0)	99	0	0	0	0	21	846127	120	99	426127	6127
Z3str4-arr	79 (0.0)	79	0	5	0	0	36	1772295	120	84	852295	132295
Z3str4	78 (0.0)	78	0	7	0	0	35	1845602	120	85	865602	165602
Z3str4-alwayscf	78 (0.0)	78	0	7	0	0	35	1855913	120	85	875913	175913
Z3str4-virtualBestSolver	117 (-)	117	0	0	0	0	3	156744	120	117	96744	36744

Note	Z3seq had the biggest lead with 1.01 and Z3seq hat the largest contribution with 0.11. Other solvers contributed as follows: Z3str4-arr: 0.0,CVC4: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3str4: 0.0.

BanditFuzz

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
CVC4	346 (0.78)	63	283	0	0	0	11	561044	357	346	341044	121044
Z3str4-nevercf	343 (0.0)	51	292	0	0	0	14	586328	357	343	306328	26328
Z3str4	343 (0.0)	53	290	0	0	0	14	592769	357	343	312769	32769
Z3str4-regex	341 (0.0)	49	292	0	0	0	16	661688	357	341	341688	21688
Z3str4-seq	341 (0.0)	51	290	1	0	0	15	686748	357	342	346748	46748
Z3seq	338 (0.0)	47	291	0	0	0	19	822453	357	338	442453	62453
Z3str4-alwayscf	310 (0.0)	25	285	5	0	0	42	1922081	357	315	882081	42081
Z3str3	307 (0.0)	20	287	0	0	0	50	2052628	357	307	1052628	52628
Z3str4-arr	299 (0.0)	14	285	5	0	0	53	2371549	357	304	1111549	51549
Z3str4-virtualBestSolver	347 (-)	55	292	1	0	0	9	436301	357	348	233599	36301

Note	CVC4 had the biggest lead with 1.01 and CVC4 hat the largest contribution with 0.78. Other solvers contributed as follows: Z3str4-arr: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

automatark25

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	19925 (0.0)	14465	5460	0	0	0	54	4703025	19979	19925	3623025	2543025
Z3str4-regex	19925 (0.0)	14465	5460	0	0	0	54	4783855	19979	19925	3703855	2623855
Z3str4-nevercf	19925 (0.0)	14465	5460	0	0	0	54	4790189	19979	19925	3710189	2630189
Z3str4-arr	19816 (0.0)	14437	5379	0	0	0	163	7921911	19979	19816	4661911	1401911
Z3str4-seq	19771 (0.0)	14362	5409	0	0	0	208	14172592	19979	19771	10012592	5852592
Z3seq	19677 (0.0)	14344	5333	5	0	0	297	18048226	19979	19682	11908226	5968226
CVC4	19456 (3.34)	14166	5290	0	0	0	523	23113768	19979	19456	12653768	2193768
Z3str3	16247 (0.11)	11836	4411	431	0	0	3301	158825397	19979	16678	75565397	9545397
Z3str4-alwayscf	19652 (0.0)	14373	5280	240	1	96	86	14717002	19979	19893	3257002	1537002
Z3str4-virtualBestSolver	19930 (-)	14468	5462	35	0	0	14	2946679	19979	19965	1292662	986679

Note	Z3str4 had the biggest lead with 1.0 and CVC4 hat the largest contribution with 3.34. Other solvers contributed as follows: Z3str3: 0.11,Z3str4-arr: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

stringfuzzregexgenerated

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	4114 (0.0)	3284	830	10	0	0	46	8199002	4170	4124	6879002	5959002
Z3str4-regex	4114 (0.0)	3284	830	5	0	0	51	8535619	4170	4119	7315619	6295619
Z3str4-arr	4111 (0.0)	3281	830	10	0	0	49	5705209	4170	4121	4325209	3345209
Z3str4-nevercf	4107 (0.0)	3277	830	11	0	0	52	8680432	4170	4118	7200432	6160432
Z3str4-alwayscf	4104 (0.0)	3274	830	11	0	0	55	7042785	4170	4115	5502785	4402785
Z3str3	3316 (0.0)	3284	32	0	0	0	854	37633604	4170	3316	20553604	3473604
Z3str4-seq	2211 (0.11)	1514	697	0	0	0	1959	84287950	4170	2211	45107950	5927950
Z3seq	2172 (0.0)	1475	697	0	0	0	1998	85618191	4170	2172	45658191	5698191
CVC4	1290 (0.0)	835	455	39	0	0	2841	119233019	4170	1329	60853892	4033019
Z3str4-virtualBestSolver	4126 (-)	3296	830	0	0	0	44	5691736	4170	4126	4811736	3931736

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-seq hat the largest contribution with 0.11. Other solvers contributed as follows: Z3str4-arr: 0.0,CVC4: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

stringfuzzregextransformed

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	10679 (0.0)	4631	6048	0	0	0	3	597563	10682	10679	537563	477563
Z3str4-nevercf	10679 (0.0)	4631	6048	0	0	0	3	602193	10682	10679	542193	482193
Z3str4-regex	10679 (0.0)	4631	6048	0	0	0	3	608912	10682	10679	548912	488912
Z3str4-seq	10673 (0.0)	4630	6043	0	0	0	9	890089	10682	10673	710089	530089
Z3str4-alwayscf	10646 (0.0)	4605	6041	15	0	8	21	1786210	10682	10661	766210	346210
CVC4	10643 (0.33)	4621	6022	0	0	0	39	1970815	10682	10643	1190815	410815
Z3str4-arr	10639 (0.0)	4598	6041	6	0	0	37	2031029	10682	10645	1051029	311029
Z3seq	10619 (0.0)	4628	5991	0	0	0	63	3171244	10682	10619	1911244	651244
Z3str3	9242 (0.0)	4346	4896	1	0	0	1439	58348049	10682	9243	29528049	748049
Z3str4-virtualBestSolver	10679 (-)	4631	6048	0	0	0	3	420936	10682	10679	360936	300936

Note	Z3str4 had the biggest lead with 1.0 and CVC4 hat the largest contribution with 0.33. Other solvers contributed as follows: Z3str4-arr: 0.0,Z3str4-regex: 0.0,Z3str4-nevercf: 0.0,Z3str3: 0.0,Z3str4-seq: 0.0,Z3str4-alwayscf: 0.0,Z3seq: 0.0,Z3str4: 0.0.

Total

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	116439 (2.35)	71842	44597	170	0	0	3757	189396964	120366	116609	107456964	32316964
Z3str4-seq	113841 (1.01)	69807	44034	89	0	0	6436	296807036	120366	113930	164527036	35807036
Z3seq	113636 (3.7)	69853	43783	50	0	0	6680	311734056	120366	113686	176134056	42534056
CVC4	112283 (48.93)	68386	43897	40	0	0	8043	350400148	120366	112323	187941021	27080148
Z3str4-alwayscf	108534 (22.73)	64272	44263	2527	1	249	9304	489955374	120366	111062	202655374	16575374
Z3str4-regex	115182 (7.28)	70660	44524	247	2	0	4935	230066118	120366	115431	121206118	22506118
Z3str4-nevercf	115118 (5.37)	70587	44534	260	3	0	4985	232687324	120366	115381	122167324	22467324
Z3str4-arr	107401 (1.01)	63095	44314	525	8	0	12432	532807893	120366	107934	262047893	13407893
Z3str3	100852 (3.58)	59663	41198	949	9	0	18556	801719159	120366	101810	391379159	20259159
Z3str4-virtualBestSolver	118671 (-)	74012	44659	454	0	0	1241	91643007	120366	119125	50996414	23843007

Note	Z3str4 had the biggest lead with 1.02 and CVC4 hat the largest contribution with 48.93. Other solvers contributed as follows: Z3str4-alwayscf: 22.73,Z3str4-regex: 7.28,Z3str4-nevercf: 5.37,Z3seq: 3.7,Z3str3: 3.58,Z3str4: 2.35,Z3str4-arr: 1.01,Z3str4-seq: 1.01.

Fragment Experiment

RegexFragment

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	35046 (3.77)	22840	12206	9	0	0	290	10914204	35345	35055	16702244	10902244
Z3str4-arr	34692 (4.03)	22632	12060	73	0	0	580	5596872	35345	34765	17170752	5570752
Z3str4-seq	32758 (13.33)	20767	11991	9	0	0	2578	13525831	35345	32767	64982351	13422351
Z3str4-las	32603 (1.51)	20762	11842	2727	1	117	14	3807951	35345	35331	3978171	3698171

Note	Z3str4 had the biggest lead with 1.01 and Z3str4-seq hat the largest contribution with 13.33. Other solvers contributed as follows: Z3str4-arr: 4.03,Z3str4: 3.77,Z3str4-las: 1.51.

SeqFragment

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	39680 (7.71)	23227	16453	87	0	0	2755	18104566	42522	39767	73090886	17990886
Z3str4-seq	39639 (0.77)	23187	16452	83	0	0	2800	18680405	42522	39722	74565085	18565085
Z3str4-arr	31376 (303.68)	14937	16439	314	0	0	10832	3882773	42522	31690	220076933	3436933
Z3str4-las	28990 (65.26)	13185	15805	13532	0	141	0	12629361	42522	42522	12088081	12088081

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-arr hat the largest contribution with 303.68. Other solvers contributed as follows: Z3str4-las: 65.26,Z3str4: 7.71,Z3str4-seq: 0.77.

ConjunctiveFragment

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-seq	14647 (37.95)	12115	2532	1	0	0	465	774663	15113	14648	10056023	756023
Z3str4	14631 (3.57)	11954	2677	13	0	0	469	1338043	15113	14644	10698763	1318763
Z3str4-las	14172 (0.0)	11693	2479	941	0	0	0	1127231	15113	15113	1089591	1089591
Z3str4-arr	14471 (3.82)	11887	2592	90	8	0	544	1702357	15113	14569	12555877	1675877

Note	Z3str4-seq had the biggest lead with 1.0 and Z3str4-seq hat the largest contribution with 37.95. Other solvers contributed as follows: Z3str4-arr: 3.82,Z3str4: 3.57,Z3str4-las: 0.0.

NonConjFragment

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	23286 (1.27)	13749	9537	68	0	0	289	1813757	23643	23354	7579477	1799477
Z3str4-arr	23120 (1.52)	13611	9509	51	0	0	472	1185261	23643	23171	10604341	1164341
Z3str4-seq	23081 (0.25)	13740	9341	1	0	0	561	815911	23643	23082	12013431	793431
Z3str4-las	22466 (0.0)	13478	8988	1177	0	0	0	1186235	23643	23643	1139155	1139155

Note	Z3str4 had the biggest lead with 1.01 and Z3str4-arr hat the largest contribution with 1.52. Other solvers contributed as follows: Z3str4: 1.27,Z3str4-seq: 0.25,Z3str4-las: 0.0.

Simple

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-las	3743 (0.0)	27	3716	0	0	0	0	215468	3743	3743	215468	215468
Z3str4	3743 (0.0)	27	3716	0	0	0	0	290379	3743	3743	290379	290379
Z3str4-seq	3743 (0.0)	27	3716	0	0	0	0	305838	3743	3743	305838	305838
Z3str4-arr	3743 (0.0)	27	3716	0	0	0	0	309255	3743	3743	309255	309255

Note	Z3str4-las had the biggest lead with 1.0 and Z3str4 hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4-seq: 0.0,Z3str4-arr: 0.0,Z3str4-las: 0.0.

Total

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	116386 (16.27)	71797	44589	177	0	0	3803	32460949	120366	116563	108361749	32301749
Z3str4-seq	113868 (52.37)	69836	44032	94	0	0	6404	34102648	120366	113962	161922728	33842728
Z3str4-las	101974 (66.1)	59145	42830	18377	1	258	14	18966246	120366	120352	18510466	18230466
Z3str4-arr	107402 (309.89)	63094	44316	528	8	0	12428	12676518	120366	107938	260717158	12157158

Note	Z3str4 had the biggest lead with 1.02 and Z3str4-arr hat the largest contribution with 309.89. Other solvers contributed as follows: Z3str4-las: 66.1,Z3str4-seq: 52.37,Z3str4: 16.27.

Bit-vector integration Experiment

PyEx

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	14848 (6385.12)	1143	13705	240	0	0	10333	425001881	25421	15088	208741881	2081881
Z3str2	5506 (1025.89)	6381	3812	574	4687	0	14654	1277049099	25421	10767	304829099	11749099

Note	Z3str4-arr had the biggest lead with 2.7 and Z3str4-arr hat the largest contribution with 6385.12. Other solvers contributed as follows: Z3str2: 1025.89.

SMTLIB25

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	5302 (140.76)	1800	3502	77	0	0	534	25715170	5913	5379	11955170	1275170
Z3str2	4401 (68.46)	1793	3455	110	847	0	555	146025612	5913	5358	11945612	845612

Note	Z3str4-arr had the biggest lead with 1.2 and Z3str4-arr hat the largest contribution with 140.76. Other solvers contributed as follows: Z3str2: 68.46.

Pisa

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	6 (0.0)	6	0	0	0	0	6	240335	12	6	120335	335
Z3str2	10 (3.0)	7	4	0	1	0	1	180458	12	11	20458	458

Note	Z3str4-arr had the biggest lead with 0.6 and Z3str2 hat the largest contribution with 3.0. Other solvers contributed as follows: Z3str4-arr: 0.0.

Norn

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	883 (71.85)	693	190	0	0	0	144	5805341	1027	883	2925341	45341
Z3str2	756 (0.0)	675	85	0	4	0	267	11289739	1027	760	5389739	49739

Note	Z3str4-arr had the biggest lead with 1.17 and Z3str4-arr hat the largest contribution with 71.85. Other solvers contributed as follows: Z3str2: 0.0.

Trau Light

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str2	97 (0.0)	4	93	1	0	0	2	123366	100	98	43366	3366
Z3str4-arr	97 (0.0)	4	93	1	0	0	2	133050	100	98	53050	13050

Note	Z3str2 had the biggest lead with 1.0 and Z3str2 hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4-arr: 0.0.

Leetcode Strings

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	2517 (87.22)	706	1811	14	0	0	130	5962291	2661	2531	2802291	202291
Z3str2	2067 (16.84)	620	1785	131	338	0	125	57730966	2661	2536	2670966	170966

Note	Z3str4-arr had the biggest lead with 1.22 and Z3str4-arr hat the largest contribution with 87.22. Other solvers contributed as follows: Z3str2: 16.84.

IBM Appscan

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	5 (1.33)	5	0	0	0	0	3	120506	8	5	60506	506
Z3str2	2 (0.0)	4	0	0	2	0	4	440193	8	4	80193	193

Note	Z3str4-arr had the biggest lead with 2.5 and Z3str4-arr hat the largest contribution with 1.33. Other solvers contributed as follows: Z3str2: 0.0.

Sloth

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	23 (2.09)	10	13	0	0	0	1	41610	24	23	21610	1610
Z3str2	19 (0.0)	9	10	0	0	0	5	200673	24	19	100673	673

Note	Z3str4-arr had the biggest lead with 1.21 and Z3str4-arr hat the largest contribution with 2.09. Other solvers contributed as follows: Z3str2: 0.0.

Woorpje Word Equations

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	687 (9.41)	523	172	11	8	0	103	5819968	809	706	2199968	139968
Z3str2	672 (7.64)	521	171	14	20	0	103	7625988	809	706	2205988	145988

Note	Z3str4-arr had the biggest lead with 1.02 and Z3str4-arr hat the largest contribution with 9.41. Other solvers contributed as follows: Z3str2: 7.64.

Kaluza

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	46526 (110.46)	34539	11987	99	0	0	659	34304368	47284	46625	17164368	3984368
Z3str2	41753 (8.45)	34406	11975	39	4628	0	864	687633462	47284	46420	20873462	3593462

Note	Z3str4-arr had the biggest lead with 1.11 and Z3str4-arr hat the largest contribution with 110.46. Other solvers contributed as follows: Z3str2: 8.45.

StringFuzz

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	890 (68.81)	662	228	0	0	0	175	7388595	1065	890	3888595	388595
Z3str2	775 (0.0)	592	183	5	0	0	285	11865466	1065	780	5965466	265466

Note	Z3str4-arr had the biggest lead with 1.15 and Z3str4-arr hat the largest contribution with 68.81. Other solvers contributed as follows: Z3str2: 0.0.

z3Str3 Regression

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	238 (2.28)	192	46	0	0	0	4	170959	242	238	90959	10959
Z3str2	208 (1.14)	195	43	1	30	0	3	4368177	242	239	68177	8177

Note	Z3str4-arr had the biggest lead with 1.14 and Z3str4-arr hat the largest contribution with 2.28. Other solvers contributed as follows: Z3str2: 1.14.

Cashew

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	394 (0.0)	382	12	0	0	0	0	17067	394	394	17067	17067
Z3str2	392 (0.0)	382	12	0	2	0	0	302628	394	394	22628	22628

Note	Z3str4-arr had the biggest lead with 1.01 and Z3str2 hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4-arr: 0.0.

JOACO

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	37 (15.67)	17	20	57	0	0	0	2284465	94	94	4465	4465
Z3str2	20 (0.0)	7	20	67	7	0	0	3665957	94	94	5957	5957

Note	Z3str4-arr had the biggest lead with 1.85 and Z3str4-arr hat the largest contribution with 15.67. Other solvers contributed as follows: Z3str2: 0.0.

Stranger

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	4 (2.0)	4	0	0	0	0	0	294	4	4	294	294
Z3str2	0 (0.0)	0	0	4	0	0	0	160611	4	4	611	611

Note	Z3str4-arr had the biggest lead with 0 and Z3str4-arr hat the largest contribution with 2.0. Other solvers contributed as follows: Z3str2: 0.0.

Kausler

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	79 (0.0)	79	0	5	0	0	36	1772295	120	84	852295	132295
Z3str2	7 (42.86)	119	0	0	112	0	1	15807510	120	119	107510	87510

Note	Z3str4-arr had the biggest lead with 11.29 and Z3str2 hat the largest contribution with 42.86. Other solvers contributed as follows: Z3str4-arr: 0.0.

BanditFuzz

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	299 (3.53)	14	285	5	0	0	53	2371549	357	304	1111549	51549
Z3str2	297 (4.12)	24	286	2	13	0	45	3782843	357	312	982843	82843

Note	Z3str4-arr had the biggest lead with 1.01 and Z3str2 hat the largest contribution with 4.12. Other solvers contributed as follows: Z3str4-arr: 3.53.

automatark25

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	19816 (4026.98)	14437	5379	0	0	0	163	7921911	19979	19816	4661911	1401911
Z3str2	8108 (6.62)	11643	2708	4759	6243	3	869	1101582230	19979	19110	19822230	2442230

Note	Z3str4-arr had the biggest lead with 2.44 and Z3str4-arr hat the largest contribution with 4026.98. Other solvers contributed as follows: Z3str2: 6.62.

stringfuzzregexgenerated

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	4111 (432.18)	3281	830	10	0	0	49	5705209	4170	4121	4325209	3345209
Z3str2	3266 (5.06)	3232	35	0	1	0	903	40084881	4170	3267	21884881	3824881

Note	Z3str4-arr had the biggest lead with 1.26 and Z3str4-arr hat the largest contribution with 432.18. Other solvers contributed as follows: Z3str2: 5.06.

stringfuzzregextransformed

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	10639 (680.74)	4598	6041	6	0	0	37	2031029	10682	10645	1051029	311029
Z3str2	8838 (7.91)	4459	4906	0	527	0	1317	127049304	10682	9365	26929304	589304

Note	Z3str4-arr had the biggest lead with 1.2 and Z3str4-arr hat the largest contribution with 680.74. Other solvers contributed as follows: Z3str2: 7.91.

Total

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-arr	107401 (9252.07)	63095	44314	525	8	0	12432	532807893	120366	107934	262047893	13407893
Z3str2	77194 (731.69)	65073	29583	5707	17462	3	20003	3496969163	120366	100363	423949163	23889163

Note	Z3str4-arr had the biggest lead with 1.39 and Z3str4-arr hat the largest contribution with 9252.07. Other solvers contributed as follows: Z3str2: 731.69.

Clause-sharing Experiment

PyEx

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	24483 (28.54)	10789	13694	37	0	0	901	52372918	25421	24520	32872918	14852918
Z3str4-no-c-sharing	24439 (5.71)	10747	13692	35	0	0	947	54429828	25421	24474	34089828	15149828

Note	Z3str4 had the biggest lead with 1.0 and Z3str4 hat the largest contribution with 28.54. Other solvers contributed as follows: Z3str4-no-c-sharing: 5.71.

SMTLIB25

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-no-c-sharing	5464 (19.89)	1871	3593	4	0	1	445	19435405	5913	5468	10375405	1475405
Z3str4	5463 (19.35)	1869	3594	6	0	0	444	19503735	5913	5469	10383735	1503735

Note	Z3str4-no-c-sharing had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 19.89. Other solvers contributed as follows: Z3str4: 19.35.

Pisa

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	8 (0.0)	8	0	0	0	0	4	160583	12	8	80583	583
Z3str4-no-c-sharing	8 (0.0)	8	0	0	0	0	4	160703	12	8	80703	703

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4: 0.0.

Norn

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	954 (0.0)	712	242	0	0	0	73	3027248	1027	954	1567248	107248
Z3str4-no-c-sharing	954 (0.0)	712	242	0	0	0	73	3031093	1027	954	1571093	111093

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4: 0.0.

Trau Light

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	97 (0.0)	4	93	0	0	0	3	124388	100	97	64388	4388
Z3str4-no-c-sharing	97 (0.0)	4	93	0	0	0	3	124637	100	97	64637	4637

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4: 0.0.

Leetcode Strings

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	2657 (0.0)	846	1811	1	0	0	3	312633	2661	2658	212633	152633
Z3str4-no-c-sharing	2657 (0.0)	846	1811	1	0	0	3	326138	2661	2658	226138	166138

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4: 0.0.

IBM Appscan

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-no-c-sharing	6 (0.67)	6	0	0	0	0	2	82609	8	6	42609	2609
Z3str4	5 (0.0)	5	0	0	0	0	3	121421	8	5	61421	1421

Note	Z3str4-no-c-sharing had the biggest lead with 1.2 and Z3str4-no-c-sharing hat the largest contribution with 0.67. Other solvers contributed as follows: Z3str4: 0.0.

Sloth

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	23 (0.0)	10	13	0	0	0	1	41033	24	23	21033	1033
Z3str4-no-c-sharing	23 (0.0)	10	13	0	0	0	1	41187	24	23	21187	1187

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4: 0.0.

Woorpje Word Equations

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	727 (6.05)	563	164	0	0	0	82	3354318	809	727	1714318	74318
Z3str4-no-c-sharing	725 (4.95)	561	164	0	0	0	84	3435015	809	725	1755015	75015

Note	Z3str4 had the biggest lead with 1.0 and Z3str4 hat the largest contribution with 6.05. Other solvers contributed as follows: Z3str4-no-c-sharing: 4.95.

Kaluza

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-no-c-sharing	45471 (16.64)	33484	11987	60	0	0	1753	79203808	47284	45531	41743808	6683808
Z3str4	45444 (2.6)	33458	11986	64	0	0	1776	79420496	47284	45508	41340496	5820496

Note	Z3str4-no-c-sharing had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 16.64. Other solvers contributed as follows: Z3str4: 2.6.

StringFuzz

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	714 (0.75)	412	302	45	0	0	306	14595111	1065	759	6675111	555111
Z3str4-no-c-sharing	713 (0.0)	411	302	46	0	0	306	14683708	1065	759	6723708	603708

Note	Z3str4 had the biggest lead with 1.0 and Z3str4 hat the largest contribution with 0.75. Other solvers contributed as follows: Z3str4-no-c-sharing: 0.0.

z3Str3 Regression

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	233 (0.0)	196	37	0	0	0	9	367287	242	233	187287	7287
Z3str4-no-c-sharing	233 (0.0)	196	37	0	0	0	9	368294	242	233	188294	8294

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4: 0.0.

Cashew

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	394 (0.0)	382	12	0	0	0	0	22184	394	394	22184	22184
Z3str4-no-c-sharing	394 (0.0)	382	12	0	0	0	0	23527	394	394	23527	23527

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4: 0.0.

JOACO

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	94 (0.0)	73	21	0	0	0	0	31331	94	94	31331	31331
Z3str4-no-c-sharing	94 (0.0)	73	21	0	0	0	0	32194	94	94	32194	32194

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4: 0.0.

Stranger

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	4 (0.0)	4	0	0	0	0	0	4317	4	4	4317	4317
Z3str4-no-c-sharing	4 (0.0)	4	0	0	0	0	0	4321	4	4	4321	4321

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4: 0.0.

Kausler

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	78 (0.0)	78	0	7	0	0	35	1845602	120	85	865602	165602
Z3str4-no-c-sharing	78 (0.0)	78	0	7	0	0	35	1852083	120	85	872083	172083

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4: 0.0.

BanditFuzz

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4-no-c-sharing	344 (0.52)	54	290	0	0	0	13	553746	357	344	293746	33746
Z3str4	343 (0.0)	53	290	0	0	0	14	592769	357	343	312769	32769

Note	Z3str4-no-c-sharing had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.52. Other solvers contributed as follows: Z3str4: 0.0.

automatark25

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	19925 (0.0)	14465	5460	0	0	0	54	4703025	19979	19925	3623025	2543025
Z3str4-no-c-sharing	19925 (0.0)	14465	5460	0	0	0	54	4804125	19979	19925	3724125	2644125

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4: 0.0.

stringfuzzregexgenerated

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	4114 (5.56)	3284	830	10	0	0	46	8199002	4170	4124	6879002	5959002
Z3str4-no-c-sharing	4114 (5.56)	3284	830	6	0	0	50	8517994	4170	4120	7277994	6277994

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 5.56. Other solvers contributed as follows: Z3str4: 5.56.

stringfuzzregextransformed

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	10679 (0.0)	4631	6048	0	0	0	3	597563	10682	10679	537563	477563
Z3str4-no-c-sharing	10679 (0.0)	4631	6048	0	0	0	3	608339	10682	10679	548339	488339

Note	Z3str4 had the biggest lead with 1.0 and Z3str4-no-c-sharing hat the largest contribution with 0.0. Other solvers contributed as follows: Z3str4: 0.0.

Total

Solver	Cor. class. (contr.)	SAT	UNSAT	UNKN	ERR	CRA	TO	Par2	Tot. inst.	Tot. inst. w/o TO	Tot. time	Tot. time w/o TO
Z3str4	116439 (61.45)	71842	44597	170	0	0	3757	189396964	120366	116609	107456964	32316964
Z3str4-no-c-sharing	116422 (52.67)	71827	44595	159	0	1	3785	191718754	120366	116581	109658754	33958754

Note	Z3str4 had the biggest lead with 1.0 and Z3str4 hat the largest contribution with 61.45. Other solvers contributed as follows: Z3str4-no-c-sharing: 52.67.