SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2017

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

QF_RDL (Main Track)

Competition results for the QF_RDL division as of Fri Jul 21 10:18:02 GMT

Benchmarks in this division: 255
Time Limit: 1200s

Winners

Sequential Performance Parallel Performance
Yices2 Yices2

Result table1

Sequential Performance

Solver Error Score Correct Score CPU Time Unsolved
CVC4 0.000 233.075 134.600 39
SMTInterpol 0.000 216.740 254.612 52
Yices2 0.000 235.886 98.311 34
veriT 0.000 231.850 134.956 40
z3-4.5.0n 0.000 231.602 132.130 40

Parallel Performance

Solver Error Score Correct Score CPU Score WALL Score Unsolved
CVC4 0.000 233.075 134.602 134.617 39
SMTInterpol 0.000 216.740 280.957 245.262 52
Yices2 0.000 235.886 98.314 98.320 34
veriT 0.000 231.850 134.957 134.971 40
z3-4.5.0n 0.000 231.602 132.132 132.147 40

n. Non-competing.

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