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

UFNIA (Single Query Track)

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

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

Benchmarks: 5993
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 3506 6230692.435 6103765.261 3506 455 3051 2487 2477 10
CVC4-SymBreakn 0 3325 6613445.664 6891006.83 3325 453 2872 2668 2666 0
CVC4 0 3316 6542541.597 6844099.983 3316 455 2861 2677 2674 0
Z3n 0 2496 6527302.798 6532235.778 2496 355 2141 3497 2466 12
2018-Z3n 0 2462 6566706.847 6571648.333 2462 347 2115 3531 2481 7
Vampire 0 2352 9372892.581 8901045.119 2352 0 2352 3641 3641 0
2018-Vampiren 0 2137 9910677.307 9422860.859 2137 0 2137 3856 3856 0
Alt-Ergo 0 1001 8314962.019 7558228.524 1001 0 1001 4992 2794 177
UltimateEliminator+MathSAT-5.5.4 0 20 589384.757 583032.793 20 0 20 5973 236 0
UltimateEliminator+Yices-2.6.1 0 0 550604.062 606084.406 0 0 0 5993 245 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Vampiren 0 3774 16115465.297 7407890.407 3774 0 3774 2219 2219 0
Par4 0 3513 6234500.095 6097428.771 3513 455 3058 2480 2470 10
CVC4-SymBreakn 0 3325 6857534.154 6890865.67 3325 453 2872 2668 2666 0
CVC4 0 3316 6828611.544 6843968.593 3316 455 2861 2677 2675 0
Vampire 0 2510 10614412.931 8762318.366 2510 0 2510 3483 3483 0
Z3n 0 2496 6528991.378 6532128.428 2496 355 2141 3497 2466 12
2018-Z3n 0 2462 6569187.697 6571543.013 2462 347 2115 3531 2481 7
Alt-Ergo 0 1041 8881364.949 7084848.122 1041 0 1041 4952 2392 177
UltimateEliminator+MathSAT-5.5.4 0 20 965056.527 507410.633 20 0 20 5973 128 0
UltimateEliminator+Yices-2.6.1 0 0 985239.123 541737.776 0 0 0 5993 145 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 455 46158.86 32894.924 455 455 0 5538 2470 10
CVC4 0 455 57428.932 58743.389 455 455 0 5538 2675 0
CVC4-SymBreakn 0 453 60083.228 61034.461 453 453 0 5540 2666 0
Z3n 0 355 242862.056 243021.43 355 355 0 5638 2466 12
2018-Z3n 0 347 264897.996 264900.095 347 347 0 5646 2481 7
UltimateEliminator+MathSAT-5.5.4 0 0 1581.293 1111.201 0 0 0 5993 128 0
UltimateEliminator+Yices-2.6.1 0 0 8672.491 8213.296 0 0 0 5993 145 0
Alt-Ergo 0 0 174639.733 173527.261 0 0 0 5993 2392 177
2018-Vampiren 0 0 1672812.85 1110405.91 0 0 0 5993 2219 0
Vampire 0 0 1154401.18 1111085.27 0 0 0 5993 3483 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
2018-Vampiren 0 3774 9647335.147 3059462.787 3774 0 3774 2219 2219 0
Par4 0 3058 2948341.234 2824533.847 3058 0 3058 2935 2470 10
CVC4-SymBreakn 0 2872 3559368.223 3591740.131 2872 0 2872 3121 2666 0
CVC4 0 2861 3532619.558 3546642.628 2861 0 2861 3132 2675 0
Vampire 0 2510 5953604.971 4411852.076 2510 0 2510 3483 3483 0
Z3n 0 2141 3636561.063 3637807.669 2141 0 2141 3852 2466 12
2018-Z3n 0 2115 3651782.274 3652119.15 2115 0 2115 3878 2481 7
Alt-Ergo 0 1041 6583449.735 5039440.002 1041 0 1041 4952 2392 177
UltimateEliminator+MathSAT-5.5.4 0 20 958922.89 502894.916 20 0 20 5973 128 0
UltimateEliminator+Yices-2.6.1 0 0 955356.106 513608.027 0 0 0 5993 145 0

24s Performance

Solver Error Score Correct Score CPU Time Score Wall Time Score Solved Solved SAT Solved UNSAT Unsolved Timeout Memout
Par4 0 2907 80665.317 77643.12 2907 410 2497 3086 3076 10
CVC4 0 2430 90359.415 90311.8 2430 393 2037 3563 3562 0
CVC4-SymBreakn 0 2398 91389.83 91344.793 2398 390 2008 3595 3594 0
Z3n 0 2299 88961.382 88925.002 2299 329 1970 3694 3536 12
2018-Z3n 0 2245 89833.519 89811.581 2245 315 1930 3748 3585 7
2018-Vampiren 0 1521 116058.676 109689.503 1521 0 1521 4472 4472 0
Vampire 0 1455 125364.932 113305.256 1455 0 1455 4538 4538 0
Alt-Ergo 0 841 101444.895 95404.638 841 0 841 5152 3695 177
UltimateEliminator+MathSAT-5.5.4 0 20 25734.318 19991.943 20 0 20 5973 257 0
UltimateEliminator+Yices-2.6.1 0 0 25414.984 19702.56 0 0 0 5993 270 0

n Non-competing.