SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2019

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

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 UNSATUnsolvedAbstainedTimeout 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 ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Par4 0 63579231.445574140.82963360237231 6
CVC4 0 58584791.509585015.51858157242239 0
2018-CVC4n 0 57580753.004580809.84657156243240 0
Vampire 0 57611447.172590308.43557057243243 0
Z3n 0 40279505.649284071.7414033726047 3
Alt-Ergo 0 37647912.142629787.79737037263261 1
UltimateEliminator+Yices-2.6.1 0 0952.187799.0040003000 0
UltimateEliminator+MathSAT-5.5.4 0 03426.4393923.2350003001 0

SAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 30.0180.068330297231 6
Z3n 0 30.1130.11333029747 3
2018-CVC4n 0 12884.5982906.816110299240 0
CVC4 0 13366.1573404.964110299239 0
UltimateEliminator+Yices-2.6.1 0 09.3796.8850003000 0
UltimateEliminator+MathSAT-5.5.4 0 010.1927.0980003001 0
Alt-Ergo 0 04800.1394800.052000300261 1
Vampire 0 07200.07200.0000300243 0

UNSAT Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 6024831.42719740.7660060240231 6
Vampire 0 5749847.17228708.43557057243243 0
CVC4 0 5730381.75530560.97957057243239 0
2018-CVC4n 0 5627515.24427576.47456056244240 0
Z3n 0 3728515.69829182.8983703726347 3
Alt-Ergo 0 3774310.40370789.75537037263261 1
UltimateEliminator+Yices-2.6.1 0 0209.835151.5040003000 0
UltimateEliminator+MathSAT-5.5.4 0 0224.418159.2010003001 0

24 seconds Performance

Solver Error Score Correct ScoreCPU Time ScoreWall Time ScoreSolvedSolved SATSolved UNSATUnsolvedAbstainedTimeout Memout
Par4 0 446241.5756196.17344341256250 6
Vampire 0 417238.7026479.31441041259259 0
Z3n 0 375929.7525929.75537334263243 3
2018-CVC4n 0 346418.3716418.36434034266265 0
Alt-Ergo 0 326658.2026474.38432032268266 1
CVC4 0 316449.3336449.32131031269268 0
UltimateEliminator+Yices-2.6.1 0 0972.85705.1930003001 0
UltimateEliminator+MathSAT-5.5.4 0 01090.85782.8620003003 0

n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.