SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Papers
Benchmark Submission
Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Previous Competitions

SMT-LIB

AUFNIRA (Single Query Track)

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

Page generated on 2019-07-23 17:56:09 +0000

Benchmarks: 300
Time Limit: 2400 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Par4Par4Par4 Par4 Par4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 62 577498.135 574451.76962359238232 6
CVC4 0 58 562394.729 585027.72858157242239 0
2018-CVC4n 0 57 576360.664 580819.89657156243240 0
Vampire 0 51 605970.742 599715.40551051249249 0
Z3n 0 40 279014.839 284074.0514033726047 3
Alt-Ergo 0 37 633510.542 629989.80737037263261 1
UltimateEliminator+Yices-2.6.1 0 0 952.187 799.0040003000 0
UltimateEliminator+MathSAT-5.5.4 0 0 3426.439 3923.2350003001 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 63 579231.445 574140.82963360237231 6
CVC4 0 58 584791.509 585015.51858157242239 0
2018-CVC4n 0 57 580753.004 580809.84657156243240 0
Vampire 0 57 611447.172 590308.43557057243243 0
Z3n 0 40 279505.649 284071.7414033726047 3
Alt-Ergo 0 37 647912.142 629787.79737037263261 1
UltimateEliminator+Yices-2.6.1 0 0 952.187 799.0040003000 0
UltimateEliminator+MathSAT-5.5.4 0 0 3426.439 3923.2350003001 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 3 0.018 0.068330297231 6
Z3n 0 3 0.113 0.11333029747 3
2018-CVC4n 0 1 2884.598 2906.816110299240 0
CVC4 0 1 3366.157 3404.964110299239 0
UltimateEliminator+Yices-2.6.1 0 0 9.379 6.8850003000 0
UltimateEliminator+MathSAT-5.5.4 0 0 10.192 7.0980003001 0
Alt-Ergo 0 0 4800.139 4800.052000300261 1
Vampire 0 0 7200.0 7200.0000300243 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 60 24831.427 19740.7660060240231 6
Vampire 0 57 49847.172 28708.43557057243243 0
CVC4 0 57 30381.755 30560.97957057243239 0
2018-CVC4n 0 56 27515.244 27576.47456056244240 0
Z3n 0 37 28515.698 29182.8983703726347 3
Alt-Ergo 0 37 74310.403 70789.75537037263261 1
UltimateEliminator+Yices-2.6.1 0 0 209.835 151.5040003000 0
UltimateEliminator+MathSAT-5.5.4 0 0 224.418 159.2010003001 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 44 6241.575 6196.17344341256250 6
Vampire 0 41 7238.702 6479.31441041259259 0
Z3n 0 37 5929.752 5929.75537334263243 3
2018-CVC4n 0 34 6418.371 6418.36434034266265 0
Alt-Ergo 0 32 6658.202 6474.38432032268266 1
CVC4 0 31 6449.333 6449.32131031269268 0
UltimateEliminator+Yices-2.6.1 0 0 972.85 705.1930003001 0
UltimateEliminator+MathSAT-5.5.4 0 0 1090.85 782.8620003003 0

n Non-competing.