SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2020

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

QF_LIA (Unsat Core Track)

Competition results for the QF_LIA division in the Unsat Core Track.

Page generated on 2020-07-04 11:49:33 +0000

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

Winners

Sequential PerformanceParallel Performance
Yices2Yices2

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreAbstainedTimeout Memout
Yices2-fixedn 0 945496 30877.88 30874.54423 0
Yices2 0 945496 30881.511 30889.13723 0
z3n 0 925924 75559.242 75567.51662 0
MathSAT5n 0 924387 104421.548 104422.81486 0
CVC4-uc 0 827760 108993.611 109007.13788 0
SMTInterpol 0 811054 38135.709 37100.76822 0
SMTInterpol-fixedn 0 811054 38199.89 37220.58122 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreAbstainedTimeout Memout
Yices2-fixedn 0 94549630883.8230873.91423 0
Yices2 0 94549630887.09130888.31723 0
z3n 0 92592475565.41275565.58662 0
MathSAT5n 0 924387104441.458104419.04486 0
CVC4-uc 0 827760109003.321109003.65788 0
SMTInterpol 0 81105438135.70937100.76822 0
SMTInterpol-fixedn 0 81105438199.8937220.58122 0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.