QF_FPLRA (Model Validation Track)

Competition results for the QF_FPLRA logic in the Model Validation Track. Chart

Results were generated on 2026-07-25

Benchmarks: 51
Time Limit: 1200 seconds
Memory Limit: 30720 GB

Winners

Sequential Performance	Parallel Performance	SAT Performance (parallel)	UNSAT Performance (parallel)	24 seconds Performance (parallel)
Bitwuzla	Bitwuzla	Bitwuzla	-	Bitwuzla

Sequential Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
Bitwuzla	51	1240.01	1246.58	51	51	0	0
cvc5	44	550.53	556.07	44	44	7	7
z3-BooledASS ^ne	1 (base -38)	2.61	2.74	1	1	50	10
z3-BooledASS-base ⁿ	39	2617.26	2622.35	39	39	12	2

(base +/- n): for derived solvers: increment over base solver
^ne: not eligible for winning as it does not substantially improve over the base solver (at least 10 % improvement in PAR2 score) ⁿ: non-competing solver

Parallel Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
Bitwuzla	51	1240.01	1246.58	51	51	0	0
cvc5	44	550.53	556.07	44	44	7	7
z3-BooledASS ^ne	1 (base -38)	2.61	2.74	1	1	50	10
z3-BooledASS-base ⁿ	39	2617.26	2622.35	39	39	12	2

SAT Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Timeout
Bitwuzla	51	1240.01	1246.58	51	51	0	0
cvc5	44	550.53	556.07	44	44	7	7
z3-BooledASS ^ne	1 (base -38)	2.61	2.74	1	1	50	10
z3-BooledASS-base ⁿ	39	2617.26	2622.35	39	39	12	2

24 seconds Performance Performance

Solver	Correct Score	CPU Time Score	Wall Time Score	Solved	Solved SAT	Unsolved	Abstained
Bitwuzla	46	10.16	15.91	46	46	0	5
cvc5	41	14.71	19.82	41	41	0	10
z3-BooledASS ^ne	1 (base -20)	2.61	2.74	1	1	25	25
z3-BooledASS-base ⁿ	21	129.07	131.71	21	21	0	30

SMT-COMP 2026