QF_BV (Model Validation Track (experimental))

Competition results for the QF_BV division in the Model Validation Track (experimental).

Page generated on 2019-07-23 17:57:57 +0000

Benchmarks: 7191
Time Limit: 2400 seconds
Memory Limit: 60 GB

This track is experimental. Solvers are only ranked by performance, but no winner is selected.

Sequential Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Boolector	0	7171	161311.749	161334.219		19	0
CVC4-mv	0	7152	232895.987	232608.291		31	3
Yices 2.6.2 CaDiCal/SMT-LIB2 Models	0	7143	202444.731	202365.79		47	0
Minkeyrink Solver	0	7142	239971.427	239870.732		48	0
Yices 2.6.2 Model Validation	0	7129	282734.621	282739.257		61	0
Yices 2.6.2 New Bvsolver with SMT2 Models	0	7128	241766.842	241786.166		62	0
Minkeyrink Solver MT	0	7103	369834.416	253321.647		87	0
Yices 2.6.2 Cryptominisat/SMT-LIB2 Models	0	7083	374426.859	374118.103		105	0
STP-incremental	0	7009	676626.088	677275.285		179	0
STP-mt	0	0	893242.449	692213.598		254	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Boolector	0	7171	161315.079	161333.589		19	0
CVC4-mv	0	7152	232909.657	232606.841		31	3
Minkeyrink Solver MT	0	7151	506451.066	203284.052		39	0
Yices 2.6.2 CaDiCal/SMT-LIB2 Models	0	7143	202455.451	202363.94		47	0
Minkeyrink Solver	0	7142	239984.177	239869.272		48	0
Yices 2.6.2 Model Validation	0	7129	282747.331	282736.847		61	0
Yices 2.6.2 New Bvsolver with SMT2 Models	0	7128	241779.532	241783.666		62	0
Yices 2.6.2 Cryptominisat/SMT-LIB2 Models	0	7083	374452.909	374113.933		105	0
STP-incremental	0	7009	676666.938	677268.215		179	0
STP-mt	0	0	1122106.179	592689.298		166	0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.