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

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

Benchmarks in this division : 10245

Winners

Sequential Performance Parallel Performance
Yices2 Yices2

Result table1

Sequential Performance

Solver Error Score Correct Score avg. CPU time
CVC4 0.000 1081.079 0.171
SMT-RAT 5.596 9079.258 268.504
Yices2 0.000 9860.239 101.448
raSAT 0.3 0.000 7893.839 551.473
raSAT 0.4 0.000 8784.741 340.970
z3n 0.000 9875.032 80.073

Parallel Performance

SolverError Score Correct Score avg. CPU time avg. WALL time Unsolved
CVC4 0.000 1081.079 0.171 0.164 7551
SMT-RAT 5.596 9079.258 268.663 268.506 1215
Yices2 0.000 9860.239 101.499 101.450 226
raSAT 0.3 131.426 7893.839 551.797 551.485 1552
raSAT 0.4 0.000 8787.700 674.903 336.415 1221
z3n 0.000 9875.032 80.112 80.068 189

n. Non-competitive.

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