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

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 7 222.249 111.96771600 0
z3n 0 6 1338.104 1338.13761511 0
Yices2 0 6 1341.479 1341.60561511 0
Yices2-fixedn 0 6 1342.579 1342.69761511 0
MathSAT5n 0 5 2405.291 2405.77151422 0
CVC4 0 5 2405.58 2406.49951422 0
SMTInterpol-fixedn 0 4 3734.913 3689.83641333 0
SMTInterpol 0 4 3735.389 3688.63241333 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 7 222.249 111.96771600 0
z3n 0 6 1338.104 1338.13761511 0
Yices2 0 6 1341.539 1341.57561511 0
Yices2-fixedn 0 6 1342.669 1342.67761511 0
MathSAT5n 0 5 2405.701 2405.70151422 0
CVC4 0 5 2406.45 2406.44951422 0
SMTInterpol 0 4 3735.389 3688.63241333 0
SMTInterpol-fixedn 0 4 3734.913 3689.83641333 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2 0 1 0.07 0.0711061 0
Yices2-fixedn 0 1 0.071 0.07111061 0
MathSAT5n 0 1 0.289 0.28911062 0
z3n 0 1 0.312 0.31211061 0
2019-Par4n 0 1 0.006 0.33411060 0
CVC4 0 1 1.138 1.13711062 0
SMTInterpol-fixedn 0 1 46.762 28.62711063 0
SMTInterpol 0 1 50.935 29.1711063 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2019-Par4n 0 6 222.243 111.63360610 0
z3n 0 5 1337.792 1337.82450521 0
Yices2 0 5 1341.469 1341.50550521 0
Yices2-fixedn 0 5 1342.598 1342.60550521 0
CVC4 0 4 2405.312 2405.31240432 0
MathSAT5n 0 4 2405.412 2405.41240432 0
SMTInterpol 0 3 3684.454 3659.46330343 0
SMTInterpol-fixedn 0 3 3688.151 3661.20930343 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices2-fixedn 0 5 48.358 48.36151422 0
Yices2 0 5 48.358 48.36151422 0
z3n 0 5 50.931 50.93251422 0
2019-Par4n 0 5 52.689 51.07651422 0
MathSAT5n 0 5 53.701 53.70151422 0
CVC4 0 5 54.45 54.44951422 0
SMTInterpol 0 2 125.591 122.05720255 0
SMTInterpol-fixedn 0 2 125.739 122.06920255 0

n Non-competing.