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

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

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

Benchmarks: 651
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
Yices 2.6.2 0 651 17.325 18.56865127237900 0
2018-Yicesn 0 651 18.675 19.7865127237900 0
Z3n 0 651 67.211 67.27365127237900 0
CVC4 0 651 711.378 711.35965127237900 0
SMTInterpol 0 651 842.077 442.22165127237900 0
Alt-Ergo 0 356 110485.242 76156.168356035629526 0
veriT 0 135 8.44 8.44513501355160 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 651 17.325 18.56865127237900 0
2018-Yicesn 0 651 18.675 19.7865127237900 0
Z3n 0 651 67.211 67.27365127237900 0
SMTInterpol 0 651 842.077 442.22165127237900 0
CVC4 0 651 711.378 711.35965127237900 0
Alt-Ergo 0 365 144880.672 68654.513365036528617 0
veriT 0 135 8.44 8.44513501355160 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 272 5.607 6.05927227203790 0
2018-Yicesn 0 272 6.034 6.47627227203790 0
Z3n 0 272 11.016 11.02127227203790 0
CVC4 0 272 65.852 65.81227227203790 0
SMTInterpol 0 272 224.046 117.55127227203790 0
veriT 0 0 3.513 3.5280006510 0
Alt-Ergo 0 0 29841.833 16322.72700065117 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 379 11.717 12.50937903792720 0
2018-Yicesn 0 379 12.642 13.30337903792720 0
Z3n 0 379 56.195 56.25337903792720 0
SMTInterpol 0 379 618.031 324.6737903792720 0
CVC4 0 379 645.526 645.54737903792720 0
Alt-Ergo 0 365 115038.839 52331.786365036528617 0
veriT 0 135 4.927 4.91713501355160 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Yices 2.6.2 0 651 17.325 18.56865127237900 0
2018-Yicesn 0 651 18.675 19.7865127237900 0
Z3n 0 650 58.024 58.08465027237811 0
SMTInterpol 0 650 770.046 383.13765027237811 0
CVC4 0 649 208.725 208.62464927237722 0
Alt-Ergo 0 307 7537.461 4198.0293070307344116 0
veriT 0 135 8.44 8.44513501355160 0

n Non-competing.