SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Papers
Benchmark Submission
Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Previous Competitions

SMT-LIB

QF_RDL (Single Query Track)

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

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

Benchmarks: 247
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 214 83405.108 83410.5952141051093333 0
2018-Yicesn 0 214 83634.304 83638.7512141051093333 0
CVC4 0 211 95504.663 95417.9512111031083636 0
veriT 0 210 102696.7 102704.2682101041063737 0
Z3n 0 209 99844.008 99850.1382091021073838 0
SMTInterpol 0 194 153890.186 152250.169194101935353 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 214 83409.238 83409.4552141051093333 0
2018-Yicesn 0 214 83637.364 83637.7712141051093333 0
CVC4 0 211 95511.093 95416.6912111031083636 0
veriT 0 210 102701.87 102703.1082101041063737 0
Z3n 0 209 99848.198 99848.6482091021073838 0
SMTInterpol 0 194 153890.186 152250.169194101935353 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 105 741.918 741.942105105014233 0
2018-Yicesn 0 105 775.591 775.666105105014233 0
veriT 0 104 9130.002 9130.602104104014337 0
CVC4 0 103 9458.873 9441.467103103014436 0
Z3n 0 102 13437.537 13437.757102102014538 0
SMTInterpol 0 101 22736.958 21890.126101101014653 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 109 3467.32 3467.513109010913833 0
2018-Yicesn 0 109 3661.773 3662.105109010913833 0
CVC4 0 108 6852.22 6775.224108010813936 0
Z3n 0 107 7210.661 7210.891107010714038 0
veriT 0 106 14371.868 14372.506106010614137 0
SMTInterpol 0 93 51953.228 51160.0429309315453 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 195 1602.044 1602.09195100955252 0
2018-Yicesn 0 194 1623.238 1623.3194100945353 0
Z3n 0 179 2106.94 2106.99117991886868 0
CVC4 0 168 2529.624 2511.83716886827979 0
veriT 0 167 2312.207 2312.18116781868080 0
SMTInterpol 0 135 4030.699 3338.3261357461112112 0

n Non-competing.