SMT-COMP 2019

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Papers
Benchmark Submission
Rules
Benchmarks
Tools
Specs
Participants
Results
Slides

Previous Competitions

SMT-LIB

QF_BV (Challenge Track (non-incremental))

Competition results for the QF_BV division in the Challenge Track (non-incremental).

Page generated on 2019-07-23 17:57:29 +0000

Benchmarks: 7
Time Limit: 43200 seconds
Memory Limit: 60 GB

Winners

Sequential PerformanceParallel PerformanceSAT Performance (parallel)UNSAT Performance (parallel)24s Performance (parallel)
BoolectorMinkeyrink Solver MTMinkeyrink Solver MT Minkeyrink Solver MT

Sequential Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Boolectorn 0 7 607.673 607.76377000 0
Boolector 0 7 708.912 708.96277000 0
Yices 2.6.2 CaDiCal 0 7 716.181 716.26577000 0
Minkeyrink Solver MT 0 7 767.592 443.4377000 0
Yices 2.6.2 New Bvsolver 0 7 1111.014 1111.25177000 0
Minkeyrink Solver 0 7 1150.653 1150.72577000 0
2018-Minkeyrink MTn 0 7 1324.014 536.01577000 0
Poolector 0 7 2367.829 640.277000 0
Yices 2.6.2 Cryptominisat 0 7 8453.778 8454.78977000 0
Yices 2.6.2 0 7 12696.426 12697.88477000 0
Z3n 0 7 31544.226 31546.58377000 0
STP-minisat 0 7 43053.772 43054.44577000 0
STP 0 7 43468.136 43471.54877000 0
STP-mergesat-fixedn 0 6 8134.53 8135.1566011 0
STP-portfolio-fixedn 0 6 10278.826 8184.24366011 0
CVC4 0 6 44063.069 44064.67366011 0
STP-mt 0 6 44113.041 43499.46966011 0
STP-mergesat 0 0 42262.973 42266.20500070 0
STP-riss 0 0 42962.673 42969.06800070 0
STP-portfolio 0 0 44986.465 44248.77100070 0

Parallel Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Minkeyrink Solver MT 0 7 767.592 443.4377000 0
2018-Minkeyrink MTn 0 7 1324.014 536.01577000 0
2018-Boolectorn 0 7 607.673 607.76377000 0
Poolector 0 7 2367.829 640.277000 0
Boolector 0 7 708.912 708.96277000 0
Yices 2.6.2 CaDiCal 0 7 716.181 716.26577000 0
Yices 2.6.2 New Bvsolver 0 7 1111.014 1111.25177000 0
Minkeyrink Solver 0 7 1150.653 1150.72577000 0
Yices 2.6.2 Cryptominisat 0 7 8453.778 8454.78977000 0
Yices 2.6.2 0 7 12696.426 12697.88477000 0
Z3n 0 7 31544.226 31546.58377000 0
STP-minisat 0 7 43053.772 43054.44577000 0
STP 0 7 43468.136 43471.54877000 0
STP-mergesat-fixedn 0 6 8134.53 8135.1566011 0
STP-portfolio-fixedn 0 6 10278.826 8184.24366011 0
STP-mt 0 6 44113.041 43499.46966011 0
CVC4 0 6 44064.469 44064.57366011 0
STP-mergesat 0 0 42262.973 42266.20500070 0
STP-riss 0 0 42962.673 42969.06800070 0
STP-portfolio 0 0 44986.465 44248.77100070 0

SAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Minkeyrink Solver MT 0 7 767.592 443.4377000 0
2018-Minkeyrink MTn 0 7 1324.014 536.01577000 0
2018-Boolectorn 0 7 607.673 607.76377000 0
Poolector 0 7 2367.829 640.277000 0
Boolector 0 7 708.912 708.96277000 0
Yices 2.6.2 CaDiCal 0 7 716.181 716.26577000 0
Yices 2.6.2 New Bvsolver 0 7 1111.014 1111.25177000 0
Minkeyrink Solver 0 7 1150.653 1150.72577000 0
Yices 2.6.2 Cryptominisat 0 7 8453.778 8454.78977000 0
Yices 2.6.2 0 7 12696.426 12697.88477000 0
Z3n 0 7 31544.226 31546.58377000 0
STP-minisat 0 7 43053.772 43054.44577000 0
STP 0 7 43468.136 43471.54877000 0
STP-mergesat-fixedn 0 6 8134.53 8135.1566011 0
STP-portfolio-fixedn 0 6 10278.826 8184.24366011 0
STP-mt 0 6 44113.041 43499.46966011 0
CVC4 0 6 44064.469 44064.57366011 0
STP-mergesat 0 0 42262.973 42266.20500070 0
STP-riss 0 0 42962.673 42969.06800070 0
STP-portfolio 0 0 44986.465 44248.77100070 0

UNSAT Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
2018-Boolectorn 0 0 0.0 0.000070 0
2018-Minkeyrink MTn 0 0 0.0 0.000070 0
Boolector 0 0 0.0 0.000070 0
CVC4 0 0 0.0 0.000071 0
Minkeyrink Solver 0 0 0.0 0.000070 0
Minkeyrink Solver MT 0 0 0.0 0.000070 0
Poolector 0 0 0.0 0.000070 0
STP 0 0 0.0 0.000070 0
STP-mergesat 0 0 0.0 0.000070 0
STP-minisat 0 0 0.0 0.000070 0
STP-mt 0 0 0.0 0.000071 0
STP-portfolio 0 0 0.0 0.000070 0
STP-riss 0 0 0.0 0.000070 0
Yices 2.6.2 0 0 0.0 0.000070 0
Yices 2.6.2 CaDiCal 0 0 0.0 0.000070 0
Yices 2.6.2 Cryptominisat 0 0 0.0 0.000070 0
Yices 2.6.2 New Bvsolver 0 0 0.0 0.000070 0
Z3n 0 0 0.0 0.000070 0
STP-mergesat-fixedn 0 0 0.0 0.000071 0
STP-portfolio-fixedn 0 0 0.0 0.000071 0

24 seconds Performance

Solver Error Score Correct Score CPU Time Score Wall Time ScoreSolvedSolved SATSolved UNSATUnsolvedTimeout Memout
Minkeyrink Solver MT 0 4 194.556 129.7244033 0
STP-mt 0 3 136.029 117.55533044 0
2018-Minkeyrink MTn 0 3 203.363 133.49633044 0
Minkeyrink Solver 0 2 143.674 143.67622055 0
Z3n 0 2 145.367 145.36722055 0
2018-Boolectorn 0 2 156.169 156.17622055 0
Poolector 0 2 263.006 156.36222055 0
STP 0 1 150.84 150.84211066 0
Boolector 0 1 159.007 159.00911066 0
STP-minisat 0 1 160.925 160.92511066 0
Yices 2.6.2 CaDiCal 0 1 161.719 161.71811066 0
STP-mergesat 0 0 65.273 65.30500071 0
STP-riss 0 0 69.073 74.66800071 0
STP-portfolio 0 0 162.852 161.13200076 0
CVC4 0 0 168.0 168.000077 0
Yices 2.6.2 0 0 168.0 168.000077 0
Yices 2.6.2 Cryptominisat 0 0 168.0 168.000077 0
Yices 2.6.2 New Bvsolver 0 0 168.0 168.000077 0
STP-mergesat-fixedn 0 0 168.0 168.000077 0
STP-portfolio-fixedn 0 0 168.0 168.000077 0

n Non-competing.