SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_AUFBV (Single Query Track)

Competition results for the QF_AUFBV division in the Single Query Track.

Page generated on 2020-07-04 11:46:58 +0000

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Yices2Yices2Yices2 Yices2 Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Yices2-fixedn 0 25 15017.022 15019.2212581799 0
2019-Yices 2.6.2n 0 25 15038.346 15040.0812581799 0
Yices2 0 25 15127.059 15129.1822581799 0
z3n 0 19 19206.98 19211.257194151515 0
MathSAT5n 0 17 22764.421 22769.753173141717 0
Bitwuzla 0 14 5399.081 5401.90914410204 0
Bitwuzla-fixedn 0 14 5402.079 5403.64814410204 0
CVC4 0 11 26776.435 27711.066111102323 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Yices2-fixedn 0 2515018.19215018.9112581799 0
2019-Yices 2.6.2n 0 2515039.20615039.7712581799 0
Yices2 0 2515128.22915128.7922581799 0
z3n 0 1919210.2419210.607194151515 0
MathSAT5n 0 1722768.63122769.113173141717 0
Bitwuzla 0 145401.2915401.63914410204 0
Bitwuzla-fixedn 0 145403.0095403.38814410204 0
CVC4 0 1127709.92527709.926111102323 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2-fixedn 0 87104.927105.556880269 0
2019-Yices 2.6.2n 0 87126.6627127.088880269 0
Yices2 0 87128.947129.456880269 0
Bitwuzla 0 4562.554562.814440304 0
Bitwuzla-fixedn 0 4563.406563.636440304 0
z3n 0 48767.4238767.624403015 0
MathSAT5n 0 39766.9239766.9473303117 0
CVC4 0 112081.03812081.041103323 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Yices 2.6.2n 0 173112.5443112.68317017179 0
Yices2-fixedn 0 173113.2723113.35517017179 0
Yices2 0 173199.2883199.33617017179 0
z3n 0 155642.8175642.987150151915 0
MathSAT5n 0 148201.7098202.167140142017 0
Bitwuzla 0 1038.73738.82510010244 0
Bitwuzla-fixedn 0 1039.60339.75210010244 0
CVC4 0 1010828.88710828.886100102423 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Yices 2.6.2n 0 16468.288468.29162141818 0
Yices2 0 16469.117469.13162141818 0
Yices2-fixedn 0 16469.24469.245162141818 0
z3n 0 13558.623558.631132112121 0
MathSAT5n 0 11567.898567.914111102323 0
Bitwuzla 0 10196.231196.3911019248 0
Bitwuzla-fixedn 0 10196.191196.431019248 0
CVC4 0 10604.887604.886100102424 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.