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

NRA (Single Query Track)

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

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

Benchmarks: 93
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 86 18125.521 17469.2018618577 0
Vampire 0 82 27315.095 26640.396820821111 0
2018-Z3n 0 82 27824.522 27827.118821811111 0
Z3n 0 82 27934.787 27936.588821811111 0
2018-Vampiren 0 74 56842.632 48435.42740741919 0
CVC4 0 62 69354.415 69735.439620623129 0
UltimateEliminator+MathSAT-5.5.4 0 1 324.94 223.03101920 0
UltimateEliminator+Yices-2.6.1 0 0 317.696 223.112000930 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 87 18560.051 16488.7118718666 0
Vampire 0 82 27315.095 26640.396820821111 0
2018-Z3n 0 82 27826.612 27826.808821811111 0
Z3n 0 82 27936.017 27936.048821811111 0
2018-Vampiren 0 81 66169.472 38212.969810811212 0
CVC4 0 62 69732.905 69733.749620623129 0
UltimateEliminator+MathSAT-5.5.4 0 1 324.94 223.03101920 0
UltimateEliminator+Yices-2.6.1 0 0 317.696 223.112000930 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 1 2400.051 2400.0521109211 0
2018-Z3n 0 1 2400.058 2400.0581109211 0
Par4 0 1 2400.006 2400.065110926 0
UltimateEliminator+Yices-2.6.1 0 0 6.79 4.82000930 0
UltimateEliminator+MathSAT-5.5.4 0 0 6.987 5.108000930 0
2018-Vampiren 0 0 4800.0 4800.00009312 0
CVC4 0 0 4800.0 4800.00009329 0
Vampire 0 0 4800.0 4800.00009311 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 86 16160.045 14088.6478608676 0
Vampire 0 82 22515.095 21840.396820821111 0
2018-Z3n 0 81 25426.554 25426.75810811211 0
Z3n 0 81 25535.966 25535.997810811211 0
2018-Vampiren 0 81 61369.472 33412.969810811212 0
CVC4 0 62 64932.905 64933.749620623129 0
UltimateEliminator+MathSAT-5.5.4 0 1 317.953 217.922101920 0
UltimateEliminator+Yices-2.6.1 0 0 310.906 218.292000930 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 85 203.011 201.2128518488 0
Z3n 0 81 303.117 303.118811801212 0
2018-Z3n 0 81 303.592 303.598811801212 0
Vampire 0 78 550.915 417.885780781515 0
CVC4 0 62 756.462 756.441620623131 0
2018-Vampiren 0 61 1428.382 938.938610613232 0
UltimateEliminator+MathSAT-5.5.4 0 1 324.94 223.03101920 0
UltimateEliminator+Yices-2.6.1 0 0 317.696 223.112000930 0

n Non-competing.