SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Competitions by Year

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_IDL (Single Query Track)

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

Page generated on 2020-07-04 11:46:59 +0000

Benchmarks: 834
Time Limit: 1200 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Yices2Yices2Yices2 CVC4 Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 742 123877.335 123888.427424862569292 0
Yices2-fixedn 0 742 124121.869 124117.6037424862569292 0
2019-Z3n 0 739 137184.425 137145.9537394782619595 0
2019-Par4n 0 736 140562.936 123468.337364812559898 0
z3n 0 721 122201.539 122188.97372148223911384 0
CVC4 0 680 235473.129 235454.564680423257154154 0
veriT 0 610 320196.593 320176.879610362248224224 0
MathSAT5n 0 566 356443.967 356493.482566326240268268 0
SMTInterpol 0 534 410519.691 405162.97534302232300300 0
SMTInterpol-fixedn 0 534 410714.465 405313.293534302232300300 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 752 162651.156 114684.4457524902628282 0
Yices2 0 742 123885.645 123885.417424862569292 0
Yices2-fixedn 0 742 124129.899 124114.7737424862569292 0
2019-Z3n 0 739 137191.995 137143.0237394782619595 0
z3n 0 721 122208.739 122186.10372148223911384 0
CVC4 0 680 235500.889 235447.814680423257154154 0
veriT 0 610 320214.923 320170.329610362248224224 0
MathSAT5n 0 566 356482.137 356483.712566326240268268 0
SMTInterpol 0 535 410534.011 405159.63535303232299299 0
SMTInterpol-fixedn 0 535 410724.685 405305.573535303232299299 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 490 66818.877 40240.697490490034482 0
Yices2 0 486 43714.319 43713.35486486034892 0
Yices2-fixedn 0 486 43784.623 43772.185486486034892 0
z3n 0 482 48397.606 48377.255482482035284 0
2019-Z3n 0 478 59807.796 59758.151478478035695 0
CVC4 0 423 150474.754 150423.0384234230411154 0
veriT 0 362 228006.542 227961.1433623620472224 0
MathSAT5n 0 326 257334.842 257337.8383263260508268 0
SMTInterpol 0 303 292797.388 289315.9693033030531299 0
SMTInterpol-fixedn 0 303 292892.027 289379.3563033030531299 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 262 63432.28 42043.747262026257282 0
2019-Z3n 0 261 44984.199 44984.872261026157395 0
CVC4 0 257 52626.136 52624.7762570257577154 0
Yices2 0 256 47771.326 47772.061256025657892 0
Yices2-fixedn 0 256 47945.276 47942.588256025657892 0
veriT 0 248 59808.381 59809.1862480248586224 0
MathSAT5n 0 240 66747.295 66745.8742400240594268 0
z3n 0 239 41411.132 41408.848239023959584 0
SMTInterpol 0 232 85336.624 83443.6612320232602299 0
SMTInterpol-fixedn 0 232 85432.658 83526.2182320232602299 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 672 7410.35 4845.351672438234162162 0
Yices2 0 670 4966.996 4965.419670439231164164 0
Yices2-fixedn 0 669 4982.731 4966.236669438231165165 0
2019-Z3n 0 623 6747.046 6695.638623403220211211 0
z3n 0 605 6590.321 6564.906605405200229200 0
CVC4 0 447 11082.358 11070.213447240207387387 0
MathSAT5n 0 443 10674.752 10672.77443227216391391 0
veriT 0 415 11021.181 11021.246415195220419419 0
SMTInterpol-fixedn 0 349 15198.685 13235.643349172177485485 0
SMTInterpol 0 348 15192.707 13235.96348172176486486 0

n Non-competing.