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

UFNIA (Single Query Track)

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

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

Benchmarks: 5993
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 3506 6230692.435 6103765.2613506455305124872477 10
CVC4-SymBreakn 0 3325 6613445.664 6891006.833325453287226682666 0
CVC4 0 3316 6542541.597 6844099.9833316455286126772674 0
Z3n 0 2496 6527302.798 6532235.7782496355214134972466 12
2018-Z3n 0 2462 6566706.847 6571648.3332462347211535312481 7
Vampire 0 2352 9372892.581 8901045.11923520235236413641 0
2018-Vampiren 0 2137 9910677.307 9422860.85921370213738563856 0
Alt-Ergo 0 1001 8314962.019 7558228.52410010100149922794 177
UltimateEliminator+MathSAT-5.5.4 0 20 589384.757 583032.793200205973236 0
UltimateEliminator+Yices-2.6.1 0 0 550604.062 606084.4060005993245 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Vampiren 0 3774 16115465.297 7407890.40737740377422192219 0
Par4 0 3513 6234500.095 6097428.7713513455305824802470 10
CVC4-SymBreakn 0 3325 6857534.154 6890865.673325453287226682666 0
CVC4 0 3316 6828611.544 6843968.5933316455286126772675 0
Vampire 0 2510 10614412.931 8762318.36625100251034833483 0
Z3n 0 2496 6528991.378 6532128.4282496355214134972466 12
2018-Z3n 0 2462 6569187.697 6571543.0132462347211535312481 7
Alt-Ergo 0 1041 8881364.949 7084848.12210410104149522392 177
UltimateEliminator+MathSAT-5.5.4 0 20 965056.527 507410.633200205973128 0
UltimateEliminator+Yices-2.6.1 0 0 985239.123 541737.7760005993145 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 455 46158.86 32894.924455455055382470 10
CVC4 0 455 57428.932 58743.389455455055382675 0
CVC4-SymBreakn 0 453 60083.228 61034.461453453055402666 0
Z3n 0 355 242862.056 243021.43355355056382466 12
2018-Z3n 0 347 264897.996 264900.095347347056462481 7
UltimateEliminator+MathSAT-5.5.4 0 0 1581.293 1111.2010005993128 0
UltimateEliminator+Yices-2.6.1 0 0 8672.491 8213.2960005993145 0
Alt-Ergo 0 0 174639.733 173527.26100059932392 177
2018-Vampiren 0 0 1672812.85 1110405.9100059932219 0
Vampire 0 0 1154401.18 1111085.2700059933483 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Vampiren 0 3774 9647335.147 3059462.78737740377422192219 0
Par4 0 3058 2948341.234 2824533.84730580305829352470 10
CVC4-SymBreakn 0 2872 3559368.223 3591740.13128720287231212666 0
CVC4 0 2861 3532619.558 3546642.62828610286131322675 0
Vampire 0 2510 5953604.971 4411852.07625100251034833483 0
Z3n 0 2141 3636561.063 3637807.66921410214138522466 12
2018-Z3n 0 2115 3651782.274 3652119.1521150211538782481 7
Alt-Ergo 0 1041 6583449.735 5039440.00210410104149522392 177
UltimateEliminator+MathSAT-5.5.4 0 20 958922.89 502894.916200205973128 0
UltimateEliminator+Yices-2.6.1 0 0 955356.106 513608.0270005993145 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 2907 80665.317 77643.122907410249730863076 10
CVC4 0 2430 90359.415 90311.82430393203735633562 0
CVC4-SymBreakn 0 2398 91389.83 91344.7932398390200835953594 0
Z3n 0 2299 88961.382 88925.0022299329197036943536 12
2018-Z3n 0 2245 89833.519 89811.5812245315193037483585 7
2018-Vampiren 0 1521 116058.676 109689.50315210152144724472 0
Vampire 0 1455 125364.932 113305.25614550145545384538 0
Alt-Ergo 0 841 101444.895 95404.638841084151523695 177
UltimateEliminator+MathSAT-5.5.4 0 20 25734.318 19991.943200205973257 0
UltimateEliminator+Yices-2.6.1 0 0 25414.984 19702.560005993270 0

n Non-competing.