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

Competition results for the QF_UFIDL 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 298 5406.047 5406.4772987622222 0
2018-Yicesn 0 298 5418.913 5419.4722987622222 0
Z3n 0 298 5631.745 5631.4962987622222 0
SMTInterpol 0 285 50037.164 48281.097285762091515 0
veriT 0 278 62289.678 62294.447278762022217 0
CVC4 0 276 81633.348 81642.172276762002424 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 298 5406.307 5406.3572987622222 0
2018-Yicesn 0 298 5419.263 5419.3422987622222 0
Z3n 0 298 5632.375 5631.4662987622222 0
SMTInterpol 0 285 50037.164 48281.097285762091515 0
veriT 0 278 62292.618 62293.757278762022217 0
CVC4 0 276 81639.118 81641.402276762002424 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 76 5.939 5.956767602242 0
2018-Yicesn 0 76 9.587 9.609767602242 0
Z3n 0 76 11.291 11.292767602242 0
veriT 0 76 14.017 14.07676022417 0
CVC4 0 76 61.443 61.457676022424 0
SMTInterpol 0 76 303.882 111.3767676022415 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 222 5400.368 5400.4012220222782 0
2018-Yicesn 0 222 5409.676 5409.7332220222782 0
Z3n 0 222 5621.085 5620.1732220222782 0
SMTInterpol 0 209 49733.283 48169.72120902099115 0
veriT 0 202 62278.601 62279.75720202029817 0
CVC4 0 200 81577.675 81579.952200020010024 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 294 307.8 307.8382947621866 0
2018-Yicesn 0 294 316.706 316.7522947621866 0
Z3n 0 291 375.46 374.4792917621599 0
SMTInterpol 0 256 3305.323 2033.401256761804444 0
veriT 0 254 1526.776 1526.755254761784646 0
CVC4 0 207 2814.217 2814.236207761319393 0

n Non-competing.