QF_Equality+Bitvec (Model Validation Track)

Competition results for the QF_Equality+Bitvec division in the Model Validation Track.

Page generated on 2021-07-18 17:31:50 +0000

Benchmarks: 375
Time Limit: 1200 seconds
Memory Limit: 60 GB

Logics:

• QF_UFBV : 375 benchmarks

This division 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
Yices2 model-validation	0	374	2185.384	2186.329		1	0
Bitwuzla	0	374	2616.587	2574.322		1	0
MathSAT5n	0	362	16905.111	16911.378		13	0
cvc5-mv	0	361	26215.782	26219.147		14	0
z3-mvn	0	358	23531.293	23525.065		17	0

Parallel Performance

Solver	Error Score	Correct Score	CPU Time Score	Wall Time Score	Abstained	Timeout	Memout
Yices2 model-validation	0	374	2185.624	2186.309		1	0
Bitwuzla	0	374	2616.957	2574.302		1	0
MathSAT5n	0	362	16909.551	16910.788		13	0
cvc5-mv	0	361	26221.662	26218.607		14	0
z3-mvn	0	358	23534.363	23524.385		17	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.