SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Previous Competitions
SMT-LIB

SMT-COMP 2019

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 2019-07-23 17:56:09 +0000

Benchmarks: 275
Time Limit: 2400 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 275 23099.697 23380.6682759318200 0
CVC4 0 275 46216.901 46638.2252759318200 0
Alt-Ergo 0 181 111747.563 105360.72918101819443 0
Vampire 0 181 230014.351 226730.23818101819494 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-CVC4n 0 275 23099.697 23380.6682759318200 0
CVC4 0 275 46216.901 46638.2252759318200 0
Vampire 0 182 245286.341 225137.22318201829393 0
Alt-Ergo 0 181 111747.563 105360.72918101819443 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-CVC4n 0 93 23090.726 23371.745939301820 0
CVC4 0 93 46207.251 46628.633939301820 0
Alt-Ergo 0 0 100812.65 100804.26100027543 0
Vampire 0 0 237600.48 223182.2900027593 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-CVC4n 0 182 8.971 8.9231820182930 0
CVC4 0 182 9.651 9.5921820182930 0
Vampire 0 182 7685.861 1954.93318201829393 0
Alt-Ergo 0 181 10934.913 4556.46818101819443 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-CVC4n 0 227 1174.469 1174.324227451824848 0
CVC4 0 227 1175.658 1175.503227451824848 0
Alt-Ergo 0 176 1214.053 1175.02317601769948 0
Vampire 0 176 2869.623 2517.60317601769999 0

n Non-competing.