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

UF (Main Track)

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

Benchmarks in this division: 7562
Time Limit: 1200s

Winners

Sequential Performance Parallel Performance
vampire 4.2 vampire 4.2

Result table1

Sequential Performance

Solver Error Score Correct Score CPU Time Unsolved
CVC4 0.000 4321.108 546.993 3438
vampire 4.2 0.000 4413.241 517.145 3313
veriT 0.000 3645.162 623.098 4320
z3-4.5.0n 0.000 3142.850 580.609 4716

Parallel Performance

Solver Error Score Correct Score CPU Score WALL Score Unsolved
CVC4 0.000 4321.644 547.471 554.718 3437
vampire 4.2 0.000 4481.063 1620.059 415.948 3245
veriT 0.000 3645.162 624.413 623.124 4320
z3-4.5.0n 0.000 3142.850 580.610 580.799 4716

n. Non-competing.

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