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

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

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

Benchmarks: 139
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 139 57.784 57.948139598000 0
2018-Yicesn 0 139 61.481 61.647139598000 0
SMTInterpol 0 139 849.261 413.676139598000 0
CVC4 0 138 5920.914 5922.027138597911 0
Z3n 0 134 13291.91 13290.119134548055 0
Alt-Ergo 0 70 142021.048 133943.646700706954 0
veriT 0 16 7.645 7.606160161230 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 139 57.784 57.948139598000 0
2018-Yicesn 0 139 61.481 61.647139598000 0
SMTInterpol 0 139 849.261 413.676139598000 0
CVC4 0 138 5921.154 5922.007138597911 0
Z3n 0 134 13293.57 13289.869134548055 0
Alt-Ergo 0 71 154452.518 129673.616710716849 0
veriT 0 16 7.645 7.606160161230 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 59 51.416 51.4259590800 0
2018-Yicesn 0 59 54.831 54.84359590800 0
SMTInterpol 0 59 450.646 179.27859590800 0
CVC4 0 59 1940.408 1941.10859590801 0
Z3n 0 54 13203.67 13199.96854540855 0
veriT 0 0 3.753 3.7370001390 0
Alt-Ergo 0 0 121389.831 105180.36700013949 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 80 6.367 6.52880080590 0
2018-Yicesn 0 80 6.65 6.80580080590 0
Z3n 0 80 89.9 89.90180080595 0
SMTInterpol 0 80 398.615 234.39980080590 0
CVC4 0 79 3980.746 3980.89979079601 0
Alt-Ergo 0 71 33062.687 24493.249710716849 0
veriT 0 16 3.892 3.87160161230 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 139 57.784 57.948139598000 0
2018-Yicesn 0 139 61.481 61.647139598000 0
SMTInterpol 0 136 767.209 367.851136597733 0
Z3n 0 118 666.767 663.00711839792121 0
CVC4 0 116 634.852 634.81911645712323 0
Alt-Ergo 0 66 2784.92 1960.728660667369 0
veriT 0 16 7.645 7.606160161230 0

n Non-competing.