SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_AUFBV (Challenge Track (non-incremental))

Competition results for the QF_AUFBV division in the Challenge Track (non-incremental).

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

Benchmarks: 15
Time Limit: 43200 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Yices 2.6.2Yices 2.6.2Yices 2.6.2 Poolector Yices 2.6.2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 10 226776.086 226787.281109155 0
Z3n 0 8 259238.116 259268.17887175 0
Boolector 0 5 173174.008 173186.179541104 0
Poolector 0 4 216680.247 216173.112431114 1
2018-CVC4n 0 3 239216.642 240991.473321124 0
CVC4 0 3 354363.865 356633.43321127 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 10 226782.286 226787.081109155 0
Z3n 0 8 259256.016 259267.97887175 0
Boolector 0 5 173182.008 173185.979541104 0
Poolector 0 4 216680.247 216173.112431114 1
2018-CVC4n 0 3 239236.442 240991.273321124 0
CVC4 0 3 354389.765 356633.23321127 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 9 53963.205 53969.599065 0
Z3n 0 7 124712.244 124716.15477085 0
Boolector 0 4 351.731 351.797440114 0
Poolector 0 3 43820.627 43357.957330124 1
2018-CVC4n 0 2 209777.33 210433.897220134 0
CVC4 0 2 316357.17 317437.836220137 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Poolector 0 1 59.62 15.156101144 1
Yices 2.6.2 0 1 17.582 17.581101145 0
2018-CVC4n 0 1 18.142 18.146101144 0
CVC4 0 1 18.645 18.644101147 0
Z3n 0 1 19.292 19.293101145 0
Boolector 0 1 34.177 34.182101144 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 3 305.966 305.9663211212 0
Poolector 0 2 229.367 184.573211136 1
Z3n 0 2 331.916 331.9182111313 0
Boolector 0 1 192.31 192.31110148 0
2018-CVC4n 0 1 354.142 354.1461011414 0
CVC4 0 1 354.645 354.6441011414 0

n Non-competing.