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

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 UNSATUnsolvedTimeout 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 Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 760 79786.403 65156.7767603124484242 0
z3n 0 744 103287.313 103273.5677443054395858 0
2019-Z3n 0 742 103547.878 103544.0687423054376060 0
CVC4 0 653 201706.907 202291.346653269384149149 0
UltimateEliminator+MathSAT 0 504 370033.47 368155.787504201303298297 0
Vampire 0 237 739115.338 693847.3272370237565565 0
SMTInterpol 0 132 19655.618 18391.48132113167014 0
SMTInterpol-fixedn 0 132 19669.496 18408.514132113167014 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 312 20829.361 15243.897312312049042 0
2019-Z3n 0 305 24943.113 24944.059305305049760 0
z3n 0 305 25132.246 25125.705305305049758 0
CVC4 0 269 70934.037 71271.2832692690533149 0
UltimateEliminator+MathSAT 0 201 144077.879 143398.9382012010601297 0
SMTInterpol 0 1 14949.868 14359.05811080114 0
SMTInterpol-fixedn 0 1 14992.736 14377.23811080114 0
Vampire 0 0 391200.32 383975.89000802565 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 448 44557.041 35512.879448044835442 0
z3n 0 439 63755.067 63747.863439043936358 0
2019-Z3n 0 437 64204.765 64200.01437043736560 0
CVC4 0 384 116372.87 116620.0633840384418149 0
UltimateEliminator+MathSAT 0 303 211555.591 210356.8493030303499297 0
Vampire 0 237 333515.018 295471.4372370237565565 0
SMTInterpol-fixedn 0 131 4637.41 4018.25131013167114 0
SMTInterpol 0 131 4670.701 4019.3131013167114 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 694 3921.923 3298.561694289405108108 0
z3n 0 642 5114.393 5097.564642279363160160 0
2019-Z3n 0 641 5209.609 5202.519641279362161161 0
CVC4 0 593 5222.645 5222.518593244349209209 0
UltimateEliminator+MathSAT 0 455 10851.2 9782.643455191264347346 0
Vampire 0 144 16420.483 15980.6281440144658658 0
SMTInterpol-fixedn 0 132 2379.787 1297.818132113167023 0
SMTInterpol 0 132 2371.876 1299.02132113167023 0

n Non-competing.