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

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

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

Benchmarks: 11494
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 8971 6669100.357 6217845.83389716142282925232368 155
CVC4 0 8289 9049915.549 9312701.24682895785250432053145 60
CVC4-SymBreakn 0 7936 10150889.498 10253204.12379365542239435583526 11
Yices 2.6.2 0 7642 9539458.61 9542887.59576425106253638523852 0
2018-CVC4n 0 7387 10315282.403 10412342.71873875101228641074019 59
Z3n 0 5276 15583575.037 15590828.0952763344193262186010 2
AProVE 0 4165 14649432.473 17992548.13741654165073297233 0
SMT-RAT 0 1041 25111697.825 25126644.85210417642771045310426 1
ProB 0 348 19347770.845 19461161.61734826484111467822 0
MathSAT-default 2 8109 8843151.29 8847791.81381095564254533853382 1
MathSAT-na-ext 5 7892 9207941.341 9213582.62778925382251036023597 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 9084 7001271.317 6089981.49790846229285524102255 155
CVC4 0 8289 9304966.749 9312543.25682895785250432053145 60
CVC4-SymBreakn 0 7936 10246658.578 10253017.15379365542239435583526 11
Yices 2.6.2 0 7642 9542876.64 9542746.00576425106253638523852 0
2018-CVC4n 0 7387 10408606.763 10412159.24873875101228641074019 59
Z3n 0 5276 15590372.767 15590570.7752763344193262186010 2
AProVE 0 4168 18008043.77 17992440.43741684168073267230 0
SMT-RAT 0 1041 25125565.855 25126187.32210417642771045310426 1
ProB 0 348 19370042.845 19460928.28734826484111467822 0
MathSAT-default 2 8109 8847365.3 8847651.86381095564254533853382 1
MathSAT-na-ext 5 7892 9213466.411 9213426.97778925382251036023597 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 6229 2107070.975 1402095.52162296229052652255 155
CVC4 0 5785 3642862.147 3649537.48557855785057093145 60
CVC4-SymBreakn 0 5542 4377181.822 4383045.53655425542059523526 11
Yices 2.6.2 0 5106 4089051.978 4088940.87851065106063883852 0
2018-CVC4n 0 5101 4399140.536 4402593.56251015101063934019 59
AProVE 0 4168 6701612.37 6686020.28541684168073267230 0
Z3n 0 3344 8761977.162 8762119.98433443344081506010 2
SMT-RAT 0 764 14340413.557 14340552.44976476401073010426 1
ProB 0 264 11344334.432 11378531.2812642640112307822 0
MathSAT-default 2 5564 3338667.101 3338964.14455645564059303382 1
MathSAT-na-ext 5 5382 3648017.362 3648046.42153825382061123597 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 2855 516599.873 332021.67628550285586392255 155
MathSAT-default 0 2545 1152698.199 1152687.71925450254589493382 1
Yices 2.6.2 0 2536 1100224.662 1100205.12725360253689583852 0
MathSAT-na-ext 0 2510 1209449.049 1209380.55625100251089843597 0
CVC4 0 2504 1308504.602 1309405.77125040250489903145 60
CVC4-SymBreakn 0 2394 1523113.898 1523579.48623940239491003526 11
2018-CVC4n 0 2286 1662846.555 1662930.77922860228692084019 59
Z3n 0 1932 2693739.823 2693733.16119320193295626010 2
SMT-RAT 0 277 6438298.149 6438758.95627702771121710426 1
ProB 0 84 4812505.199 4845772.49284084114107822 0
AProVE 0 0 7087204.385 7087203.018000114947230 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 7994 159469.142 104683.85379945374262035003345 155
Yices 2.6.2 0 6539 134264.703 134175.09965394209233049554955 0
CVC4 0 5043 174751.229 174566.81650433226181764516391 60
2018-CVC4n 0 4982 176849.047 176667.71249823182180065126453 59
CVC4-SymBreakn 0 4761 185243.739 185115.4547613046171567336722 11
Z3n 0 3088 219342.011 219160.75230881824126484068398 2
AProVE 0 3003 219126.35 211881.33430033003084918395 0
SMT-RAT 0 828 257727.345 257734.0418285832451066610663 1
ProB 0 290 212949.663 213016.72729023357112048493 0
MathSAT-default 1 5932 159519.94 159330.21459323916201655625560 1
MathSAT-na-ext 3 5855 160069.328 159897.90958553868198756395636 0

n Non-competing.