SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

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

Previous

SMT-LIB

AUFNIRA (Single Query Track)

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

Page generated on 2019-07-07 12:14:30 +0000

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

Winners

Sequential Performance Parallel Performance SAT Performance (parallel) UNSAT Performance (parallel) 24 seconds Performance (parallel)
Par4 Par4 Par4 Par4 Par4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 62 577498.135 574451.769 62 3 59 238 232 6
CVC4 0 58 562394.729 585027.728 58 1 57 242 239 0
2018-CVC4n 0 57 576360.664 580819.896 57 1 56 243 240 0
Vampire 0 51 605970.742 599715.405 51 0 51 249 249 0
Z3n 0 40 279014.839 284074.051 40 3 37 260 47 3
Alt-Ergo 0 37 633510.542 629989.807 37 0 37 263 261 1
UltimateEliminator+Yices-2.6.1 0 0 952.187 799.004 0 0 0 300 0 0
UltimateEliminator+MathSAT-5.5.4 0 0 3426.439 3923.235 0 0 0 300 1 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 63 579231.445 574140.829 63 3 60 237 231 6
CVC4 0 58 584791.509 585015.518 58 1 57 242 239 0
2018-CVC4n 0 57 580753.004 580809.846 57 1 56 243 240 0
Vampire 0 57 611447.172 590308.435 57 0 57 243 243 0
Z3n 0 40 279505.649 284071.741 40 3 37 260 47 3
Alt-Ergo 0 37 647912.142 629787.797 37 0 37 263 261 1
UltimateEliminator+Yices-2.6.1 0 0 952.187 799.004 0 0 0 300 0 0
UltimateEliminator+MathSAT-5.5.4 0 0 3426.439 3923.235 0 0 0 300 1 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 3 0.018 0.068 3 3 0 297 231 6
Z3n 0 3 0.113 0.113 3 3 0 297 47 3
2018-CVC4n 0 1 2884.598 2906.816 1 1 0 299 240 0
CVC4 0 1 3366.157 3404.964 1 1 0 299 239 0
UltimateEliminator+Yices-2.6.1 0 0 9.379 6.885 0 0 0 300 0 0
UltimateEliminator+MathSAT-5.5.4 0 0 10.192 7.098 0 0 0 300 1 0
Alt-Ergo 0 0 4800.139 4800.052 0 0 0 300 261 1
Vampire 0 0 7200.0 7200.0 0 0 0 300 243 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 60 24831.427 19740.76 60 0 60 240 231 6
Vampire 0 57 49847.172 28708.435 57 0 57 243 243 0
CVC4 0 57 30381.755 30560.979 57 0 57 243 239 0
2018-CVC4n 0 56 27515.244 27576.474 56 0 56 244 240 0
Z3n 0 37 28515.698 29182.898 37 0 37 263 47 3
Alt-Ergo 0 37 74310.403 70789.755 37 0 37 263 261 1
UltimateEliminator+Yices-2.6.1 0 0 209.835 151.504 0 0 0 300 0 0
UltimateEliminator+MathSAT-5.5.4 0 0 224.418 159.201 0 0 0 300 1 0

24s Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 44 6241.575 6196.173 44 3 41 256 250 6
Vampire 0 41 7238.702 6479.314 41 0 41 259 259 0
Z3n 0 37 5929.752 5929.755 37 3 34 263 243 3
2018-CVC4n 0 34 6418.371 6418.364 34 0 34 266 265 0
Alt-Ergo 0 32 6658.202 6474.384 32 0 32 268 266 1
CVC4 0 31 6449.333 6449.321 31 0 31 269 268 0
UltimateEliminator+Yices-2.6.1 0 0 972.85 705.193 0 0 0 300 1 0
UltimateEliminator+MathSAT-5.5.4 0 0 1090.85 782.862 0 0 0 300 3 0

n Non-competing.