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

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

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

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

Winners

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

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
SMTInterpol 0 541 4649.218 3214.41154133021100 0
Yices 2.6.2 0 540 2563.179 2563.8654032921111 0
2018-Yicesn 0 540 2567.292 2567.76954032921111 0
Z3n 0 540 2687.28 2687.62854032921111 0
veriT 0 540 4614.051 4614.13954032921111 0
CVC4 0 539 5656.556 5657.66853932821122 0
Alt-Ergo 0 200 456223.225 402187.9432000200341130 6

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
SMTInterpol 0 541 4649.218 3214.41154133021100 0
Yices 2.6.2 0 540 2563.369 2563.7854032921111 0
2018-Yicesn 0 540 2567.502 2567.70954032921111 0
Z3n 0 540 2687.56 2687.59854032921111 0
veriT 0 540 4614.171 4614.10954032921111 0
CVC4 0 539 5657.446 5657.61853932821122 0
Alt-Ergo 0 201 466971.375 394859.1782010201340122 6

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
SMTInterpol 0 330 3699.904 2760.19333033002110 0
Yices 2.6.2 0 329 2551.4 2551.6232932902121 0
2018-Yicesn 0 329 2556.269 2556.3732932902121 0
Z3n 0 329 2653.588 2653.61932932902121 0
veriT 0 329 4571.31 4571.25432932902121 0
CVC4 0 328 5513.909 5514.08432832802132 0
Alt-Ergo 0 0 402130.284 360578.51000541122 6

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Yicesn 0 211 11.233 11.33821102113301 0
Yices 2.6.2 0 211 11.968 12.1621102113301 0
Z3n 0 211 33.971 33.97821102113301 0
veriT 0 211 42.861 42.85421102113301 0
CVC4 0 211 143.537 143.53421102113302 0
SMTInterpol 0 211 949.314 454.21721102113300 0
Alt-Ergo 0 201 64841.091 34280.6692010201340122 6

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Yicesn 0 539 93.714 93.91253932821122 0
Yices 2.6.2 0 539 96.123 96.53153932821122 0
veriT 0 538 194.373 194.31653832721133 0
Z3n 0 537 206.592 206.62553732621144 0
CVC4 0 534 348.433 348.36153432421077 0
SMTInterpol 0 534 1957.696 856.73753432520977 0
Alt-Ergo 0 89 15298.058 11343.19789089452402 6

n Non-competing.