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

AUFDTLIA (Single Query Track)

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

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

Benchmarks: 147
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
2018-CVC4n 0 147 23110.799 23328.546147935400 0
CVC4 0 147 23164.987 23515.546147935400 0
Vampire 0 54 112771.215 112020.667540549393 0
Alt-Ergo 0 53 52229.293 49071.433530539440 0
UltimateEliminator+MathSAT 0 0 482.985 341.5190001470 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-CVC4n 0 147 23110.799 23328.546147935400 0
CVC4 0 147 23164.987 23515.546147935400 0
Alt-Ergo 0 54 53028.373 48374.45540549339 0
Vampire 0 54 116371.495 112003.377540549393 0
UltimateEliminator+MathSAT 0 0 482.985 341.5190001470 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-CVC4n 0 93 23093.255 23310.99193930540 0
CVC4 0 93 23149.376 23499.9593930540 0
UltimateEliminator+MathSAT 0 0 308.535 213.5790001470 0
Alt-Ergo 0 0 46812.671 46804.22800014739 0
Vampire 0 0 115200.28 111582.7100014793 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 54 15.611 15.59554054930 0
2018-CVC4n 0 54 17.544 17.55654054930 0
Vampire 0 54 1171.215 420.667540549393 0
Alt-Ergo 0 54 6215.702 1570.222540549339 0
UltimateEliminator+MathSAT 0 0 174.45 127.9390001470 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 99 1181.877 1182.2829945544848 0
2018-CVC4n 0 99 1182.86 1182.7839945544848 0
Vampire 0 49 2560.365 2447.418490499898 0
Alt-Ergo 0 47 1126.043 1113.984704710046 0
UltimateEliminator+MathSAT 0 0 482.985 341.5190001470 0

n Non-competing.