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_AX (Single Query Track)

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

Page generated on 2019-07-23 17:56:09 +0000

Benchmarks: 300
Time Limit: 2400 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 Yices 2.6.2 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 300 4.146 4.81430015015000 0
2018-Yicesn 0 300 4.254 4.80530015015000 0
Z3n 0 300 25.783 25.79330015015000 0
CVC4 0 300 71.28 71.22330015015000 0
SMTInterpol 0 300 401.031 181.98330015015000 0
Alt-Ergo 0 138 55759.336 35948.001138013816212 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Yicesn 0 300 4.254 4.80530015015000 0
Yices 2.6.2 0 300 4.146 4.81430015015000 0
Z3n 0 300 25.783 25.79330015015000 0
CVC4 0 300 71.28 71.22330015015000 0
SMTInterpol 0 300 401.031 181.98330015015000 0
Alt-Ergo 0 147 82680.986 26565.75914701471533 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Yicesn 0 150 1.246 1.59715015001500 0
Yices 2.6.2 0 150 1.199 1.63215015001500 0
CVC4 0 150 8.203 8.16515015001500 0
Z3n 0 150 9.113 9.12115015001500 0
SMTInterpol 0 150 112.675 60.14115015001500 0
Alt-Ergo 0 0 4348.359 1447.1840003003 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 150 2.947 3.18215001501500 0
2018-Yicesn 0 150 3.008 3.20815001501500 0
Z3n 0 150 16.67 16.67215001501500 0
CVC4 0 150 63.078 63.05815001501500 0
SMTInterpol 0 150 288.356 121.84215001501500 0
Alt-Ergo 0 147 78332.628 25118.57514701471533 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Yicesn 0 300 4.254 4.80530015015000 0
Yices 2.6.2 0 300 4.146 4.81430015015000 0
Z3n 0 300 25.783 25.79330015015000 0
CVC4 0 300 71.28 71.22330015015000 0
SMTInterpol 0 300 401.031 181.98330015015000 0
Alt-Ergo 0 99 3802.304 2361.3339909920176 0

n Non-competing.