SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

Participants
Results

QF_Equality+BVArith (QF_ABV, QF_UFBV, QF_AUFBV) - Single Query Track

Competition results for the QF_Equality+BVArith (QF_ABV, QF_UFBV, QF_AUFBV) division in the Single Query Track.

Page generated on 2020-01-29 22:04:58 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Yices2Yices2Bitwuzla Yices2 Bitwuzla

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 3594 84216.893 84246.4693594244211524242 0
Yices2-fixedn 0 3594 84416.636 84458.3313594244211524242 0
Bitwuzla 0 3591 39279.56 39298.6663591244311484519 0
Bitwuzla-fixedn 0 3591 39399.656 39374.3473591244311484519 0
MathSAT5n 0 3526 159948.267 159953.645352624091117110109 1
CVC4 0 3517 162592.875 165636.447351724121105119119 0
z3n 0 3489 204669.966 204567.035348923891100147147 0
2019-Boolectorn 0 3369 30976.492 30972.2073369231110581616 0
2019-Par4n 0 3365 69306.186 52921.143365230710582020 0
2019-Yices 2.6.2n 0 235 30011.237 30012.745235137981616 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 3594 84216.893 84246.4693594244211524242 0
Yices2-fixedn 0 3594 84416.636 84458.3313594244211524242 0
Bitwuzla 0 3591 39279.56 39298.6663591244311484519 0
Bitwuzla-fixedn 0 3591 39399.656 39374.3473591244311484519 0
MathSAT5n 0 3526 159948.267 159953.645352624091117110109 1
CVC4 0 3517 162592.875 165636.447351724121105119119 0
z3n 0 3489 204669.966 204567.035348923891100147147 0
2019-Boolectorn 0 3369 30976.492 30972.2073369231110581616 0
2019-Par4n 0 3366 89838.446 31147.693366230810581919 0
2019-Yices 2.6.2n 0 235 30011.237 30012.745235137981616 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla-fixedn 0 2443 6716.142 6700.09244324430119319 0
Bitwuzla 0 2443 6701.521 6705.071244324430119319 0
Yices2 0 2442 21327.899 21339.293244224420119442 0
Yices2-fixedn 0 2442 21326.109 21348.546244224420119442 0
CVC4 0 2412 54991.687 57232.092412241201224119 0
MathSAT5n 0 2409 63560.516 63545.4432409240901227109 1
z3n 0 2389 88494.525 88420.7612389238901247147 0
2019-Boolectorn 0 2311 5497.682 5487.168231123110107416 0
2019-Par4n 0 2308 19045.198 7450.659230823080107719 0
2019-Yices 2.6.2n 0 137 7338.95 7339.895137137011416 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 1152 58089.523 58107.007115201152248442 0
Yices2-fixedn 0 1152 58290.828 58309.605115201152248442 0
Bitwuzla 0 1148 27780.249 27793.325114801148248819 0
Bitwuzla-fixedn 0 1148 27884.444 27873.997114801148248819 0
MathSAT5n 0 1117 91588.971 91607.9121117011172519109 1
CVC4 0 1105 103029.708 103604.1271105011052531119 0
z3n 0 1100 111377.401 111346.0941100011002536147 0
2019-Par4n 0 1058 70793.249 23697.031105801058232719 0
2019-Boolectorn 0 1058 25478.81 25485.039105801058232716 0
2019-Yices 2.6.2n 0 98 17872.697 17872.6699809815316 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Bitwuzla 0 3518 3722.678 3732.69535182406111211892 0
Bitwuzla-fixedn 0 3518 3775.07 3742.80635182406111211892 0
Yices2 0 3487 4803.832 4822.163348723991088149149 0
Yices2-fixedn 0 3487 4793.74 4822.554348723991088149149 0
CVC4 0 3420 8406.768 8373.301342023601060216216 0
MathSAT5n 0 3404 7873.802 7837.288340423441060232231 1
z3n 0 3386 8266.616 8231.564338623331053250250 0
2019-Par4n 0 3328 3205.756 2104.3793328229310355757 0
2019-Boolectorn 0 3306 2991.139 2982.3123306227510317979 0
2019-Yices 2.6.2n 0 204 1264.128 1262.459204130744747 0

n Non-competing.