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

LRA (Single Query Track)

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

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

Benchmarks: 802
Time Limit: 1200 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 UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 755 76904.603 66708.3167553104454747 0
z3n 0 744 103284.173 103275.4677443054395858 0
2019-Z3n 0 742 103542.378 103546.4087423054376060 0
CVC4 0 653 201426.837 202297.426653269384149149 0
UltimateEliminator+MathSAT 0 504 370033.47 368155.787504201303298297 0
Vampire 0 222 715390.128 702806.2722220222580580 0
SMTInterpol 0 132 19655.618 18391.48132113167014 0
SMTInterpol-fixedn 0 132 19669.496 18408.514132113167014 0

Parallel Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 76079786.40365156.7767603124484242 0
z3n 0 744103287.313103273.5677443054395858 0
2019-Z3n 0 742103547.878103544.0687423054376060 0
CVC4 0 653201706.907202291.346653269384149149 0
UltimateEliminator+MathSAT 0 504370033.47368155.787504201303298297 0
Vampire 0 237739115.338693847.3272370237565565 0
SMTInterpol 0 13219655.61818391.48132113167014 0
SMTInterpol-fixedn 0 13219669.49618408.514132113167014 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 31220829.36115243.897312312049042 0
2019-Z3n 0 30524943.11324944.059305305049760 0
z3n 0 30525132.24625125.705305305049758 0
CVC4 0 26970934.03771271.2832692690533149 0
UltimateEliminator+MathSAT 0 201144077.879143398.9382012010601297 0
SMTInterpol 0 114949.86814359.05811080114 0
SMTInterpol-fixedn 0 114992.73614377.23811080114 0
Vampire 0 0391200.32383975.89000802565 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 44844557.04135512.879448044835442 0
z3n 0 43963755.06763747.863439043936358 0
2019-Z3n 0 43764204.76564200.01437043736560 0
CVC4 0 384116372.87116620.0633840384418149 0
UltimateEliminator+MathSAT 0 303211555.591210356.8493030303499297 0
Vampire 0 237333515.018295471.4372370237565565 0
SMTInterpol-fixedn 0 1314637.414018.25131013167114 0
SMTInterpol 0 1314670.7014019.3131013167114 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
2019-Par4n 0 6943921.9233298.561694289405108108 0
z3n 0 6425114.3935097.564642279363160160 0
2019-Z3n 0 6415209.6095202.519641279362161161 0
CVC4 0 5935222.6455222.518593244349209209 0
UltimateEliminator+MathSAT 0 45510851.29782.643455191264347346 0
Vampire 0 14416420.48315980.6281440144658658 0
SMTInterpol-fixedn 0 1322379.7871297.818132113167023 0
SMTInterpol 0 1322371.8761299.02132113167023 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.