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

AUFDTLIRA (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
CVC4CVC4 CVC4 CVC4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 3958 48357.478 48365.81339580395848139 0
Alt-Ergo 0 3901 319435.455 303622.359390103901538240 7
Vampire 0 3855 1124286.672 829911.106385503855584584 0
UltimateEliminator+MathSAT 0 0 14664.401 10027.54300044390 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 3958 48364.678 48363.96339580395848139 0
Vampire 0 3944 1181745.532 765629.137394403944495495 0
Alt-Ergo 0 3903 335611.165 297697.372390303903536229 7
UltimateEliminator+MathSAT 0 0 14664.401 10027.54300044390 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Alt-Ergo 0 0 0.0 0.00004439229 7
Vampire 0 0 0.0 0.00004439495 0
CVC4 0 0 0.0 0.0000443939 0
UltimateEliminator+MathSAT 0 0 0.0 0.000044390 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 3958 25544.366 25543.6739580395848139 0
Vampire 0 3944 851745.532 435629.137394403944495495 0
Alt-Ergo 0 3903 162503.893 142199.329390303903536229 7
UltimateEliminator+MathSAT 0 0 13768.725 9404.32500044390 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
CVC4 0 3954 1391.34 1390.3839540395448543 0
Alt-Ergo 0 3848 11020.172 8792.48384803848591310 7
Vampire 0 2702 46922.612 44198.40527020270217371737 0
UltimateEliminator+MathSAT 0 0 14664.401 10027.54300044390 0

n Non-competing.