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_AX (Main Track)

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

Benchmarks in this division: 551
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 551.000 0.085
MathSat5n 0.000 551.000 0.059
SMTInterpol 0.000 551.000 1.183
Yices2 0.000 551.000 0.011
z3n 0.000 551.000 0.067

Parallel Performance

SolverError Score Correct Score avg. CPU time avg. WALL time Unsolved
CVC4 0.000 551.000 0.085 0.086 0
MathSat5n 0.000 551.000 0.059 0.058 0
SMTInterpol 0.000 551.000 1.183 0.523 0
Yices2 0.000 551.000 0.011 0.017 0
z3n 0.000 551.000 0.067 0.066 0

n. Non-competitive.

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