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

Competition results for the QF_UFNIA 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)
CVC4CVC4CVC4 CVC4 CVC4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 285 2710.693 2711.335285175110151 0
MathSAT-default 0 270 76062.695 76068.552701601103030 0
2018-Yicesn 0 268 50701.869 50708.43268170983221 0
Yices 2.6.2 0 268 50762.306 50770.931268170983221 0
Z3n 0 264 59509.047 59513.2022641541103622 0
MathSAT-na-ext 0 259 100270.792 100279.1812591491104141 0
Alt-Ergo 0 71 50.84 21.119710712290 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 285 2711.193 2711.235285175110151 0
MathSAT-default 0 270 76067.355 76067.462701601103030 0
2018-Yicesn 0 268 50707.199 50707.63268170983221 0
Yices 2.6.2 0 268 50769.736 50770.291268170983221 0
Z3n 0 264 59511.797 59512.3622641541103622 0
MathSAT-na-ext 0 259 100277.352 100277.6612591491104141 0
Alt-Ergo 0 71 50.84 21.119710712290 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 175 300.4 300.46517517501251 0
2018-Yicesn 0 170 2705.806 2706.008170170013021 0
Yices 2.6.2 0 170 2768.254 2768.551170170013021 0
MathSAT-default 0 160 49646.011 49646.106160160014030 0
Z3n 0 154 44461.549 44461.939154154014622 0
MathSAT-na-ext 0 149 73847.765 73848.062149149015141 0
Alt-Ergo 0 0 38.885 14.9760003000 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 110 5.337 5.31411001101901 0
Z3n 0 110 7724.986 7725.136110011019022 0
MathSAT-default 0 110 16821.344 16821.355110011019030 0
MathSAT-na-ext 0 110 16829.587 16829.599110011019041 0
2018-Yicesn 0 98 38401.393 38401.6229809820221 0
Yices 2.6.2 0 98 38401.482 38401.749809820221 0
Alt-Ergo 0 71 11.145 5.828710712290 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 283 120.66 120.628283173110173 0
2018-Yicesn 0 266 568.423 568.848266168983423 0
Yices 2.6.2 0 266 571.218 571.732266168983423 0
MathSAT-default 0 266 990.553 990.5762661561103434 0
Z3n 0 254 1190.89 1190.9042541461084645 0
MathSAT-na-ext 0 252 1266.419 1266.4422521421104848 0
Alt-Ergo 0 71 50.84 21.119710712290 0

n Non-competing.