SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2018

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

QF_BV (Main Track)

Competition results for the QF_BV division as of Fri Jul 13 00:02:11 GMT

Benchmarks in this division : 40102
Time limit: 1200s

Winners

Sequential PerformanceParallel Performance
BoolectorMinkeyrink-MT

Result table1

Sequential Performance

Solver Error Score Correctly Solved Score CPU time Score Solved Unsolved
Boolector 0.000 36129.153 157.722 39613 489
CVC4 0.000 35397.747 188.042 39274 828
MathSATn 0.000 31912.757 286.331 38570 1532
Minkeyrink-MT 0.000 34177.756 228.504 39327 775
Minkeyrink-ST 0.000 35892.846 172.188 39529 573
STP-CMS-mt-2018 0.000 33817.158 258.014 38421 1681
STP-CMS-st-2018 0.000 35215.086 199.040 38796 1306
STP-Riss-st-2018 0.000 34032.066 232.003 38068 2034
Yices 2.6.0 0.000 32801.421 261.922 39045 1057
z3-4.7.1n 0.000 33199.774 244.757 37349 2753

Parallel Performance

Solver Error Score Correctly Solved Score CPU time Score WALL time Score Solved Unsolved
Boolector 0.00036129.153157.723157.73639613489
CVC4 0.00035397.747188.043187.99039274828
MathSATn 0.00031912.757286.331286.325385701532
Minkeyrink-MT 0.00036465.250602.093157.74939573529
Minkeyrink-ST 0.00035892.846172.189172.18139529573
STP-CMS-mt-2018 0.00035820.543648.331181.409388841218
STP-CMS-st-2018 0.00035215.086199.041199.060387961306
STP-Riss-st-2018 0.00034032.066232.005231.988380682034
Yices 2.6.0 0.00032801.421261.924261.940390451057
z3-4.7.1n 0.00033199.774244.759244.728373492753

n. Non-competing.

1. Scores are computed according to Section 7 of the rules.