SMT-COMP

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions

SMT-COMP 2016

Rules
Benchmarks
Tools
Specs
Participants
Results
Slides
Report

QF_LIRA (Main Track)

Competition results for the QF_LIRA division as of Thu Jul 7 07:24:34 GMT

Benchmarks in this division: 6
Time Limit: 1200s

Winners

Sequential Performance Parallel Performance
Yices2 Yices2

Result table1

Sequential Performance

Solver Error Score Correct Score avg. CPU time
CVC4 0.000 6.000 164.039
SMTInterpol 0.000 3.000 1203.021
Yices2 0.000 6.000 19.110
z3n 0.000 5.000 11.183

Parallel Performance

SolverError Score Correct Score avg. CPU time avg. WALL time Unsolved
CVC4 0.000 6.000 164.039 164.086 0
SMTInterpol 0.000 3.000 1215.079 1200.937 3
Yices2 0.000 6.000 19.110 19.099 0
z3n 0.000 5.000 11.183 11.175 1

n. Non-competitive.

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