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

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

Benchmarks in this division: 2
Time Limit: 1200s

Winners

Sequential Performance Parallel Performance
CVC4 CVC4

Result table1

Sequential Performance

Solver Error Score Correct Score avg. CPU time
CVC4 0.000 2.000 6.771
Yices2 0.000 1.000 1200.002
raSAT 0.3 0.000 0.000 0.437
raSAT 0.4 0.000 0.000 19.911
z3n 0.000 1.000 0.154

Parallel Performance

SolverError Score Correct Score avg. CPU time avg. WALL time Unsolved
CVC4 0.000 2.000 6.771 6.767 0
Yices2 0.000 1.000 1200.717 1200.066 1
raSAT 0.3 0.000 0.000 0.437 0.441 2
raSAT 0.4 0.000 0.000 19.911 2400.050 2
z3n 0.000 1.000 0.154 0.153 1

n. Non-competitive.

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