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

QF_UF (Single Query Track)

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

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

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

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
Yices 2.6.2Par4Yices 2.6.2 Par4 Par4

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 3512 417.659 422.38235121452206000 0
2018-Yicesn 0 3512 444.924 446.41935121452206000 0
Par4 0 3512 478.936 380.62135121452206000 0
veriT 0 3512 1519.372 1517.53835121452206000 0
CVC4 0 3510 15684.755 15682.53935101452205822 0
OpenSMT2 0 3510 17079.175 17063.67535101451205922 0
Z3n 0 3476 93821.293 93797.9633476145220243636 0
SMTInterpol 0 3474 116925.145 109649.8443474145220223838 0
Alt-Ergo 0 1606 2531524.051 1973594.7051606016061906667 21

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 3512 478.936 380.62135121452206000 0
Yices 2.6.2 0 3512 417.659 422.38235121452206000 0
2018-Yicesn 0 3512 444.924 446.41935121452206000 0
veriT 0 3512 1519.372 1517.53835121452206000 0
CVC4 0 3510 15685.195 15682.42935101452205822 0
OpenSMT2 0 3510 17079.705 17063.53535101451205922 0
Z3n 0 3476 93829.333 93796.3833476145220243636 0
SMTInterpol 0 3474 116925.145 109649.8443474145220223838 0
Alt-Ergo 0 1883 3259319.061 1638425.6851883018831629371 21

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 1452 51.502 53.82314521452020600 0
2018-Yicesn 0 1452 53.633 54.35514521452020600 0
Par4 0 1452 24.354 59.96714521452020600 0
veriT 0 1452 148.176 148.05414521452020600 0
Z3n 0 1452 319.131 319.217145214520206036 0
SMTInterpol 0 1452 3215.728 1323.107145214520206038 0
CVC4 0 1452 1387.755 1387.82914521452020602 0
OpenSMT2 0 1451 5884.11 5884.94914511451020612 0
Alt-Ergo 0 0 943721.256 737444.4370003512371 21

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 2060 454.582 320.65420600206014520 0
Yices 2.6.2 0 2060 366.157 368.5620600206014520 0
2018-Yicesn 0 2060 391.292 392.06420600206014520 0
veriT 0 2060 1371.196 1369.48520600206014520 0
OpenSMT2 0 2059 11195.595 11178.58720590205914532 0
CVC4 0 2058 14297.439 14294.620580205814542 0
Z3n 0 2024 93510.202 93477.166202402024148836 0
SMTInterpol 0 2022 113709.417 108326.737202202022149038 0
Alt-Ergo 0 1883 2315597.805 900981.2471883018831629371 21

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 3510 348.876 339.45235101452205822 0
Yices 2.6.2 0 3509 355.218 359.93535091452205733 0
2018-Yicesn 0 3509 371.652 373.13235091452205733 0
veriT 0 3508 491.257 489.32135081452205644 0
OpenSMT2 0 3457 3591.845 3574.9873457144120165555 0
CVC4 0 3455 3253.438 3249.4933455144620095757 0
Z3n 0 3428 3454.353 3450.4863428144819808484 0
SMTInterpol 0 3412 13490.059 6898.352341214511961100100 0
Alt-Ergo 0 959 93869.855 66814.792959095925532311 21

n Non-competing.