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_IDL (Single Query Track)

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 938 307934.359 307947.077938600338104104 0
2018-Yicesn 0 924 319876.37 319902.034924597327118118 0
Yices 2.6.2 0 924 321130.895 321142.934924597327118118 0
Par4 0 922 335958.888 300194.315922591331120120 0
CVC4 0 875 507754.115 507685.121875544331167167 0
veriT 0 773 784001.654 784024.691773453320269269 0
SMTInterpol 0 682 974603.494 967640.255682386296360360 0
ProB 0 173 2086371.547 2086495.6911739875869864 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 944 410170.698 279440.1149446073379898 0
Z3n 0 938 307948.649 307943.617938600338104104 0
2018-Yicesn 0 924 319895.38 319898.304924597327118118 0
Yices 2.6.2 0 924 321146.745 321138.774924597327118118 0
CVC4 0 875 507798.585 507677.421875544331167167 0
veriT 0 773 784036.504 784015.531773453320269269 0
SMTInterpol 0 685 974645.634 967586.655685388297357357 0
ProB 0 173 2086466.227 2086466.8911739875869864 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 607 209742.247 121180.361607607043598 0
Z3n 0 600 148034.842 148029.5176006000442104 0
2018-Yicesn 0 597 141972.722 141974.9085975970445118 0
Yices 2.6.2 0 597 143148.813 143151.1255975970445118 0
CVC4 0 544 329589.187 329521.4325445440498167 0
veriT 0 453 579254.707 579233.8414534530589269 0
SMTInterpol 0 388 704547.303 699904.1433883880654357 0
ProB 0 98 1313511.332 1313510.68698980944864 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 338 90313.807 90314.0993380338704104 0
Par4 0 337 130828.452 88659.753337033770598 0
CVC4 0 331 108609.398 108555.993310331711167 0
2018-Yicesn 0 327 108322.659 108323.3963270327715118 0
Yices 2.6.2 0 327 108397.933 108387.6493270327715118 0
veriT 0 320 135181.797 135181.6893200320722269 0
SMTInterpol 0 297 200498.331 198082.5112970297745357 0
ProB 0 75 703354.894 703356.20575075967864 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 831 9699.562 6321.822831532299211211 0
2018-Yicesn 0 818 6510.767 6511.012818521297224224 0
Yices 2.6.2 0 817 6527.729 6516.407817520297225225 0
Z3n 0 761 8519.399 8508.844761477284281281 0
CVC4 0 585 13471.419 13410.875585312273457457 0
veriT 0 501 14387.03 14385.908501223278541541 0
SMTInterpol 0 439 18792.463 16451.602439217222603603 0
ProB 0 152 21844.916 21844.9911529458890887 0

n Non-competing.