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

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

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

Benchmarks: 3136
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 3072 197764.078 168700.9613072172913436464 0
SPASS-SATT 0 3048 282189.257 281995.2453048171313358884 4
2018-SPASS-SATTn 0 3045 295055.067 294911.3473045171713289187 4
Z3n 0 2946 549287.73 549177.789294616631283190190 0
CVC4 0 2841 783304.577 783176.221284115491292295292 0
Ctrl-Ergo 0 2797 1033195.356 867421.359279715231274339134 204
Yices 2.6.2 0 2744 1050186.26 1050208.801274414761268392392 0
SMTInterpol 0 2734 1205032.684 1171829.842273414021332402402 0
CVC4-SymBreakn 0 2646 1307242.706 1328980.076264613621284490490 0
veriT 0 1113 3338624.715 3338782.703111373437920231324 1
ProB 0 274 6591657.04 6592372.0872741829228622718 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 3086 215147.668 152103.1963086173813485050 0
SPASS-SATT 0 3048 282208.177 281992.1653048171313358884 4
2018-SPASS-SATTn 0 3045 295076.397 294907.4773045171713289187 4
Z3n 0 2946 549320.08 549170.529294616631283190190 0
CVC4 0 2841 783358.407 783165.991284115491292295292 0
Ctrl-Ergo 0 2833 1124939.326 825874.02628331534129930398 204
Yices 2.6.2 0 2744 1050239.29 1050196.301274414761268392392 0
SMTInterpol 0 2736 1205091.524 1171803.842273614041332400400 0
CVC4-SymBreakn 0 2646 1321757.416 1328960.066264613621284490490 0
veriT 0 1113 3338791.785 3338736.023111373437920231324 1
ProB 0 274 6591933.66 6592287.1572741829228622718 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 1738 126913.526 82532.942173817380139850 0
2018-SPASS-SATTn 0 1717 162084.481 161997.841171717170141987 4
SPASS-SATT 0 1713 165675.025 165605.88171317130142384 4
Z3n 0 1663 297488.335 297371.5031663166301473190 0
CVC4 0 1549 567155.175 567059.031549154901587292 0
Ctrl-Ergo 0 1534 750026.962 600208.104153415340160298 204
Yices 2.6.2 0 1476 775889.037 775879.6771476147601660392 0
SMTInterpol 0 1404 1045151.738 1027742.5841404140401732400 0
CVC4-SymBreakn 0 1362 1061142.277 1064058.2921362136201774490 0
veriT 0 734 1606797.554 1606762.357734734024021324 1
ProB 0 182 3585929.583 3586284.736182182029542718 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 1348 52234.142 33570.254134801348178850 0
SPASS-SATT 0 1335 80533.152 80386.286133501335180184 4
SMTInterpol 0 1332 123939.786 108061.2581332013321804400 0
2018-SPASS-SATTn 0 1328 96991.916 96909.636132801328180887 4
Ctrl-Ergo 0 1299 338912.363 189665.922129901299183798 204
CVC4 0 1292 180203.232 180106.961292012921844292 0
CVC4-SymBreakn 0 1284 224615.139 228901.7741284012841852490 0
Z3n 0 1283 215831.745 215799.0261283012831853190 0
Yices 2.6.2 0 1268 238350.253 238316.6241268012681868392 0
veriT 0 379 1695994.231 1695973.666379037927571324 1
ProB 0 92 2970004.078 2970002.4219209230442718 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Par4 0 2994 9534.185 5822.129299416651329142142 0
SPASS-SATT 0 2527 23562.509 23409.786252714581069609605 4
Yices 2.6.2 0 2526 17620.525 17568.902252612881238610610 0
2018-SPASS-SATTn 0 2450 24081.823 24004.924245014031047686682 4
Z3n 0 2329 26796.696 26776.302232912801049807807 0
Ctrl-Ergo 0 2301 46909.169 27051.212230112081093835630 204
CVC4 0 2281 31332.521 31250.872228112291052855855 0
SMTInterpol 0 1651 56168.719 44749.132165181883314851485 0
CVC4-SymBreakn 0 1332 49175.502 49124.765133262870418041804 0
veriT 0 902 40494.275 40454.03890261728522341576 1
ProB 0 186 69048.47 69050.5131861325429502833 0

n Non-competing.