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

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Yicesn 0 300 30.625 30.7643002336700 0
Yices 2.6.2 0 300 31.352 31.5713002336700 0
Z3n 0 300 65.623 65.6363002336700 0
CVC4 0 300 318.094 318.1473002336700 0
SMTInterpol 0 300 1122.714 574.573002336700 0
veriT 0 262 48831.396 48784.44226219567386 0
Alt-Ergo 0 64 179239.217 175841.7046406423662 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Yicesn 0 300 30.625 30.7643002336700 0
Yices 2.6.2 0 300 31.352 31.5713002336700 0
Z3n 0 300 65.623 65.6363002336700 0
CVC4 0 300 318.094 318.1473002336700 0
SMTInterpol 0 300 1122.714 574.573002336700 0
veriT 0 262 48832.036 48784.18226219567386 0
Alt-Ergo 0 65 180660.337 174403.5816506523561 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 233 6.049 6.1892332330670 0
2018-Yicesn 0 233 6.144 6.2262332330670 0
Z3n 0 233 46.236 46.2482332330670 0
CVC4 0 233 107.235 107.282332330670 0
SMTInterpol 0 233 788.13 365.8922332330670 0
veriT 0 195 45400.385 45352.23619519501056 0
Alt-Ergo 0 0 169962.705 168111.83600030061 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Z3n 0 67 19.386 19.388670672330 0
2018-Yicesn 0 67 24.481 24.538670672330 0
Yices 2.6.2 0 67 25.303 25.382670672330 0
SMTInterpol 0 67 334.585 208.678670672330 0
CVC4 0 67 210.859 210.867670672330 0
veriT 0 67 3431.651 3431.946670672336 0
Alt-Ergo 0 65 10697.632 6291.7456506523561 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Yicesn 0 300 30.625 30.7643002336700 0
Yices 2.6.2 0 300 31.352 31.5713002336700 0
Z3n 0 300 65.623 65.6363002336700 0
CVC4 0 297 256.833 256.8672972336433 0
SMTInterpol 0 297 924.242 421.7412972326533 0
veriT 0 169 3965.714 3965.71116911653131123 0
Alt-Ergo 0 62 4737.998 3620.51462062238123 0

n Non-competing.